OAI/Combinatorics/TriangleRemoval/Process/TriangleThird.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.graphCandidate_iff line 18
  2. lemma OAI.SharpTerminalLeave.triangle_third_exists line 28
  3. def OAI.SharpTerminalLeave.triangleThird line 41
  4. lemma OAI.SharpTerminalLeave.triangleThird_spec line 45
  5. def OAI.SharpTerminalLeave.RecordedCallForest.incoming line 55
  6. theorem OAI.SharpTerminalLeave.RecordedCallForest.incoming_spec line 58
  7. theorem OAI.SharpTerminalLeave.RecordedCallForest.incoming_unique line 65
  8. lemma OAI.SharpTerminalLeave.RecordedCallForest.incoming_graph line 78
  9. def OAI.SharpTerminalLeave.RecordedCallForest.newVertex line 85
  10. lemma OAI.SharpTerminalLeave.RecordedCallForest.newVertex_spec line 89
  11. lemma OAI.SharpTerminalLeave.RecordedCallForest.incoming_card line 94
  12. lemma OAI.SharpTerminalLeave.RecordedCallForest.incoming_parent line 98
  13. lemma OAI.SharpTerminalLeave.RecordedCallForest.incoming_focus line 102
  14. lemma OAI.SharpTerminalLeave.RecordedCallForest.incoming_of_nonroot_parent line 107