OAI/Combinatorics/MatchingCount/Machines/Wrapper.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.LiteralPhysical.pack line 13
  2. def OAI.MatchingFPRAS.LiteralPhysical.erase line 14
  3. def OAI.MatchingFPRAS.LiteralPhysical.unpack line 15
  4. def OAI.MatchingFPRAS.LiteralPhysical.post line 16
  5. def OAI.MatchingFPRAS.LiteralPhysical.packTime line 17
  6. def OAI.MatchingFPRAS.LiteralPhysical.eraseTime line 19
  7. def OAI.MatchingFPRAS.LiteralPhysical.unpackTime line 20
  8. def OAI.MatchingFPRAS.LiteralPhysical.postTime line 22
  9. lemma OAI.MatchingFPRAS.LiteralPhysical.packTime_mono line 23
  10. lemma OAI.MatchingFPRAS.LiteralPhysical.postTime_mono line 25
  11. lemma OAI.MatchingFPRAS.LiteralPhysical.pack_realizes line 27
  12. lemma OAI.MatchingFPRAS.LiteralPhysical.post_realizes line 30
  13. def OAI.MatchingFPRAS.LiteralPhysical.wrap line 42
  14. def OAI.MatchingFPRAS.LiteralPhysical.wrapTime line 44
  15. lemma OAI.MatchingFPRAS.LiteralPhysical.wrap_realizes line 46
  16. lemma OAI.MatchingFPRAS.LiteralPhysical.encodeNat_nonzero line 57
  17. lemma OAI.MatchingFPRAS.LiteralPhysical.encodeRat_nonzero line 62
  18. lemma OAI.MatchingFPRAS.LiteralPhysical.input_nonzero line 68
  19. lemma OAI.MatchingFPRAS.LiteralPhysical.natWord_alphabet line 77
  20. lemma OAI.MatchingFPRAS.LiteralPhysical.ratWord_alphabet line 82
  21. lemma OAI.MatchingFPRAS.LiteralPhysical.algorithm_alphabet line 88
  22. def OAI.MatchingFPRAS.LiteralPhysical.mainProgram line 92
  23. lemma OAI.MatchingFPRAS.LiteralPhysical.mainProgram_realizes line 93