OAI/Computability/MeanPayoff/BitProgram.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MeanPayoff.BinaryStack.Op line 10
  2. structure OAI.MeanPayoff.BinaryStack.Act line 14
  3. structure OAI.MeanPayoff.BinaryStack.Program line 19
  4. structure OAI.MeanPayoff.BinaryStack.Config line 24
  5. def OAI.MeanPayoff.BinaryStack.applyOp line 29
  6. def OAI.MeanPayoff.BinaryStack.shiftOp line 34
  7. def OAI.MeanPayoff.BinaryStack.firstWrite line 40
  8. def OAI.MeanPayoff.BinaryStack.pendingWrite line 44
  9. def OAI.MeanPayoff.BinaryStack.step line 48
  10. def OAI.MeanPayoff.BinaryStack.initial line 58
  11. def OAI.MeanPayoff.BinaryStack.run line 61
  12. def OAI.MeanPayoff.BinaryStack.cells line 65
  13. theorem OAI.MeanPayoff.BinaryStack.cells_top line 68
  14. theorem OAI.MeanPayoff.BinaryStack.cells_nil line 71
  15. theorem OAI.MeanPayoff.BinaryStack.cells_push line 74
  16. theorem OAI.MeanPayoff.BinaryStack.cells_pop line 87
  17. theorem OAI.MeanPayoff.BinaryStack.cells_emit line 99
  18. abbrev OAI.MeanPayoff.BinaryStack.Control line 115
  19. def OAI.MeanPayoff.BinaryStack.controlEquiv line 117
  20. def OAI.MeanPayoff.BinaryStack.normal line 120
  21. def OAI.MeanPayoff.BinaryStack.pending line 123
  22. def OAI.MeanPayoff.BinaryStack.machine line 126
  23. def OAI.MeanPayoff.BinaryStack.concrete line 147
  24. theorem OAI.MeanPayoff.BinaryStack.cells_end line 153
  25. theorem OAI.MeanPayoff.BinaryStack.cells_applyOp line 156
  26. def OAI.MeanPayoff.BinaryStack.newHeads line 175
  27. theorem OAI.MeanPayoff.BinaryStack.concrete_ext line 178
  28. theorem OAI.MeanPayoff.BinaryStack.decode_normal line 182
  29. theorem OAI.MeanPayoff.BinaryStack.decode_pending line 185
  30. theorem OAI.MeanPayoff.BinaryStack.shiftOp_formula line 189
  31. theorem OAI.MeanPayoff.BinaryStack.double_step line 196
  32. theorem OAI.MeanPayoff.BinaryStack.concrete_initial line 252
  33. theorem OAI.MeanPayoff.BinaryStack.simulate line 263
  34. theorem OAI.MeanPayoff.BinaryStack.concrete_halted line 275
  35. theorem OAI.MeanPayoff.BinaryStack.concrete_output line 280
  36. theorem OAI.MeanPayoff.BinaryStack.cells_ofFn line 283
  37. theorem OAI.MeanPayoff.BinaryStack.cells_outside line 287
  38. theorem OAI.MeanPayoff.BinaryStack.concrete_correct line 293