OAI/Computability/MeanPayoff/RecursiveExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.Label.downOracle line 7
  2. def OAI.MeanPayoff.Label.upOracle line 12
  3. def OAI.MeanPayoff.Label.provisionalLabels line 17
  4. def OAI.MeanPayoff.Label.continuationLabels line 23
  5. theorem OAI.MeanPayoff.Label.labeller_base line 29
  6. theorem OAI.MeanPayoff.Label.labeller_small line 34
  7. theorem OAI.MeanPayoff.Label.labeller_step line 41
  8. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.branchFactor line 55
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.call_exec line 57