At:
dfs-df-traversal
2
2
2
1
2
1
1
3
1
2
3
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
s1: traversal(the_graph)
4.
s2: traversal(the_graph)
5.
i1: Vertices(the_graph)
6.
(inr(i1) 
s1)
7.
(inl(i1) s1)
8.
paren(Vertices(the_graph);s2)
9.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
10.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
11.
j:Vertices(the_graph). (inr(j) s2) 
i1-the_graph- > *j
12.
j:Vertices(the_graph). i1-the_graph- > j j = i1 (inl(j) s2) 
(inl(j) s1) (inr(j) s1)
13.
df-traversal(the_graph;s1)
14.
j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i1
15.
df-traversal(the_graph;s2 @ [inr(i1) / s1])
16.
j:Vertices(the_graph). i1-the_graph- > *j non-trivial-loop(the_graph;j)
17.
j: Vertices(the_graph)
18.
z: Vertices(the_graph)
19.
z = i1
20.
i1-the_graph- > z
21.
z-the_graph- > *j
22.
(inl(z) s1) (inr(z) s1)
23.
(inl(z) s1)
(inr(j) s2 @ [inr(i1) / s1])
By:
((Analyze -2) THEN (InstHyp [z] 14) THEN (InstHyp [i1] 16)) THENA (Auto THEN Connect)
THEN
Analyze -1
THEN
Unfold `non-trivial-loop` 0
THEN
InstConcl [z]
THEN
Connect
Generated subgoals:
None
About:
