OAI/Combinatorics/TriangleRemoval/Process/IndexedWitnessCode.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpTerminalLeave.IndexedWitnessCode line 18
  2. instance OAI.SharpTerminalLeave.(instance at line 24) line 24
  3. def OAI.SharpTerminalLeave.decodeWitnessPattern line 30
  4. def OAI.SharpTerminalLeave.decodedWitnessPatterns line 35
  5. lemma OAI.SharpTerminalLeave.decodedWitnessPatterns_card line 40
  6. def OAI.SharpTerminalLeave.rootEdgeUniverse line 49
  7. def OAI.SharpTerminalLeave.seedPatternChoices line 51
  8. lemma OAI.SharpTerminalLeave.seedPatternChoices_card line 54
  9. def OAI.SharpTerminalLeave.allDecodedWitnessPatterns line 64
  10. lemma OAI.SharpTerminalLeave.allDecodedWitnessPatterns_card line 68
  11. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathRootEdges_mem_seedPatternChoices line 84
  12. lemma OAI.SharpTerminalLeave.TriangleGrowth.actual_decoded_pattern_mem line 123