At:
connect-iff
1
1
1
1
2
1
1
3
1
1
1.
the_graph: Graph
2.
x,y:Vertices(the_graph). Dec(x = y)
3.
x: Vertices(the_graph)
4.
y: Vertices(the_graph)
5.
n: 
6.
u: Vertices(the_graph)
7.
v: Vertices(the_graph) List
8.
p1:Vertices(the_graph) List.
||p1|| < ||v||+1
path(the_graph;p1)
p1[0] = x
last(p1) = y x = y 
(
z:Vertices(the_graph). 
z = x & x-the_graph- > z & z-the_graph- > *y)
9.
path(the_graph;[u / v])
10.
[u / v][0] = x
11.
last([u / v]) = y
12.
1 < ||v||+1
13.
[u / v][1] = x
14.
path(the_graph;v)
null(v)
By:
RW assert_pushdownC 0
THEN
ObviousFrom [-3]
Generated subgoals:
None
About:
