OAI/Computability/MeanPayoff/Comparison.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.ArithmeticForest.placeA line 12
  2. def OAI.MeanPayoff.ArithmeticForest.placeB line 13
  3. def OAI.MeanPayoff.ArithmeticForest.placeAdd line 14
  4. def OAI.MeanPayoff.ArithmeticForest.placeBox line 15
  5. theorem OAI.MeanPayoff.ArithmeticForest.injectA line 17
  6. theorem OAI.MeanPayoff.ArithmeticForest.injectB line 18
  7. theorem OAI.MeanPayoff.ArithmeticForest.injectAdd line 19
  8. theorem OAI.MeanPayoff.ArithmeticForest.injectBox line 20
  9. theorem OAI.MeanPayoff.ArithmeticForest.installA line 22
  10. theorem OAI.MeanPayoff.ArithmeticForest.installB line 31
  11. theorem OAI.MeanPayoff.ArithmeticForest.installAdd line 40
  12. theorem OAI.MeanPayoff.ArithmeticForest.installBox line 49
  13. abbrev OAI.MeanPayoff.ArithmeticForest.flow line 58
  14. def OAI.MeanPayoff.ArithmeticForest.program line 73
  15. def OAI.MeanPayoff.ArithmeticForest.unboxTime line 75
  16. def OAI.MeanPayoff.ArithmeticForest.addTime line 76
  17. def OAI.MeanPayoff.ArithmeticForest.boxTime line 77
  18. def OAI.MeanPayoff.ArithmeticForest.addWord line 79
  19. def OAI.MeanPayoff.ArithmeticForest.store0 line 81
  20. def OAI.MeanPayoff.ArithmeticForest.store1 line 83
  21. def OAI.MeanPayoff.ArithmeticForest.store2 line 85
  22. def OAI.MeanPayoff.ArithmeticForest.store3 line 87
  23. def OAI.MeanPayoff.ArithmeticForest.store4 line 89
  24. theorem OAI.MeanPayoff.ArithmeticForest.stage0 line 92
  25. theorem OAI.MeanPayoff.ArithmeticForest.stage1 line 105
  26. theorem OAI.MeanPayoff.ArithmeticForest.stage2 line 116
  27. theorem OAI.MeanPayoff.ArithmeticForest.stage3 line 129
  28. theorem OAI.MeanPayoff.ArithmeticForest.addWord_val line 148
  29. theorem OAI.MeanPayoff.ArithmeticForest.total_bound line 153
  30. theorem OAI.MeanPayoff.ArithmeticForest.program_adds line 167
  31. def OAI.MeanPayoff.SignedBits.compareBit line 191
  32. def OAI.MeanPayoff.SignedBits.compare line 193
  33. theorem OAI.MeanPayoff.SignedBits.compare_bit_correct line 200
  34. theorem OAI.MeanPayoff.SignedBits.compare_correct line 206
  35. theorem OAI.MeanPayoff.SignedBits.compare_lt line 238
  36. inductive OAI.MeanPayoff.WorkStack.SignedCompare.Label line 245
  37. def OAI.MeanPayoff.WorkStack.SignedCompare.equiv line 250
  38. def OAI.MeanPayoff.WorkStack.SignedCompare.enc line 251
  39. theorem OAI.MeanPayoff.WorkStack.SignedCompare.decode line 252
  40. def OAI.MeanPayoff.WorkStack.SignedCompare.program line 254
  41. def OAI.MeanPayoff.WorkStack.SignedCompare.state line 264
  42. def OAI.MeanPayoff.WorkStack.SignedCompare.stopped line 266
  43. theorem OAI.MeanPayoff.WorkStack.SignedCompare.step_start line 268
  44. theorem OAI.MeanPayoff.WorkStack.SignedCompare.step_nil line 274
  45. theorem OAI.MeanPayoff.WorkStack.SignedCompare.step_left line 280
  46. theorem OAI.MeanPayoff.WorkStack.SignedCompare.step_right line 286
  47. theorem OAI.MeanPayoff.WorkStack.SignedCompare.step_both line 292
  48. theorem OAI.MeanPayoff.WorkStack.SignedCompare.step_halt line 298
  49. theorem OAI.MeanPayoff.WorkStack.SignedCompare.feed_runs line 302
  50. theorem OAI.MeanPayoff.WorkStack.SignedCompare.program_compares line 325
  51. theorem OAI.MeanPayoff.WorkStack.SignedCompare.output_correct line 332