OAI/Computability/MeanPayoff/Simulation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.BinaryStack.advance line 9
  2. theorem OAI.MeanPayoff.BinaryStack.advance_front line 13
  3. theorem OAI.MeanPayoff.BinaryStack.advance_halted line 22
  4. theorem OAI.MeanPayoff.BinaryStack.Config.ext line 28
  5. def OAI.MeanPayoff.BinaryStack.Addition.value line 34
  6. def OAI.MeanPayoff.BinaryStack.Addition.low line 38
  7. def OAI.MeanPayoff.BinaryStack.Addition.carry line 39
  8. theorem OAI.MeanPayoff.BinaryStack.Addition.full_adder line 41
  9. def OAI.MeanPayoff.BinaryStack.Addition.add line 45
  10. theorem OAI.MeanPayoff.BinaryStack.Addition.add_value line 52
  11. def OAI.MeanPayoff.BinaryStack.Addition.label line 82
  12. def OAI.MeanPayoff.BinaryStack.Addition.finiteProgram line 86
  13. def OAI.MeanPayoff.BinaryStack.Addition.state line 98
  14. def OAI.MeanPayoff.BinaryStack.Addition.stopped line 101
  15. theorem OAI.MeanPayoff.BinaryStack.Addition.label_one line 104
  16. theorem OAI.MeanPayoff.BinaryStack.Addition.step_nil_false line 107
  17. theorem OAI.MeanPayoff.BinaryStack.Addition.step_nil_true line 114
  18. theorem OAI.MeanPayoff.BinaryStack.Addition.step_cons_left line 118
  19. theorem OAI.MeanPayoff.BinaryStack.Addition.step_cons_right line 124
  20. theorem OAI.MeanPayoff.BinaryStack.Addition.step_cons_both line 130
  21. theorem OAI.MeanPayoff.BinaryStack.Addition.program_adds line 136
  22. structure OAI.MeanPayoff.WorkStack.Act line 168
  23. structure OAI.MeanPayoff.WorkStack.Program line 172
  24. structure OAI.MeanPayoff.WorkStack.Config line 177
  25. theorem OAI.MeanPayoff.WorkStack.Config.ext line 181
  26. def OAI.MeanPayoff.WorkStack.step line 185
  27. def OAI.MeanPayoff.WorkStack.initial line 193
  28. def OAI.MeanPayoff.WorkStack.advance line 196
  29. def OAI.MeanPayoff.WorkStack.run line 200
  30. theorem OAI.MeanPayoff.WorkStack.advance_zero line 203
  31. theorem OAI.MeanPayoff.WorkStack.advance_front line 206
  32. theorem OAI.MeanPayoff.WorkStack.advance_add line 215
  33. theorem OAI.MeanPayoff.WorkStack.advance_halted line 224
  34. abbrev OAI.MeanPayoff.WorkStack.Control line 230
  35. def OAI.MeanPayoff.WorkStack.controlEquiv line 231
  36. def OAI.MeanPayoff.WorkStack.normal line 233
  37. def OAI.MeanPayoff.WorkStack.pending line 235
  38. def OAI.MeanPayoff.WorkStack.machine line 238
  39. def OAI.MeanPayoff.WorkStack.concrete line 253
  40. theorem OAI.MeanPayoff.WorkStack.decode_normal line 259
  41. theorem OAI.MeanPayoff.WorkStack.decode_pending line 261
  42. def OAI.MeanPayoff.WorkStack.newHeads line 264
  43. theorem OAI.MeanPayoff.WorkStack.double_step line 267
  44. theorem OAI.MeanPayoff.WorkStack.concrete_initial line 298
  45. theorem OAI.MeanPayoff.WorkStack.simulate line 306
  46. theorem OAI.MeanPayoff.WorkStack.concrete_halted line 317