OAI/Computability/LoopMatching/LoopParser.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.InputMachine.loopRecord line 11
  2. lemma OAI.LoopMatching.InputMachine.loopRecord_encode line 16
  3. theorem OAI.LoopMatching.InputMachine.loopRecord_poly line 22
  4. lemma OAI.LoopMatching.InputMachine.loopRecord_size line 24
  5. def OAI.LoopMatching.InputMachine.loopStep line 31
  6. lemma OAI.LoopMatching.InputMachine.encodeLoopRecord_ne_nil line 34
  7. lemma OAI.LoopMatching.InputMachine.loopStep_encode line 37
  8. lemma OAI.LoopMatching.InputMachine.loopStep_records_suffix line 42
  9. lemma OAI.LoopMatching.InputMachine.loopRecords_length_le_bits line 53
  10. lemma OAI.LoopMatching.InputMachine.loopStep_size line 62
  11. lemma OAI.LoopMatching.InputMachine.loopStep_iterate_size line 72
  12. def OAI.LoopMatching.InputMachine.countedLoops line 84
  13. theorem OAI.LoopMatching.InputMachine.countedLoops_poly line 86
  14. lemma OAI.LoopMatching.InputMachine.countedLoops_encoded line 107
  15. def OAI.LoopMatching.InputMachine.loops line 112
  16. theorem OAI.LoopMatching.InputMachine.loops_poly line 116
  17. lemma OAI.LoopMatching.InputMachine.loops_encoded line 118
  18. def OAI.LoopMatching.InputMachine.parse line 129
  19. theorem OAI.LoopMatching.InputMachine.parse_poly line 133
  20. lemma OAI.LoopMatching.InputMachine.parse_encoded line 135
  21. def OAI.LoopMatching.InputMachine.prepare line 142
  22. theorem OAI.LoopMatching.InputMachine.prepare_poly line 146
  23. lemma OAI.LoopMatching.InputMachine.prepare_encoded line 153
  24. lemma OAI.LoopMatching.InputMachine.prepare_encoded_pass line 162
  25. lemma OAI.LoopMatching.InputMachine.prepare_encoded_reject line 167