OAI/Computability/BinPacking/Reductions/BinaryValidatorMachine.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingCompleteness.BinaryValidatorMachine.Mode line 10
  2. def OAI.BinPackingCompleteness.BinaryValidatorMachine.afterName line 19
  3. def OAI.BinPackingCompleteness.BinaryValidatorMachine.nextMode line 22
  4. def OAI.BinPackingCompleteness.BinaryValidatorMachine.run line 32
  5. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_reject line 36
  6. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_done_iff line 41
  7. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.finalDigit_true_iff line 46
  8. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_frame line 63
  9. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_name line 75
  10. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_literal line 80
  11. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_clause line 85
  12. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_clauses line 89
  13. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_formula line 96
  14. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.frame_inverse line 99
  15. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.name_inverse line 129
  16. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.literal_inverse line 138
  17. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.clause_inverse line 149
  18. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.clauses_inverse_aux line 162
  19. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.run_clause_iff line 189
  20. def OAI.BinPackingCompleteness.BinaryValidatorMachine.accepts line 199
  21. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.accepts_eq_decode line 201
  22. abbrev OAI.BinPackingCompleteness.BinaryValidatorMachine.Alphabet line 221
  23. abbrev OAI.BinPackingCompleteness.BinaryValidatorMachine.State line 222
  24. def OAI.BinPackingCompleteness.BinaryValidatorMachine.instruction line 224
  25. abbrev OAI.BinPackingCompleteness.BinaryValidatorMachine.machine line 232
  26. def OAI.BinPackingCompleteness.BinaryValidatorMachine.tapes line 243
  27. def OAI.BinPackingCompleteness.BinaryValidatorMachine.cfg line 247
  28. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.tapes_input line 251
  29. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.tapes_output line 254
  30. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.update_input line 257
  31. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.update_output line 262
  32. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.step_empty line 267
  33. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.step_cons line 274
  34. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.runTrace line 282
  35. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.initList_eq line 296
  36. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.haltList_eq line 303
  37. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.validatorTrace line 310
  38. def OAI.BinPackingCompleteness.BinaryValidatorMachine.outputsInTime line 322
  39. def OAI.BinPackingCompleteness.BinaryValidatorMachine.computableInPolyTime line 329
  40. theorem OAI.BinPackingCompleteness.BinaryValidatorMachine.machine_finiteAlphabet line 343