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))
s.vertex-count(the_obj;i.
member-right-paren(x,y.the_obj.eq(x,y);i;s))]
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)))
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)))
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))
0
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))
-1)
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))
-1)
None
About:
| | | | | | | | | |
 |  |  |  |  |  |  |
 |