| Rank | Theorem | Name |
| 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] |
| cites |
| 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] |
| 2 | Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-right-paren(x,y.E(x,y);i;s) (inr(i) s)) | [assert-member-right-paren] |
| 8 | Thm* For any graph
the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) (x:V. P(x) & Q(x)) vertex-count(the_obj;x.P(x)) < vertex-count(the_obj;x.Q(x)) | [vertex-count-less] |
| 8 | Thm* For any graph
the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) vertex-count(the_obj;x.P(x))vertex-count(the_obj;x.Q(x)) | [vertex-count-le] |
| 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] |