MachineRegularMetadata.lean`

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.Extra line 56
instance OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.(instance at line 59) line 59
abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.Tape line 61
abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.Alphabet line 62
abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.State line 63
inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.Label line 65
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.ownerTapes line 76
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankTape line 78
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixTape line 86
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudTape line 101
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.program line 115
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankView line 141
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixView line 152
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudView line 170
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankView_left line 184
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankView_right line 186
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixView_left line 192
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixView_right line 198
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudView_left line 204
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudView_right line 206
structure OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.Data line 212
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.frame line 225
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.frame_index line 240
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.frame_query_empty line 243
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cfg line 246
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudData line 250
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudTrace line 256
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.join_trace_inline_MachineRegularMetadata line 292
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.drainAt_inline_MachineRegularMetadata line 296
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixData line 306
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixSteps line 310
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.prefixTrace line 313
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.selected_owner line 365
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.ownerData line 373
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder line 376
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.ownerSteps line 379
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.ownerTrace line 383
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankQuery line 429
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.queryFrame line 431
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.querySteps line 435
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.queryTrace line 437
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankData line 476
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder line 480
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankSteps line 484
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankTrace line 490
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.originalMember line 553
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.originalData line 556
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.totalTime line 560
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.originalTrace line 564
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.encodeWords_drop_length_le_inline_MachineRegularMetadata line 585
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder_length_le line 592
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder_length_le line 596
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.timePolynomial line 607
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.overhead line 611
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.overhead_le line 615
theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.totalTime_le line 620
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.originalInTime line 670
def OAI.DFVSGames.Foundations.Complexity.MachineRegularMetadata.cloudInTime line 685
abbrev OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.degree line 706
abbrev OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.cloudSize line 707
abbrev OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.rowFactor line 708
structure OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.Control line 710
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.squarePorts line 718
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.start line 721
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.receiveFirst line 732
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.receiveSecond line 735
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.firstOffset line 742
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.secondOffset line 743
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputPort line 745
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputOffset line 748
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.firstAddress line 751
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.secondAddress line 754
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputAddress line 757
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.firstOffset_receiveFirst line 760
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.secondOffset_receiveFirst line 763
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.receiveFirst_port line 766
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.receiveSecond_port line 769
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.firstAddress_eq_rowIndex line 772
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.secondAddress_eq_rowIndex line 778
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.firstAddress_lt line 784
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.secondAddress_lt line 789
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.lookup_vertex_div line 794
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.lookup_port_mod line 797
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.lookup_port_eq_remainder line 800
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.rowIndex_lookup line 804
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputPair line 808
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_rowIndex line 812
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputAddress_lt line 818
def OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.evaluateRow line 823
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.evaluateRow_eq_lookup_step line 832
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_row line 841
theorem OAI.DFVSGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_reverseIndex line 849