OAI/Computability/DirectedFeedback/RankGraph/MachineClone100Finish.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Explicit.MachineClone100Finish.finishTapes line 59
  2. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.finishTapes_counter line 63
  3. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.finishTapes_reversed line 66
  4. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.finishTapes_output line 69
  5. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.finishTapes_other line 73
  6. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.counterStep line 78
  7. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.finishTrace line 85
  8. def OAI.DFVSGames.Explicit.MachineClone100Finish.finishInTime line 109
  9. theorem OAI.DFVSGames.Explicit.MachineClone100Finish.finish_eq_haltList line 118
  10. def OAI.DFVSGames.Explicit.MachineClone100Run.tm line 146
  11. def OAI.DFVSGames.Explicit.MachineClone100Run.emptyTapes line 149
  12. def OAI.DFVSGames.Explicit.MachineClone100Run.sourceBody line 151
  13. def OAI.DFVSGames.Explicit.MachineClone100Run.outputHeaders line 154
  14. def OAI.DFVSGames.Explicit.MachineClone100Run.outputBody line 158
  15. def OAI.DFVSGames.Explicit.MachineClone100Run.outputBits line 163
  16. def OAI.DFVSGames.Explicit.MachineClone100Run.inputTapes line 167
  17. def OAI.DFVSGames.Explicit.MachineClone100Run.guardTapes line 170
  18. def OAI.DFVSGames.Explicit.MachineClone100Run.afterLoopTapes line 175
  19. theorem OAI.DFVSGames.Explicit.MachineClone100Run.inputBits_eq line 180
  20. theorem OAI.DFVSGames.Explicit.MachineClone100Run.initList_eq line 185
  21. theorem OAI.DFVSGames.Explicit.MachineClone100Run.headers_result_eq line 198
  22. theorem OAI.DFVSGames.Explicit.MachineClone100Run.afterLoop_reversed line 205
  23. theorem OAI.DFVSGames.Explicit.MachineClone100Run.afterLoop_length line 210
  24. theorem OAI.DFVSGames.Explicit.MachineClone100Run.finish_eq line 216
  25. def OAI.DFVSGames.Explicit.MachineClone100Run.runInTime line 228
  26. def OAI.DFVSGames.Explicit.MachineClone100Certified.timePolynomial line 278
  27. theorem OAI.DFVSGames.Explicit.MachineClone100Certified.timePolynomial_eval line 282
  28. theorem OAI.DFVSGames.Explicit.MachineClone100Certified.numericalBudget_inline_MachineClone100Certified line 288
  29. def OAI.DFVSGames.Explicit.MachineClone100Certified.certifiedFunction line 302
  30. def OAI.DFVSGames.Explicit.MachineClone100.indices line 351
  31. def OAI.DFVSGames.Explicit.MachineClone100.triples line 354
  32. theorem OAI.DFVSGames.Explicit.MachineClone100.triples_length line 356
  33. theorem OAI.DFVSGames.Explicit.MachineClone100.triples_nonempty line 359
  34. theorem OAI.DFVSGames.Explicit.MachineClone100.equation_words line 364
  35. theorem OAI.DFVSGames.Explicit.MachineClone100.body_words line 372
  36. theorem OAI.DFVSGames.Explicit.MachineClone100.input_words_eq line 378
  37. theorem OAI.DFVSGames.Explicit.MachineClone100.input_bits_eq line 387
  38. theorem OAI.DFVSGames.Explicit.MachineClone100.serialized_polynomial_inline_MachineClone100 line 393
  39. theorem OAI.DFVSGames.Explicit.MachineClone100.size_bound line 406
  40. def OAI.DFVSGames.Explicit.MachineClone100.computation line 418
  41. theorem OAI.DFVSGames.Explicit.MachineClone100.finiteAlphabet line 423
  42. def OAI.DFVSGames.Explicit.MachineClone100.fullRunInTime line 426
  43. inductive OAI.DFVSGames.BinaryValidatorMachine.Mode line 439
  44. def OAI.DFVSGames.BinaryValidatorMachine.afterName line 448
  45. def OAI.DFVSGames.BinaryValidatorMachine.nextMode line 451
  46. def OAI.DFVSGames.BinaryValidatorMachine.run line 461
  47. theorem OAI.DFVSGames.BinaryValidatorMachine.run_reject line 465
  48. theorem OAI.DFVSGames.BinaryValidatorMachine.run_done_iff line 470
  49. theorem OAI.DFVSGames.BinaryValidatorMachine.finalDigit_true_iff_inline_MachineBinaryValidatorMachine line 475
  50. theorem OAI.DFVSGames.BinaryValidatorMachine.run_frame line 492
  51. theorem OAI.DFVSGames.BinaryValidatorMachine.run_name line 504
  52. theorem OAI.DFVSGames.BinaryValidatorMachine.run_literal line 509
  53. theorem OAI.DFVSGames.BinaryValidatorMachine.run_clause line 514
  54. theorem OAI.DFVSGames.BinaryValidatorMachine.run_clauses line 518
  55. theorem OAI.DFVSGames.BinaryValidatorMachine.run_formula line 525
  56. theorem OAI.DFVSGames.BinaryValidatorMachine.frame_inverse line 528
  57. theorem OAI.DFVSGames.BinaryValidatorMachine.name_inverse line 558
  58. theorem OAI.DFVSGames.BinaryValidatorMachine.literal_inverse line 567
  59. theorem OAI.DFVSGames.BinaryValidatorMachine.clause_inverse line 578
  60. theorem OAI.DFVSGames.BinaryValidatorMachine.clauses_inverse_aux_inline_MachineBinaryValidatorMachine line 591
  61. theorem OAI.DFVSGames.BinaryValidatorMachine.run_clause_iff line 618
  62. def OAI.DFVSGames.BinaryValidatorMachine.accepts line 628
  63. theorem OAI.DFVSGames.BinaryValidatorMachine.accepts_eq_decode line 630
  64. abbrev OAI.DFVSGames.BinaryValidatorMachine.Alphabet line 650
  65. abbrev OAI.DFVSGames.BinaryValidatorMachine.State line 651
  66. def OAI.DFVSGames.BinaryValidatorMachine.instruction line 653
  67. abbrev OAI.DFVSGames.BinaryValidatorMachine.machine line 661
  68. def OAI.DFVSGames.BinaryValidatorMachine.tapes line 672
  69. def OAI.DFVSGames.BinaryValidatorMachine.cfg line 676
  70. theorem OAI.DFVSGames.BinaryValidatorMachine.tapes_input line 680
  71. theorem OAI.DFVSGames.BinaryValidatorMachine.tapes_output line 683
  72. theorem OAI.DFVSGames.BinaryValidatorMachine.update_input_inline_MachineBinaryValidatorMachine line 686
  73. theorem OAI.DFVSGames.BinaryValidatorMachine.update_output_inline_MachineBinaryValidatorMachine line 691
  74. theorem OAI.DFVSGames.BinaryValidatorMachine.step_empty line 696
  75. theorem OAI.DFVSGames.BinaryValidatorMachine.step_cons line 703
  76. theorem OAI.DFVSGames.BinaryValidatorMachine.runTrace line 711
  77. theorem OAI.DFVSGames.BinaryValidatorMachine.initList_eq line 726
  78. theorem OAI.DFVSGames.BinaryValidatorMachine.haltList_eq line 733
  79. theorem OAI.DFVSGames.BinaryValidatorMachine.validatorTrace line 740
  80. def OAI.DFVSGames.BinaryValidatorMachine.outputsInTime line 752
  81. def OAI.DFVSGames.BinaryValidatorMachine.computableInPolyTime line 759
  82. theorem OAI.DFVSGames.BinaryValidatorMachine.machine_finiteAlphabet line 773