GraphCounterFinish.lean`

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.extraTapes line 10
def OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.frame line 15
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.trace_trans_inline_GraphCounterFinish line 22
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.start_eq line 26
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.finish_eq line 39
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.drainTrace line 51
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.clockCopyTrace line 68
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.archiveCopyTrace line 89
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.reverseTrace line 111
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.finishTrace line 137
def OAI.DFVSGames.Foundations.Complexity.GraphCounterFinish.finishInTime line 152
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.rawOutput line 167
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.rawInTime line 170
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.count line 194
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.output line 196
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.rowsBits line 199
theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.tableBits_decomposition line 202
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.outputsInTime line 206
def OAI.DFVSGames.Foundations.Complexity.GraphCounterPrefix.computableInPolyTime line 212
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.rounds line 236
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.rounds_le line 238
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.two_pow_rounds_le line 241
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.growth_pow_rounds_le line 248
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.sizeEnvelope line 256
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.semanticSize_geometric line 258
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.semanticSize_bound line 272
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial line 285
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial_eval line 288
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.timePolynomial line 292
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.timePolynomial_eval line 297
abbrev OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.Alphabet line 305
abbrev OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.State line 306
abbrev OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.Labels line 307
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.program line 309
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.program_guard line 317
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.machine line 322
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.haltedConfiguration line 335
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.haltStep line 340
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.iterationTrace line 350
theorem OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.bodyCosts_bound line 366
def OAI.DFVSGames.Foundations.Complexity.PCPIterationMachine.iterationInTime line 383
def OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.inputBits line 418
def OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.countedBits line 420
def OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.words line 422
def OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.count line 425
def OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.lengthPolynomial line 427
theorem OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.inputBits_le_countedBits line 430
theorem OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.size_le_inputBits line 434
theorem OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.count_le line 439
theorem OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.intermediate_size line 443
theorem OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.intermediate_bits line 451
def OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial line 467
theorem OAI.DFVSGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial_eval line 471
abbrev OAI.DFVSGames.Foundations.PCP.RawInitialRows.Signs line 484
abbrev OAI.DFVSGames.Foundations.PCP.RawInitialRows.Names line 485
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.clauseSigns line 487
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.clauseNames line 490
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.nameWord line 493
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.decodedLabel line 498
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.incidencePredicate line 501
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.relationPredicate line 509
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.relationWordsFor line 514
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.relationWordsFor_length line 517
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.incidenceWords line 521
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.clauseWords line 527
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.dummyWords line 535
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.orderedList line 544
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.orderedList_cast line 547
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.orderedList_prod line 552
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.orderedList_sum line 576
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.clauseDarts line 590
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.orderedList_dartOrder line 595
def OAI.DFVSGames.Foundations.PCP.RawInitialRows.rowFor line 608
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.rowList_table line 614
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.rowWords_incidence line 620
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.rowWords_dummy line 640
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.clauseDarts_rowWords line 653
theorem OAI.DFVSGames.Foundations.PCP.RawInitialRows.tableWords_eq line 659
inductive OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.Tape line 675
abbrev OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.Signs line 680
abbrev OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.State line 681
abbrev OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.Alphabet line 682
inductive OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.CopyPhase line 684
inductive OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.Label line 692
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.initialState line 706
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.stateKeys line 708
theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.stateKeys_complete line 713
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.nameField line 719
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.copySource line 721
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.copyScale line 726
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.copyNext line 730
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.relationNext line 739
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.finalTape line 745
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.drain line 748
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.headerTape line 751
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.relationOutput line 753
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.program line 757
def OAI.DFVSGames.Foundations.PCP.RawInitialMachineModel.machine line 807