OAI/Computability/PerfectCompleteness/Foundations/CutTerminalSplit.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CutTerminalSplit.refinedSpace_eq_terminal line 23
  2. abbrev OAI.PerfectCompleteness.CutTerminalSplit.TerminalFactor line 40
  3. abbrev OAI.PerfectCompleteness.CutTerminalSplit.TerminalTape line 43
  4. abbrev OAI.PerfectCompleteness.CutTerminalSplit.ExteriorIndex line 45
  5. abbrev OAI.PerfectCompleteness.CutTerminalSplit.ExteriorTape line 47
  6. def OAI.PerfectCompleteness.CutTerminalSplit.terminalFactorEquiv line 50
  7. def OAI.PerfectCompleteness.CutTerminalSplit.terminalTapeEquiv line 55
  8. def OAI.PerfectCompleteness.CutTerminalSplit.splitTape line 65
  9. theorem OAI.PerfectCompleteness.CutTerminalSplit.splitTape_terminal_apply line 72
  10. theorem OAI.PerfectCompleteness.CutTerminalSplit.splitTape_exterior_apply line 77
  11. instance OAI.PerfectCompleteness.CutTerminalSplit.childSquareFintype line 83
  12. def OAI.PerfectCompleteness.CutTerminalSplit.terminalLaw line 87
  13. def OAI.PerfectCompleteness.CutTerminalSplit.exteriorLaw line 93
  14. theorem OAI.PerfectCompleteness.CutTerminalSplit.terminalLaw_uniform line 97
  15. theorem OAI.PerfectCompleteness.CutTerminalSplit.exteriorLaw_uniform line 101
  16. theorem OAI.PerfectCompleteness.CutTerminalSplit.split_tapeLaw line 105
  17. theorem OAI.PerfectCompleteness.CutTerminalSplit.terminal_marginal line 119
  18. theorem OAI.PerfectCompleteness.CutTerminalSplit.terminal_marginal_uniform line 127