At:
paren-df-traversal
1
2
2
1
2
1
1.
G: Graph
2.
x,y:Vertices(G). Dec(x = y)
3.
s: traversal(G)
4.
paren(Vertices(G);s)
5.
no_repeats(Vertices(G)+Vertices(G);s)
6.
i:Vertices(G), s1,s2:traversal(G).
s = (s1 @ [inr(i)] @ s2) 
traversal(G)
(j:Vertices(G). (inr(j) s2) 
(inl(j) s2) j-G- > *i)
7.
i:Vertices(G), s1,s2:traversal(G).
(j:Vertices(G). i-G- > *j non-trivial-loop(G;j))
s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2))
8.
i: Vertices(G)
9.
s1: traversal(G)
10.
s2: traversal(G)
11.
j:Vertices(G). i-G- > *j non-trivial-loop(G;j)
12.
s = (s1 @ [inl(i)] @ s2) traversal(G)
13.
j: Vertices(G)
14.
j = i
15.
i-G- > *j
16.
(inr(j) s2)
17.
(inl(j) s2)
18.
s3: (Vertices(G)+Vertices(G)) List
19.
s2@0: (Vertices(G)+Vertices(G)) List
20.
s2 = (s3 @ [inr(i) / s2@0])
21.
(inr(j) s3)
22.
s = (s1 @ [inl(i)] @ s3 @ [inr(i)] @ s2@0) traversal(G)
paren(Vertices(G);s3)
By:
FwdThru
Thm* paren_interval
[4;-1]
Generated subgoals:
None
About:
