OAI/Combinatorics/TriangleRemoval/Process/RootSet.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.RecordedCallForest.rootSet line 22
  2. def OAI.SharpTerminalLeave.RecordedCallForest.rootCount line 24
  3. def OAI.SharpTerminalLeave.RecordedCallForest.vertexCount line 26
  4. lemma OAI.SharpTerminalLeave.RecordedCallForest.size_pos line 28
  5. lemma OAI.SharpTerminalLeave.RecordedCallForest.nonroot_pos line 30
  6. def OAI.SharpTerminalLeave.RecordedCallForest.birthIndex line 35
  7. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthIndex_nonroot line 43
  8. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthIndex_injective line 46
  9. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthIndex_lt line 55
  10. def OAI.SharpTerminalLeave.RecordedCallForest.callIndex line 62
  11. lemma OAI.SharpTerminalLeave.RecordedCallForest.callIndex_nonroot line 69
  12. lemma OAI.SharpTerminalLeave.RecordedCallForest.callIndex_birthIndex line 77
  13. lemma OAI.SharpTerminalLeave.RecordedCallForest.birthIndex_callIndex line 84
  14. def OAI.SharpTerminalLeave.RecordedCallForest.rootLabel line 90
  15. lemma OAI.SharpTerminalLeave.RecordedCallForest.rootLabel_mem line 93
  16. lemma OAI.SharpTerminalLeave.RecordedCallForest.rootLabel_injective line 96
  17. lemma OAI.SharpTerminalLeave.RecordedCallForest.rootLabel_covers line 101
  18. def OAI.SharpTerminalLeave.RecordedCallForest.vertexLabel line 106
  19. lemma OAI.SharpTerminalLeave.RecordedCallForest.vertexLabel_root line 110
  20. lemma OAI.SharpTerminalLeave.RecordedCallForest.vertexLabel_birth line 113
  21. lemma OAI.SharpTerminalLeave.RecordedCallForest.vertexLabel_injective_roots line 118
  22. lemma OAI.SharpTerminalLeave.RecordedCallForest.vertexLabel_covers line 123