At:
connect transitivity
2
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||
(p1 @ nil)[(||p1 @ nil||-1)] = z
By:
Subst ((p1 @ nil) ~ p1) 0
Generated subgoals:
| 1 | (p1 @ nil) ~ p1 | 1 step |
| |
| 2 | p1[(||p1||-1)] = z | 1 step |
About:
