OAI/GroupTheory/PeriodicGroups/Machines/ProgramFixedPoint.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.FiniteCode.rename line 12
  2. def OAI.SourceBurnside.FiniteCode.config line 14
  3. lemma OAI.SourceBurnside.FiniteCode.rename_next line 15
  4. lemma OAI.SourceBurnside.FiniteCode.rename_exec line 18
  5. lemma OAI.SourceBurnside.FiniteCode.exec_halt line 23
  6. lemma OAI.SourceBurnside.FiniteCode.after_halt line 28
  7. lemma OAI.SourceBurnside.FiniteCode.first_halt line 31
  8. def OAI.SourceBurnside.FiniteCode.enumeration line 41
  9. lemma OAI.SourceBurnside.FiniteCode.enumeration_zero line 43
  10. def OAI.SourceBurnside.FiniteCode.program line 44
  11. lemma OAI.SourceBurnside.FiniteCode.first_program_trace line 46
  12. lemma OAI.SourceBurnside.FiniteCode.program_trace line 66
  13. abbrev OAI.SourceBurnside.LiteralCompiler.K line 86
  14. def OAI.SourceBurnside.LiteralCompiler.src line 87
  15. def OAI.SourceBurnside.LiteralCompiler.dst line 88
  16. lemma OAI.SourceBurnside.LiteralCompiler.distinct line 89
  17. def OAI.SourceBurnside.LiteralCompiler.start line 91
  18. def OAI.SourceBurnside.LiteralCompiler.result line 93
  19. def OAI.SourceBurnside.LiteralCompiler.tokens line 96
  20. def OAI.SourceBurnside.LiteralCompiler.code line 98
  21. def OAI.SourceBurnside.LiteralCompiler.loaderTime line 99
  22. def OAI.SourceBurnside.LiteralCompiler.runTime line 102
  23. lemma OAI.SourceBurnside.LiteralCompiler.input_regs line 104
  24. lemma OAI.SourceBurnside.LiteralCompiler.compiled_trace line 110
  25. lemma OAI.SourceBurnside.LiteralCompiler.header_trace line 129
  26. lemma OAI.SourceBurnside.LiteralCompiler.specialized_trace line 148
  27. lemma OAI.SourceBurnside.PolynomialAccounting.powers line 170
  28. def OAI.SourceBurnside.PolynomialAccounting.compactCoefficient line 174
  29. lemma OAI.SourceBurnside.PolynomialAccounting.compact_bound line 175
  30. lemma OAI.SourceBurnside.PolynomialAccounting.interpreter_bound line 191
  31. lemma OAI.SourceBurnside.PolynomialAccounting.oneTape_bound line 197
  32. def OAI.SourceBurnside.RawTimeBound.size line 210
  33. def OAI.SourceBurnside.RawTimeBound.quoteCost line 211
  34. def OAI.SourceBurnside.RawTimeBound.inputCoefficient line 212
  35. def OAI.SourceBurnside.RawTimeBound.coefficient line 213
  36. lemma OAI.SourceBurnside.RawTimeBound.positive line 217
  37. lemma OAI.SourceBurnside.RawTimeBound.request_length line 218
  38. lemma OAI.SourceBurnside.RawTimeBound.twoinput_length line 224
  39. lemma OAI.SourceBurnside.RawTimeBound.envelope_length line 232
  40. lemma OAI.SourceBurnside.RawTimeBound.arithmetic_size line 235
  41. lemma OAI.SourceBurnside.RawTimeBound.trace_bound line 242
  42. def OAI.SourceBurnside.LiteralCompiler.coefficient line 276
  43. lemma OAI.SourceBurnside.LiteralCompiler.specialized_bound line 279
  44. lemma OAI.SourceBurnside.RawFixedPoint.body_exponents line 310
  45. lemma OAI.SourceBurnside.RawFixedPoint.body_boolean line 318
  46. theorem OAI.SourceBurnside.RawFixedPoint.construct line 333
  47. theorem OAI.SourceBurnside.RawFixedPoint.source_predicate_selfpoint line 372
  48. theorem OAI.SourceBurnside.RawFixedPoint.constructTimed line 392
  49. abbrev OAI.SourceBurnside.TimedTape.K line 447
  50. abbrev OAI.SourceBurnside.TimedTape.SK line 448
  51. abbrev OAI.SourceBurnside.TimedTape.TK line 449
  52. abbrev OAI.SourceBurnside.TimedTape.SQ line 450
  53. abbrev OAI.SourceBurnside.TimedTape.Γ line 451
  54. abbrev OAI.SourceBurnside.TimedTape.Q line 452
  55. def OAI.SourceBurnside.TimedTape.machine line 453
  56. def OAI.SourceBurnside.TimedTape.δ line 454
  57. def OAI.SourceBurnside.TimedTape.start line 455
  58. def OAI.SourceBurnside.TimedTape.finish line 457
  59. def OAI.SourceBurnside.TimedTape.blank line 459
  60. def OAI.SourceBurnside.TimedTape.origin line 460
  61. def OAI.SourceBurnside.TimedTape.bitSymbol line 461
  62. def OAI.SourceBurnside.TimedTape.initialState line 462
  63. def OAI.SourceBurnside.TimedTape.finalState line 463
  64. def OAI.SourceBurnside.TimedTape.output line 464
  65. lemma OAI.SourceBurnside.TimedTape.start_length line 465
  66. lemma OAI.SourceBurnside.TimedTape.finish_halt line 473
  67. lemma OAI.SourceBurnside.TimedTape.origin_tape line 475
  68. lemma OAI.SourceBurnside.TimedTape.finish_output line 477
  69. lemma OAI.SourceBurnside.TimedTape.frozen line 481
  70. lemma OAI.SourceBurnside.TimedTape.output_injective line 482
  71. lemma OAI.SourceBurnside.TimedTape.construct line 486
  72. lemma OAI.SourceBurnside.TimedTape.source_predicate line 512
  73. inductive OAI.SourceBurnside.Tableau.Formula line 529
  74. def OAI.SourceBurnside.Tableau.Formula.eval line 536
  75. def OAI.SourceBurnside.Tableau.Formula.map line 540
  76. lemma OAI.SourceBurnside.Tableau.Formula.eval_map line 544
  77. def OAI.SourceBurnside.Tableau.Formula.neg line 546
  78. def OAI.SourceBurnside.Tableau.Formula.conj line 547
  79. def OAI.SourceBurnside.Tableau.Formula.disj line 548
  80. def OAI.SourceBurnside.Tableau.Formula.mux line 549
  81. lemma OAI.SourceBurnside.Tableau.Formula.eval_mux line 550
  82. theorem OAI.SourceBurnside.Tableau.Formula.represents line 556
  83. def OAI.SourceBurnside.Tableau.Circuit.rename line 578
  84. structure OAI.SourceBurnside.Tableau.Circuit.Extension line 581
  85. lemma OAI.SourceBurnside.Tableau.Circuit.Extension.refl line 585
  86. lemma OAI.SourceBurnside.Tableau.Circuit.Extension.trans line 586
  87. lemma OAI.SourceBurnside.Tableau.Circuit.extension_snoc line 592
  88. lemma OAI.SourceBurnside.Tableau.Circuit.Extension.wire line 597
  89. theorem OAI.SourceBurnside.Tableau.Circuit.compile_formula line 603
  90. theorem OAI.SourceBurnside.Tableau.Circuit.compile_outputs line 625
  91. theorem OAI.SourceBurnside.Tableau.exists_nand_circuit line 648