OAI/Computability/MeanPayoff/Arithmetic.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MeanPayoff.WorkStack.SignedAddition.Label line 11
  2. def OAI.MeanPayoff.WorkStack.SignedAddition.equiv line 18
  3. def OAI.MeanPayoff.WorkStack.SignedAddition.enc line 19
  4. theorem OAI.MeanPayoff.WorkStack.SignedAddition.decode line 20
  5. def OAI.MeanPayoff.WorkStack.SignedAddition.program line 22
  6. def OAI.MeanPayoff.WorkStack.SignedAddition.state line 41
  7. def OAI.MeanPayoff.WorkStack.SignedAddition.stopped line 43
  8. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_start line 45
  9. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_feed_nil line 52
  10. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_feed_left line 60
  11. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_feed_right line 68
  12. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_feed_both line 76
  13. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_transfer_cons line 84
  14. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_transfer_nil line 91
  15. theorem OAI.MeanPayoff.WorkStack.SignedAddition.step_halt line 98
  16. theorem OAI.MeanPayoff.WorkStack.SignedAddition.feed_runs line 102
  17. theorem OAI.MeanPayoff.WorkStack.SignedAddition.transfer_runs line 129
  18. theorem OAI.MeanPayoff.WorkStack.SignedAddition.program_adds line 139
  19. def OAI.MeanPayoff.MachineRun.advance line 159
  20. theorem OAI.MeanPayoff.MachineRun.advance_zero line 163
  21. theorem OAI.MeanPayoff.MachineRun.advance_front line 166
  22. theorem OAI.MeanPayoff.MachineRun.advance_add line 172
  23. theorem OAI.MeanPayoff.MachineRun.advance_initial line 178
  24. theorem OAI.MeanPayoff.MachineRun.advance_halted line 184
  25. theorem OAI.MeanPayoff.MachineRun.first_termination line 190
  26. abbrev OAI.MeanPayoff.MachineRun.Sequence.Labels line 203
  27. def OAI.MeanPayoff.MachineRun.Sequence.equiv line 204
  28. def OAI.MeanPayoff.MachineRun.Sequence.lhs line 206
  29. def OAI.MeanPayoff.MachineRun.Sequence.rhs line 207
  30. def OAI.MeanPayoff.MachineRun.Sequence.machine line 209
  31. def OAI.MeanPayoff.MachineRun.Sequence.left line 220
  32. def OAI.MeanPayoff.MachineRun.Sequence.restart line 222
  33. def OAI.MeanPayoff.MachineRun.Sequence.right line 224
  34. theorem OAI.MeanPayoff.MachineRun.Sequence.decode_lhs line 227
  35. theorem OAI.MeanPayoff.MachineRun.Sequence.decode_rhs line 229
  36. theorem OAI.MeanPayoff.MachineRun.Sequence.step_left line 232
  37. theorem OAI.MeanPayoff.MachineRun.Sequence.step_right line 247
  38. theorem OAI.MeanPayoff.MachineRun.Sequence.advance_left line 256
  39. theorem OAI.MeanPayoff.MachineRun.Sequence.advance_right line 263
  40. theorem OAI.MeanPayoff.MachineRun.Sequence.left_initial line 269
  41. theorem OAI.MeanPayoff.MachineRun.Sequence.run_after_first_halt line 272