OAI/Combinatorics/TriangleRemoval/Process/Attachment.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.lookupGraph_triangle line 19
  2. def OAI.SharpTerminalLeave.RecordedCallForest.attachment line 33
  3. def OAI.SharpTerminalLeave.RecordedCallForest.birthParent line 37
  4. lemma OAI.SharpTerminalLeave.RecordedCallForest.vertexLabel_nonroot line 44
  5. lemma OAI.SharpTerminalLeave.RecordedCallForest.attachment_nonroot line 48
  6. lemma OAI.SharpTerminalLeave.RecordedCallForest.attachment_birth line 51
  7. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthParent_nonroot line 56
  8. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthParent_some line 61
  9. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthParent_none line 69
  10. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthParent_eq line 76
  11. lemma OAI.SharpTerminalLeave.RecordedCallForest.newTriangle line 88
  12. lemma OAI.SharpTerminalLeave.RecordedCallForest.attachments_distinct line 94