| Rank | Theorem | Name |
| 14 | Thm* For any graph
 the_obj:GraphObject(the_graph), P:(V  TraversalTraversalProp), s:Traversal, i:V. (s1,s2:Traversal, i:V. P(i,s1,s2)   l_disjoint(V+V;s2;s1) & no_repeats(V+V;s2)) (s:Traversal, i:V. member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V.  member-paren(x,y.the_obj.eq(x,y);i;s1) (j:V. i-the_graph- > j j = i (inl(j)  s2)  member-paren(x,y.the_obj.eq(x,y);j;s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) ( s':Traversal. P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)) | [dfs_induction3] |
| cites |
| 9 | Thm* For any graph
the_obj:GraphObject(the_graph). M:(Traversal ). (i:V, s:Traversal. M([inl(i) / s]) M(s)) & (i:V, s:Traversal. member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s)) | [dfs-measure] |
| 0 | Thm* For any graph
the_obj:GraphObject(the_graph). (x,y:V. the_obj.eq(x,y)  x = y) & (T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)) & (T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)) | [graphobj-properties] |
| 0 | Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c) | [append_assoc_sq] |
| 13 | Thm* For any graph
the_obj:GraphObject(the_graph), l:V List, s:Traversal. s':Traversal. (i:V. (i l) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & list_accum(s',j.dfs(the_obj;s';j);s;l) = (s' @ s) | [dfs_accum_member] |
| 1 | Thm* x,z,y,w:T List. ||x|| = ||z||  ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w | [append_one_one] |
| 2 | Thm* E:(TT ). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s)) | [assert-member-paren] |
| 0 | Thm* For any graph
t:GraphObject(the_graph), T:Type. t.eacc (TVT)TVT | [gro_eacc_wf] |