OAI/Combinatorics/MatchingCount/Machines/RegisterProc.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.RegisterProc.Store line 11
  2. abbrev OAI.MatchingFPRAS.RegisterProc.Stack line 12
  3. structure OAI.MatchingFPRAS.RegisterProc.Proc line 13
  4. def OAI.MatchingFPRAS.RegisterProc.Exec line 21
  5. lemma OAI.MatchingFPRAS.RegisterProc.Exec.mono line 23
  6. def OAI.MatchingFPRAS.RegisterProc.seq line 27
  7. lemma OAI.MatchingFPRAS.RegisterProc.Exec.seq line 31
  8. def OAI.MatchingFPRAS.RegisterProc.atom line 39
  9. lemma OAI.MatchingFPRAS.RegisterProc.exec_atom line 40
  10. def OAI.MatchingFPRAS.RegisterProc.reindex line 43
  11. def OAI.MatchingFPRAS.RegisterProc.frame line 45
  12. lemma OAI.MatchingFPRAS.RegisterProc.exec_reindex line 47
  13. def OAI.MatchingFPRAS.RegisterProc.triple line 58
  14. lemma OAI.MatchingFPRAS.RegisterProc.triple_zero line 61
  15. lemma OAI.MatchingFPRAS.RegisterProc.triple_one line 64
  16. lemma OAI.MatchingFPRAS.RegisterProc.triple_two line 67
  17. def OAI.MatchingFPRAS.RegisterProc.put3 line 70
  18. lemma OAI.MatchingFPRAS.RegisterProc.frame_triple line 72
  19. lemma OAI.MatchingFPRAS.RegisterProc.put3_same line 91
  20. def OAI.MatchingFPRAS.RegisterProc.clearRaw line 96
  21. def OAI.MatchingFPRAS.RegisterProc.reverseRaw line 97
  22. def OAI.MatchingFPRAS.RegisterProc.duplicateRaw line 98
  23. def OAI.MatchingFPRAS.RegisterProc.transferRaw line 99
  24. lemma OAI.MatchingFPRAS.RegisterProc.clearRaw_exec line 100
  25. lemma OAI.MatchingFPRAS.RegisterProc.reverseRaw_exec line 103
  26. lemma OAI.MatchingFPRAS.RegisterProc.duplicateRaw_exec line 106
  27. lemma OAI.MatchingFPRAS.RegisterProc.transferRaw_exec line 109