OAI/Combinatorics/MatchingCount/Tapes/TapeTools.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_head line 10
  2. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_right line 11
  3. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_left line 14
  4. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_write line 17
  5. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_left_nil line 20
  6. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_right_nil line 23
  7. lemma OAI.MatchingFPRAS.LiteralTape.mk₂_write_nil line 26
  8. lemma OAI.MatchingFPRAS.LiteralTape.blank_zero line 29
  9. lemma OAI.MatchingFPRAS.LiteralTape.blank_append_zero line 33
  10. def OAI.MatchingFPRAS.LiteralTape.Exec line 39
  11. lemma OAI.MatchingFPRAS.LiteralTape.Exec.refl line 41
  12. lemma OAI.MatchingFPRAS.LiteralTape.Exec.step line 42
  13. lemma OAI.MatchingFPRAS.LiteralTape.Exec.trans line 44
  14. lemma OAI.MatchingFPRAS.LiteralTape.Exec.mono line 49
  15. def OAI.MatchingFPRAS.LiteralTape.select line 53
  16. lemma OAI.MatchingFPRAS.LiteralTape.select_step line 56
  17. def OAI.MatchingFPRAS.LiteralTape.writeLeft line 69
  18. lemma OAI.MatchingFPRAS.LiteralTape.writeLeft_step line 71
  19. def OAI.MatchingFPRAS.LiteralTape.eraseToLeft line 81
  20. lemma OAI.MatchingFPRAS.LiteralTape.eraseToLeft_step line 83
  21. def OAI.MatchingFPRAS.LiteralTape.grab line 94
  22. lemma OAI.MatchingFPRAS.LiteralTape.grab_step line 96
  23. lemma OAI.MatchingFPRAS.LiteralTape.fold_updates line 107
  24. lemma OAI.MatchingFPRAS.LiteralTape.grab_fin line 114