| Rank | Theorem | Name |
| 17 | Thm* For any graph
 the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:V. (i  L)   (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))) | [dfsl-properties] |
| cites |
| 13 | Thm* For any graph
the_obj:GraphObject(the_graph), P:((V List)  TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & P(L,dfsl(the_obj;L))) | [dfsl-induction2] |
| 1 | Thm* For any graph
dfsl-traversal(the_graph;nil;nil) | [dfsl-traversal-nil] |
| 16 | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V. df-traversal(the_graph;s) (j:V. (inr(j) s)  (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;dfs(the_obj;s;i)) | [dfs-df-traversal] |
| 14 | Thm* For any graph
the_obj:GraphObject(the_graph), s:Traversal, i:V.  s':Traversal. ((inr(i) s)  (inl(i) s) s' = nil) & ((inr(i) s) & (inl(i) s) (s2:Traversal. s' = ([inl(i)] @ s2 @ [inr(i)]) Traversal)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s) | [dfs-properties] |
| 1 | Thm* For any graph
the_obj:GraphObject(the_graph), x,y:V. Dec(x = y) | [decidable__equal_gr_v] |
| 3 | Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s))) | [decidable__l_member_paren] |
| 3 | Thm* For any graph
A:V List, x:V. A-- > *[x]  A-- > *x | [list-list-connect-singleton] |
| 4 | Thm* For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s) | [dfsl-traversal-append] |
| 2 | Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a) | [l_disjoint_cons2] |
| 2 | Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) | [no_repeats_append_iff] |
| 4 | Thm* s:(T+T) List. paren(T;s) no_repeats(T+T;s) (s1,s2,s3:(T+T) List, x:T. s = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2)) | [paren_interval] |
| 3 | Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c) | [l_disjoint_append] |
| 0 | Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c) | [append_assoc_sq] |
| 1 | Thm* s',s3:(T+T) List. paren(T;s') paren(T;s3) paren(T;s3 @ s') | [append_paren] |
| 3 | Thm* For any graph
A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i | [list-connect-append] |
| 0 | Thm* l:T List. (l @ nil) ~ l | [append_nil_sq] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s')) | [paren_balance1] |
| 3 | Thm* For any graph
i,j:V. [i]-- > *j i-the_graph- > *j | [list-connect-singleton] |
| 0 | Thm* a,x:T. (x [a]) x = a | [member_singleton] |
| 2 | Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) | [member_append] |
| 3 | Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) | [paren_balance2] |
| 14 | Thm* For any graph
the_obj:GraphObject(the_graph), L:V List. (iL.(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))) | [dfsl_member] |