OAI/Combinatorics/Sensitivity/RecursiveFailures.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Fixed initial-input lists of clauses with exactly one failed condition.

  1. def OAI.Paper320.targetFailures line 13
  2. def OAI.Paper320.gateFailures line 18
  3. def OAI.Paper320.targetCandidates line 24
  4. def OAI.Paper320.gateCandidates line 29
  5. def OAI.Paper320.targetWitness line 34
  6. def OAI.Paper320.gateWitness line 39
  7. theorem OAI.Paper320.targetFailures_empty_iff line 44
  8. theorem OAI.Paper320.gateFailures_empty_iff line 50
  9. theorem OAI.Paper320.targetFailures_singleton line 57
  10. theorem OAI.Paper320.gateFailures_singleton line 71
  11. theorem OAI.Paper320.targetCandidates_card line 85
  12. theorem OAI.Paper320.gateCandidates_neighbor line 97
  13. theorem OAI.Paper320.gateCandidates_card line 108