OAI/Computability/PerfectCompleteness/Machines/BinaryValidatorMachine.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.BinaryValidatorMachine.Mode line 13
  2. def OAI.PerfectCompleteness.BinaryValidatorMachine.afterName line 22
  3. def OAI.PerfectCompleteness.BinaryValidatorMachine.nextMode line 25
  4. def OAI.PerfectCompleteness.BinaryValidatorMachine.run line 35
  5. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_reject line 39
  6. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_done_iff line 44
  7. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.finalDigit_true_iff line 49
  8. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_frame line 66
  9. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_name line 78
  10. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_literal line 83
  11. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_clause line 88
  12. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_clauses line 92
  13. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_formula line 99
  14. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.frame_inverse line 102
  15. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.name_inverse line 132
  16. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.literal_inverse line 141
  17. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.clause_inverse line 152
  18. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.clauses_inverse_aux line 165
  19. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.run_clause_iff line 192
  20. def OAI.PerfectCompleteness.BinaryValidatorMachine.accepts line 202
  21. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.accepts_eq_decode line 204
  22. abbrev OAI.PerfectCompleteness.BinaryValidatorMachine.Alphabet line 224
  23. abbrev OAI.PerfectCompleteness.BinaryValidatorMachine.State line 225
  24. def OAI.PerfectCompleteness.BinaryValidatorMachine.instruction line 227
  25. abbrev OAI.PerfectCompleteness.BinaryValidatorMachine.machine line 235
  26. def OAI.PerfectCompleteness.BinaryValidatorMachine.tapes line 246
  27. def OAI.PerfectCompleteness.BinaryValidatorMachine.cfg line 250
  28. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.tapes_input line 254
  29. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.tapes_output line 257
  30. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.update_input line 260
  31. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.update_output line 265
  32. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.step_empty line 270
  33. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.step_cons line 277
  34. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.runTrace line 285
  35. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.initList_eq line 299
  36. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.haltList_eq line 306
  37. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.validatorTrace line 313
  38. def OAI.PerfectCompleteness.BinaryValidatorMachine.outputsInTime line 325
  39. def OAI.PerfectCompleteness.BinaryValidatorMachine.computableInPolyTime line 332
  40. theorem OAI.PerfectCompleteness.BinaryValidatorMachine.machine_finiteAlphabet line 346