OAI/Combinatorics/MatchingCount/Machines/TreeMachine.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.RegisterProc.makeNil line 9
  2. lemma OAI.MatchingFPRAS.RegisterProc.makeNil_exec line 10
  3. lemma OAI.MatchingFPRAS.RegisterProc.exec_on line 20
  4. abbrev OAI.MatchingFPRAS.TreeMachine.K line 32
  5. abbrev OAI.MatchingFPRAS.TreeMachine.Env line 33
  6. def OAI.MatchingFPRAS.TreeMachine.encodeEnv line 35
  7. def OAI.MatchingFPRAS.TreeMachine.pairEmbedding line 38
  8. def OAI.MatchingFPRAS.TreeMachine.singleEmbedding line 40
  9. def OAI.MatchingFPRAS.TreeMachine.putPair line 43
  10. lemma OAI.MatchingFPRAS.TreeMachine.encode_putPair line 45
  11. lemma OAI.MatchingFPRAS.TreeMachine.encode_putSingle line 53
  12. inductive OAI.MatchingFPRAS.TreeMachine.Instr line 61
  13. def OAI.MatchingFPRAS.TreeMachine.procedure line 70
  14. def OAI.MatchingFPRAS.TreeMachine.successor line 77
  15. lemma OAI.MatchingFPRAS.TreeMachine.nil_exec line 81
  16. lemma OAI.MatchingFPRAS.TreeMachine.copy_exec line 89
  17. lemma OAI.MatchingFPRAS.TreeMachine.cons_exec line 95
  18. lemma OAI.MatchingFPRAS.TreeMachine.split_exec line 101