OAI/Combinatorics/TriangleRemoval/Spectral/CheckMarkedTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.ExposureTree.checkMarkedTrace line 18
2. lemma OAI.SharpTerminalLeave.ExposureTree.programDemand_marked_trace line 26
3. lemma OAI.SharpTerminalLeave.ExposureTree.checkMarkedTrace_marked line 33
4. lemma OAI.SharpTerminalLeave.ExposureTree.checkMarkedTrace_trace line 48
5. lemma OAI.SharpTerminalLeave.ExposureTree.any_fst_false line 62
6. theorem OAI.SharpTerminalLeave.ExposureTree.checkMarkedTrace_no_demands line 68
7. theorem OAI.SharpTerminalLeave.ExposureTree.checkMarkedTrace_one_hit line 92