OAI/Computability/PerfectCompleteness/Machines/SignedTupleBodyMachine.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SignedTupleBodyMachine.Tape line 18
  2. inductive OAI.PerfectCompleteness.SignedTupleBodyMachine.BodyLabel line 20
  3. structure OAI.PerfectCompleteness.SignedTupleBodyMachine.Data line 29
  4. def OAI.PerfectCompleteness.SignedTupleBodyMachine.tapes line 48
  5. def OAI.PerfectCompleteness.SignedTupleBodyMachine.next line 59
  6. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.finalTapes_eq line 68
  7. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.tapes_frame line 98
  8. abbrev OAI.PerfectCompleteness.SignedTupleBodyMachine.StageLabel line 107
  9. abbrev OAI.PerfectCompleteness.SignedTupleBodyMachine.LocalLabel line 108
  10. abbrev OAI.PerfectCompleteness.SignedTupleBodyMachine.Label line 109
  11. abbrev OAI.PerfectCompleteness.SignedTupleBodyMachine.State line 111
  12. abbrev OAI.PerfectCompleteness.SignedTupleBodyMachine.BodyState line 113
  13. def OAI.PerfectCompleteness.SignedTupleBodyMachine.localMain line 117
  14. def OAI.PerfectCompleteness.SignedTupleBodyMachine.localInstruction line 119
  15. def OAI.PerfectCompleteness.SignedTupleBodyMachine.instruction line 128
  16. def OAI.PerfectCompleteness.SignedTupleBodyMachine.entry line 139
  17. def OAI.PerfectCompleteness.SignedTupleBodyMachine.result line 144
  18. def OAI.PerfectCompleteness.SignedTupleBodyMachine.budget line 150
  19. def OAI.PerfectCompleteness.SignedTupleBodyMachine.sequenceInTime line 161
  20. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.result_count line 238
  21. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.result_leftKeys line 248
  22. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.result_rightKeys line 258
  23. def OAI.PerfectCompleteness.SignedTupleBodyMachine.blocks line 268
  24. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.result_output line 276
  25. def OAI.PerfectCompleteness.SignedTupleBodyMachine.allStages line 287
  26. def OAI.PerfectCompleteness.SignedTupleBodyMachine.tupleResult line 289
  27. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.bodyBudgetOrder line 295
  28. def OAI.PerfectCompleteness.SignedTupleBodyMachine.bodyMain line 308
  29. def OAI.PerfectCompleteness.SignedTupleBodyMachine.bodySigns line 310
  30. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.bodySigns_prepared line 314
  31. def OAI.PerfectCompleteness.SignedTupleBodyMachine.bodyExit line 320
  32. def OAI.PerfectCompleteness.SignedTupleBodyMachine.cleanupEntry line 325
  33. def OAI.PerfectCompleteness.SignedTupleBodyMachine.edgesEntry line 328
  34. def OAI.PerfectCompleteness.SignedTupleBodyMachine.bodyInstruction line 332
  35. def OAI.PerfectCompleteness.SignedTupleBodyMachine.nativeProgram line 347
  36. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.tapes_input line 350
  37. theorem OAI.PerfectCompleteness.SignedTupleBodyMachine.prepared_tapes_commute line 378
  38. def OAI.PerfectCompleteness.SignedTupleBodyMachine.bodyBudget line 394
  39. def OAI.PerfectCompleteness.SignedTupleBodyMachine.bodyInTime line 404