(21steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
connect
transitivity
2
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.
p:
Vertices(the_graph) List
11.
0 < ||p||
12.
i:
(||p||-1). p[i]-the_graph- > p[(i+1)]
13.
p[0] = y
14.
p[(||p||-1)] = z
15.
1 < ||p||
p[(||p1||+||tl(p)||-1-||p1||+1)] = z
By:
NthHypSq -2
THEN
Analyze
THEN
Analyze
Generated subgoal:
1
||p1||+||tl(p)||-1-||p1||+1 = ||p||-1
1
step
About:
(21steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
||p1||+||tl(p)||-1-||p1||+1 = ||p||-1
i:
(||p1||-1). p1[i]-the_graph- > p1[(i+1)]
i:(||p||-1). p[i]-the_graph- > p[(i+1)]
p[(||p1||+||tl(p)||-1-||p1||+1)] = z
||p1||+||tl(p)||-1-||p1||+1 = ||p||-1
