OAI/Computability/PerfectCompleteness/Foundations/OriginalTerminalSplitLemmas.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.expansionSpace_terminal line 22
  2. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.expansionSpace_exterior line 34
  3. abbrev OAI.PerfectCompleteness.OriginalTerminalSplit.ExteriorIndex line 52
  4. abbrev OAI.PerfectCompleteness.OriginalTerminalSplit.ExteriorTape line 54
  5. abbrev OAI.PerfectCompleteness.OriginalTerminalSplit.TerminalTape line 56
  6. def OAI.PerfectCompleteness.OriginalTerminalSplit.terminalFactorEquiv line 59
  7. def OAI.PerfectCompleteness.OriginalTerminalSplit.exteriorFactorEquiv line 64
  8. def OAI.PerfectCompleteness.OriginalTerminalSplit.terminalTapeEquiv line 68
  9. def OAI.PerfectCompleteness.OriginalTerminalSplit.splitExpanded line 77
  10. def OAI.PerfectCompleteness.OriginalTerminalSplit.splitTape line 84
  11. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.splitExpanded_terminal_apply line 88
  12. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.splitExpanded_exterior_apply line 93
  13. def OAI.PerfectCompleteness.OriginalTerminalSplit.terminalLaw line 103
  14. def OAI.PerfectCompleteness.OriginalTerminalSplit.exteriorLaw line 107
  15. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.terminalLaw_uniform line 111
  16. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.exteriorLaw_uniform line 115
  17. theorem OAI.PerfectCompleteness.OriginalTerminalSplit.split_tapeLaw line 119
  18. abbrev OAI.PerfectCompleteness.OriginalScalarReconstruction.TerminalValues line 154
  19. def OAI.PerfectCompleteness.OriginalScalarReconstruction.terminalValueEquiv line 156
  20. def OAI.PerfectCompleteness.OriginalScalarReconstruction.prefixSplit line 165
  21. def OAI.PerfectCompleteness.OriginalScalarReconstruction.reconstruct line 170
  22. theorem OAI.PerfectCompleteness.OriginalScalarReconstruction.collapseFactor_terminal line 174
  23. theorem OAI.PerfectCompleteness.OriginalScalarReconstruction.collapseFactor_exterior line 188
  24. theorem OAI.PerfectCompleteness.OriginalScalarReconstruction.prefixSplit_collapseExpanded line 204
  25. theorem OAI.PerfectCompleteness.OriginalScalarReconstruction.reconstruct_original line 216