OAI/Combinatorics/ParityLifts/Parser.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.TreeProgram.loop_completes line 7
  2. def OAI.ParityWL.Complexity.streamStep line 35
  3. lemma OAI.ParityWL.Complexity.streamStep_fixed line 39
  4. lemma OAI.ParityWL.Complexity.streamStep_remaining line 42
  5. lemma OAI.ParityWL.Complexity.streamStep_potential line 57
  6. def OAI.ParityWL.Complexity.streamRun line 73
  7. def OAI.ParityWL.Complexity.parseStream line 76
  8. def OAI.ParityWL.Complexity.PolyProgram.streamStep line 79
  9. def OAI.ParityWL.Complexity.PolyProgram.streamRun line 93
  10. def OAI.ParityWL.Complexity.PolyProgram.parseStream line 163
  11. lemma OAI.ParityWL.Complexity.streamStep_chunks line 174
  12. lemma OAI.ParityWL.Complexity.chunks_length line 189
  13. lemma OAI.ParityWL.Complexity.parseStream_chunks line 198
  14. lemma OAI.ParityWL.Complexity.encodeNat_ne_nil line 210
  15. lemma OAI.ParityWL.Complexity.encodeClause_ne_nil line 212
  16. def OAI.ParityWL.Complexity.parseClauses line 215
  17. def OAI.ParityWL.Complexity.PolyProgram.parseClauses line 217
  18. lemma OAI.ParityWL.Complexity.parseClauses_encode line 220
  19. def OAI.ParityWL.Complexity.parseFormula line 224
  20. def OAI.ParityWL.Complexity.PolyProgram.parseFormula line 227
  21. lemma OAI.ParityWL.Complexity.parseFormula_encode line 231