OAI/Combinatorics/MatchingCount/Tapes/OnlineStackCompiler.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.OnlineStack.Alpha line 15
  2. abbrev OAI.MatchingFPRAS.OnlineStack.L1 line 16
  3. abbrev OAI.MatchingFPRAS.OnlineStack.L2 line 17
  4. abbrev OAI.MatchingFPRAS.OnlineStack.Q line 18
  5. def OAI.MatchingFPRAS.OnlineStack.height line 20
  6. lemma OAI.MatchingFPRAS.OnlineStack.height_bound line 22
  7. def OAI.MatchingFPRAS.OnlineStack.stackCfg line 24
  8. lemma OAI.MatchingFPRAS.OnlineStack.stackCfg_spec line 28
  9. lemma OAI.MatchingFPRAS.OnlineStack.stackCfg_unique line 38
  10. def OAI.MatchingFPRAS.OnlineStack.program1 line 48
  11. def OAI.MatchingFPRAS.OnlineStack.enc line 49
  12. def OAI.MatchingFPRAS.OnlineStack.dec line 50
  13. lemma OAI.MatchingFPRAS.OnlineStack.enc0 line 51
  14. lemma OAI.MatchingFPRAS.OnlineStack.encdec line 53
  15. def OAI.MatchingFPRAS.OnlineStack.program2 line 54
  16. def OAI.MatchingFPRAS.OnlineStack.support1 line 55
  17. def OAI.MatchingFPRAS.OnlineStack.support2 line 56
  18. def OAI.MatchingFPRAS.OnlineStack.coin2 line 57
  19. def OAI.MatchingFPRAS.OnlineStack.table line 58
  20. def OAI.MatchingFPRAS.OnlineStack.states line 59
  21. lemma OAI.MatchingFPRAS.OnlineStack.supports1 line 61
  22. lemma OAI.MatchingFPRAS.OnlineStack.supports2 line 64
  23. lemma OAI.MatchingFPRAS.OnlineStack.coin2_supported line 67
  24. lemma OAI.MatchingFPRAS.OnlineStack.table_supported line 71
  25. def OAI.MatchingFPRAS.OnlineStack.cfg line 73
  26. def OAI.MatchingFPRAS.OnlineStack.accesses line 76
  27. lemma OAI.MatchingFPRAS.OnlineStack.accesses_bound line 79
  28. def OAI.MatchingFPRAS.OnlineStack.overhead line 81
  29. theorem OAI.MatchingFPRAS.OnlineStack.deterministic line 85
  30. lemma OAI.MatchingFPRAS.OnlineStack.random line 114
  31. def OAI.MatchingFPRAS.OnlineStack.initialState line 120
  32. lemma OAI.MatchingFPRAS.OnlineStack.initialState_mem line 122
  33. def OAI.MatchingFPRAS.OnlineStack.machine line 128