OAI/Computability/PerfectCompleteness/Machines/UnaryBlockSkipMachine.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.UnaryBlockSkipMachine.Alphabet line 16
  2. abbrev OAI.PerfectCompleteness.UnaryBlockSkipMachine.State line 17
  3. def OAI.PerfectCompleteness.UnaryBlockSkipMachine.nextField line 23
  4. def OAI.PerfectCompleteness.UnaryBlockSkipMachine.finish line 27
  5. def OAI.PerfectCompleteness.UnaryBlockSkipMachine.instruction line 30
  6. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.step_true line 47
  7. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.step_false line 55
  8. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.step_empty line 64
  9. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.fieldTrace line 72
  10. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.joinTrace line 90
  11. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.fromTrace line 94
  12. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.listTrace line 132
  13. def OAI.PerfectCompleteness.UnaryBlockSkipMachine.listInTime line 144
  14. abbrev OAI.PerfectCompleteness.UnaryBlockSkipMachine.ConcreteLabel line 158
  15. def OAI.PerfectCompleteness.UnaryBlockSkipMachine.concreteProgram line 160
  16. abbrev OAI.PerfectCompleteness.UnaryBlockSkipMachine.machine line 166
  17. def OAI.PerfectCompleteness.UnaryBlockSkipMachine.machineInTime line 177
  18. theorem OAI.PerfectCompleteness.UnaryBlockSkipMachine.machine_finiteAlphabet line 187