OAI/Computability/MeanPayoff/ArithmeticBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.RandomTree.maximum line 9
  2. theorem OAI.MeanPayoff.RandomTree.maximum_le_iff line 13
  3. theorem OAI.MeanPayoff.RandomTree.all_le_maximum line 19
  4. theorem OAI.MeanPayoff.RandomTree.maximum_add line 22
  5. theorem OAI.MeanPayoff.RandomTree.not_all_false line 28
  6. def OAI.MeanPayoff.Counted.maximum line 36
  7. theorem OAI.MeanPayoff.Counted.maximum_le_iff line 38
  8. theorem OAI.MeanPayoff.Counted.maximum_bind line 41
  9. def OAI.MeanPayoff.SourceControl.State.rank line 53
  10. theorem OAI.MeanPayoff.SourceControl.step_rank line 56
  11. def OAI.MeanPayoff.SourceControl.run line 68
  12. theorem OAI.MeanPayoff.SourceControl.run_halted line 72
  13. theorem OAI.MeanPayoff.SourceControl.run_halts line 84
  14. theorem OAI.MeanPayoff.SourceControl.run_denote line 102
  15. theorem OAI.MeanPayoff.SourceControl.run_solve_halts line 108
  16. theorem OAI.MeanPayoff.SourceControl.affine_power line 121
  17. theorem OAI.MeanPayoff.SourceControl.controlAllowance_scale line 129
  18. def OAI.MeanPayoff.SourceControl.rootControlBound line 173
  19. theorem OAI.MeanPayoff.SourceControl.rootControlBound_nat line 176
  20. theorem OAI.MeanPayoff.SourceControl.root_operational_halts line 199
  21. inductive OAI.MeanPayoff.WorkStack.RegisterCompile.Label line 207
  22. def OAI.MeanPayoff.WorkStack.RegisterCompile.equiv line 214
  23. def OAI.MeanPayoff.WorkStack.RegisterCompile.enc line 216
  24. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.decode line 217
  25. def OAI.MeanPayoff.WorkStack.RegisterCompile.program line 220
  26. def OAI.MeanPayoff.WorkStack.RegisterCompile.lift line 237
  27. def OAI.MeanPayoff.WorkStack.RegisterCompile.state line 241
  28. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.read0 line 244
  29. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.read1 line 250
  30. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.read2 line 256
  31. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.put_step line 262
  32. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.put_stop line 271
  33. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.six_steps line 278
  34. theorem OAI.MeanPayoff.WorkStack.RegisterCompile.advance_six line 301