OAI/Combinatorics/MatchingCount/Machines/OnlineControl.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MatchingFPRAS.OnlineControl.Instr line 11
  2. def OAI.MatchingFPRAS.OnlineControl.procedure line 17
  3. def OAI.MatchingFPRAS.OnlineControl.successor line 20
  4. abbrev OAI.MatchingFPRAS.OnlineControl.Label line 23
  5. instance OAI.MatchingFPRAS.OnlineControl.(instance at line 24) line 24
  6. def OAI.MatchingFPRAS.OnlineControl.code line 26
  7. def OAI.MatchingFPRAS.OnlineControl.coins line 36
  8. def OAI.MatchingFPRAS.OnlineControl.compile line 39
  9. def OAI.MatchingFPRAS.OnlineControl.cfg line 41
  10. def OAI.MatchingFPRAS.OnlineControl.At line 43
  11. lemma OAI.MatchingFPRAS.OnlineControl.done line 46
  12. lemma OAI.MatchingFPRAS.OnlineControl.halt line 48
  13. lemma OAI.MatchingFPRAS.OnlineControl.go line 52
  14. lemma OAI.MatchingFPRAS.OnlineControl.nilBranch line 57
  15. lemma OAI.MatchingFPRAS.OnlineControl.consBranch line 64
  16. lemma OAI.MatchingFPRAS.OnlineControl.call line 72
  17. lemma OAI.MatchingFPRAS.OnlineControl.deterministicCall line 90