OAI/Computability/MeanPayoff/StackSimulation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.ForestMachine.scratch_clear line 12
  2. theorem OAI.MeanPayoff.ForestMachine.boundary_contract line 16
  3. theorem OAI.MeanPayoff.ForestMachine.one_step line 62
  4. def OAI.MeanPayoff.ForestMachine.size line 75
  5. theorem OAI.MeanPayoff.ForestMachine.member_size line 77
  6. theorem OAI.MeanPayoff.ForestMachine.blockBound_le line 82
  7. def OAI.MeanPayoff.ForestMachine.clock line 95
  8. theorem OAI.MeanPayoff.ForestMachine.clock_pos line 100
  9. theorem OAI.MeanPayoff.ForestMachine.clock_bound line 103
  10. theorem OAI.MeanPayoff.ForestMachine.clock_simulation line 115
  11. def OAI.MeanPayoff.ForestMachine.Safe line 127
  12. def OAI.MeanPayoff.ForestMachine.tree line 132
  13. def OAI.MeanPayoff.ForestMachine.schedule line 136
  14. theorem OAI.MeanPayoff.ForestMachine.schedule_expect line 141
  15. theorem OAI.MeanPayoff.ForestMachine.schedule_all line 147
  16. theorem OAI.MeanPayoff.ForestMachine.schedule_depth line 153
  17. theorem OAI.MeanPayoff.ForestMachine.consume_step line 167
  18. theorem OAI.MeanPayoff.ForestMachine.consume_simulation line 176
  19. theorem OAI.MeanPayoff.ForestMachine.embed_halted line 195
  20. theorem OAI.MeanPayoff.ForestMachine.padded_run line 198
  21. def OAI.MeanPayoff.SourceControl.trialCredit line 217
  22. def OAI.MeanPayoff.SourceControl.askCredit line 218
  23. def OAI.MeanPayoff.SourceControl.exceptionCredit line 219
  24. def OAI.MeanPayoff.SourceControl.updateCredit line 220
  25. def OAI.MeanPayoff.SourceControl.centersCredit line 221
  26. def OAI.MeanPayoff.SourceControl.orientUnit line 222
  27. def OAI.MeanPayoff.SourceControl.orientCredit line 223
  28. def OAI.MeanPayoff.SourceControl.orientTrialsCredit line 224
  29. def OAI.MeanPayoff.SourceControl.orientPlusCredit line 225
  30. def OAI.MeanPayoff.SourceControl.tightenUnit line 226
  31. def OAI.MeanPayoff.SourceControl.tightenCredit line 227
  32. def OAI.MeanPayoff.SourceControl.reweightCredit line 229
  33. def OAI.MeanPayoff.SourceControl.Result.credit line 231
  34. def OAI.MeanPayoff.SourceControl.Job.credit line 237
  35. def OAI.MeanPayoff.SourceControl.Frame.credit line 249
  36. def OAI.MeanPayoff.SourceControl.Kont.credit line 268
  37. def OAI.MeanPayoff.SourceControl.State.credit line 272
  38. def OAI.MeanPayoff.SourceControl.State.halted line 276
  39. def OAI.MeanPayoff.SourceControl.controlAllowance line 280
  40. theorem OAI.MeanPayoff.SourceControl.orientCredit_mono line 284
  41. theorem OAI.MeanPayoff.SourceControl.orientPlusCredit_mono line 288
  42. theorem OAI.MeanPayoff.SourceControl.orientBase_credit line 294
  43. theorem OAI.MeanPayoff.SourceControl.resume_credit line 299
  44. theorem OAI.MeanPayoff.SourceControl.step_credit line 356