OAI/Combinatorics/TriangleRemoval/Process/PathRequiredBaseAppend.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.pathRequired_base_append line 18
2. lemma OAI.SharpTerminalLeave.pairRequired_base_child line 23
3. theorem OAI.SharpTerminalLeave.jointMarkedQuery_congr_required line 33
4. theorem OAI.SharpTerminalLeave.jointMarkedQuery_pair_nil line 57
5. theorem OAI.SharpTerminalLeave.jointMarkedQuery_pair_child line 70
6. theorem OAI.SharpTerminalLeave.jointMarkedQuery_hit_head line 83
7. lemma OAI.SharpTerminalLeave.query_trace_cons_hit_tail line 101