OAI/Computability/MeanPayoff/SignedBits.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.WorkStack.Addition.finiteProgram line 11
  2. def OAI.MeanPayoff.WorkStack.Addition.label line 25
  3. def OAI.MeanPayoff.WorkStack.Addition.feed line 27
  4. def OAI.MeanPayoff.WorkStack.Addition.transfer line 29
  5. def OAI.MeanPayoff.WorkStack.Addition.stopped line 31
  6. theorem OAI.MeanPayoff.WorkStack.Addition.step_feed_nil line 34
  7. theorem OAI.MeanPayoff.WorkStack.Addition.step_feed_left line 40
  8. theorem OAI.MeanPayoff.WorkStack.Addition.step_feed_right line 46
  9. theorem OAI.MeanPayoff.WorkStack.Addition.step_feed_both line 52
  10. theorem OAI.MeanPayoff.WorkStack.Addition.step_transfer_cons line 58
  11. theorem OAI.MeanPayoff.WorkStack.Addition.step_transfer_nil line 64
  12. theorem OAI.MeanPayoff.WorkStack.Addition.feed_adds line 67
  13. theorem OAI.MeanPayoff.WorkStack.Addition.transfer_runs line 91
  14. theorem OAI.MeanPayoff.WorkStack.Addition.add_length line 101
  15. theorem OAI.MeanPayoff.WorkStack.Addition.program_adds_exact line 126
  16. theorem OAI.MeanPayoff.WorkStack.Addition.program_adds_bounded line 136
  17. theorem OAI.MeanPayoff.WorkStack.Addition.result_value line 147
  18. def OAI.MeanPayoff.WorkStack.Computes line 158
  19. abbrev OAI.MeanPayoff.WorkStack.Sequence.Labels line 164
  20. def OAI.MeanPayoff.WorkStack.Sequence.equiv line 165
  21. def OAI.MeanPayoff.WorkStack.Sequence.lhs line 167
  22. def OAI.MeanPayoff.WorkStack.Sequence.rhs line 168
  23. def OAI.MeanPayoff.WorkStack.Sequence.program line 170
  24. def OAI.MeanPayoff.WorkStack.Sequence.left line 181
  25. def OAI.MeanPayoff.WorkStack.Sequence.right line 183
  26. theorem OAI.MeanPayoff.WorkStack.Sequence.decode_lhs line 186
  27. theorem OAI.MeanPayoff.WorkStack.Sequence.decode_rhs line 188
  28. theorem OAI.MeanPayoff.WorkStack.Sequence.step_left line 191
  29. theorem OAI.MeanPayoff.WorkStack.Sequence.step_right line 200
  30. theorem OAI.MeanPayoff.WorkStack.Sequence.advance_left line 209
  31. theorem OAI.MeanPayoff.WorkStack.Sequence.advance_right line 218
  32. theorem OAI.MeanPayoff.WorkStack.first_termination line 226
  33. theorem OAI.MeanPayoff.WorkStack.Computes.sequence line 240
  34. structure OAI.MeanPayoff.SignedBits.Word line 262
  35. def OAI.MeanPayoff.SignedBits.Word.val line 267
  36. def OAI.MeanPayoff.SignedBits.cons line 269
  37. def OAI.MeanPayoff.SignedBits.head line 271
  38. theorem OAI.MeanPayoff.SignedBits.val_cons line 273
  39. theorem OAI.MeanPayoff.SignedBits.val_uncons line 279
  40. def OAI.MeanPayoff.SignedBits.finalSign line 285
  41. def OAI.MeanPayoff.SignedBits.add line 287
  42. theorem OAI.MeanPayoff.SignedBits.add_val line 294
  43. theorem OAI.MeanPayoff.SignedBits.add_length line 333
  44. theorem OAI.MeanPayoff.SignedBits.value_bound line 358
  45. theorem OAI.MeanPayoff.SignedBits.val_negative line 364