i:Vertices(the_graph). (i L)

i:Vertices(the_graph). (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))

L1,L2:Vertices(the_graph) List. L = (L1 @ L2) (s1,s2:Vertices(the_graph) List. topsortl(the_obj;L) = (s2 @ s1) & (j:Vertices(the_graph). ((j s1) L1-the_graph- > *j) & ((j s2) L2-the_graph- > *j & L1-the_graph- > *j)))

i:Vertices(the_graph), s1,s2:Vertices(the_graph) List. topsortl(the_obj;L) = (s1 @ [i] @ s2) (j:Vertices(the_graph). j = i i-the_graph- > *j (j s2))

i:Vertices(the_graph). (i topsortl(the_obj;L))

i,j:Vertices(the_graph). j = i i-the_graph- > *j i before j topsortl(the_obj;L)

(j A)

(i B)

j-the_graph- > *i

k:Vertices(the_graph). k before j L k-the_graph- > *i

(j s1)

s1@0,s2@0:Vertices(the_graph) List. topsortl(the_obj;L) = (s2@0 @ s1@0) & (j@0:Vertices(the_graph). ((j@0 s1@0) s1 @ [j]-the_graph- > *j@0) & ((j@0 s2@0) s2 @ B-the_graph- > *j@0 & s1 @ [j]-the_graph- > *j@0))

i before j topsortl(the_obj;L)

RWO Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B)) 0
THEN
ExRepD
THEN
InstConcl [s2@0;s1@0]

1	27. s1@0: Vertices(the_graph) List 28. s2@0: Vertices(the_graph) List 29. topsortl(the_obj;L) = (s2@0 @ s1@0) 30. j@0:Vertices(the_graph). ((j@0 s1@0) s1 @ [j]-the_graph- > *j@0) & ((j@0 s2@0) s2 @ B-the_graph- > *j@0 & s1 @ [j]-the_graph- > *j@0) (i s2@0)	8 steps
2	27. s1@0: Vertices(the_graph) List 28. s2@0: Vertices(the_graph) List 29. topsortl(the_obj;L) = (s2@0 @ s1@0) 30. j@0:Vertices(the_graph). ((j@0 s1@0) s1 @ [j]-the_graph- > *j@0) & ((j@0 s2@0) s2 @ B-the_graph- > *j@0 & s1 @ [j]-the_graph- > *j@0) (j s1@0)	1 step

About: