OAI/Computability/DepthThree/MachineFiniteRestriction.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.Label line 13
  2. instance OAI.DepthThreeLowerBound.MachineFiniteRestriction.labelInhabited line 20
  3. instance OAI.DepthThreeLowerBound.MachineFiniteRestriction.labelFintype line 23
  4. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.retract line 26
  5. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.retract_val line 30
  6. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.retract_default line 46
  7. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.idAlphabet line 51
  8. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.listBlank_map_id line 53
  9. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.tape_map_id line 60
  10. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict line 68
  11. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrictCfg line 71
  12. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.includeCfg line 74
  13. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.include_restrict line 77
  14. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict_include line 83
  15. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.includeCfg_injective line 91
  16. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.cfg_map_eq line 96
  17. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict_step line 104
  18. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.include_step line 115
  19. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict_init line 127
  20. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.include_init line 131
  21. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.include_runSteps line 134
  22. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict_runSteps line 145
  23. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.runSteps_supports line 162
  24. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict_runsIn line 181
  25. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.include_runsIn_iff line 190
  26. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.restrict_halt_iff line 205
  27. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.include_halt_iff line 211
  28. def OAI.DepthThreeLowerBound.MachineFiniteRestriction.toFiniteMachine line 221
  29. theorem OAI.DepthThreeLowerBound.MachineFiniteRestriction.toFiniteMachine_haltsIn_iff line 234