At:
connect transitivity
1
2
2
1.
the_graph: Graph
2.
x: Vertices(the_graph)
3.
y: Vertices(the_graph)
4.
z: Vertices(the_graph)
5.
p1: Vertices(the_graph) List
6.
0 < ||p1||
7.
i:
(||p1||-1). p1[i]-the_graph- > p1[(i+1)]
8.
p1[0] = x
9.
p1[(||p1||-1)] = y
10.
u: Vertices(the_graph)
11.
v: Vertices(the_graph) List
12.
0 < ||v||+1
13.
i:(||v||+1-1). [u / v][i]-the_graph- > [u / v][(i+1)]
14.
u = y
15.
[u / v][(||v||+1-1)] = z
16.
i: (||p1 @ v||-1)
17.
i+1 < ||p1||
18.
i = ||p1||-1
(p1 @ v)[i]-the_graph- > (p1 @ v)[(i+1)]
By:
RWO
Thm* as,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]
0
THEN
InstHyp [i-||p1||+1] -6
THEN
RWO
Thm* a:T, as:T List, i:
. 0 < i 
i
||as|| [a / as][i] = as[(i-1)]
-1
THEN
NthHypSq -1
THEN
Analyze
THEN
Analyze
Generated subgoals:
None
About:
