OAI/Combinatorics/ParityLifts/RaceStage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.Emits.mono line 7
  2. lemma OAI.ParityWL.Complexity.Emits.unique line 18
  3. lemma OAI.ParityWL.Complexity.boundedAnswer_of_emits line 28
  4. lemma OAI.ParityWL.Complexity.boundedAnswer_emits line 33
  5. def OAI.ParityWL.Complexity.PolyProgram.trueTicks line 42
  6. def OAI.ParityWL.Complexity.PolyProgram.trialInput line 45
  7. def OAI.ParityWL.Complexity.racePairs line 54
  8. def OAI.ParityWL.Complexity.raceProbe line 56
  9. def OAI.ParityWL.Complexity.raceStage line 59
  10. def OAI.ParityWL.Complexity.PolyProgram.raceProbe line 62
  11. def OAI.ParityWL.Complexity.PolyProgram.racePairs line 72
  12. def OAI.ParityWL.Complexity.PolyProgram.raceStage line 75
  13. lemma OAI.ParityWL.Complexity.filter_first_sound line 80
  14. lemma OAI.ParityWL.Complexity.filter_first_complete line 91
  15. lemma OAI.ParityWL.Complexity.raceStage_sound line 101
  16. lemma OAI.ParityWL.Complexity.raceStage_complete line 113