OAI/Computability/RandomMean/StateGrowth.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.Small line 9
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.Small.mono line 18
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.zeroBudget_small line 20
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.zeroBox_small line 22
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.zeroOrient_small line 23
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.zero_small line 24
  7. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackSmall line 26
  8. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.StateSmall line 27
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackSmall.mono line 28
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackSmall.tail line 29
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackSmall.head line 30
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackSmall.cons line 34
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StateSmall.mono line 38
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.narrow_small line 39
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.wide_small line 43
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.capWidth_small line 47
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.centerAt_small line 54
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.lastPositive_small line 59
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.lastNegative_small line 65
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.basic_small line 71
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.job_small line 82
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.mask_head line 170
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.frame_small line 174
  24. def OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.listMass line 306
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.listMass_nil line 307
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.listMass_cons line 308
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.base_length line 309
  28. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.combine_length line 312
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.extend_length line 315
  30. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.mass line 320
  31. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackMass line 321
  32. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.stateMass line 322
  33. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackMass_nil line 323
  34. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackMass_cons line 324
  35. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.job_mass line 325
  36. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.frame_mass line 334