(28steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
connect-iff
1
1
1
2
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.
p:
Vertices(the_graph) List
7.
p1:Vertices(the_graph) List. ||p1|| < ||p||
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)
8.
path(the_graph;p)
9.
p[0] = x
10.
last(p) = y
11.
1 < ||p||
x = y
(
z:Vertices(the_graph).
z = x & x-the_graph- > z & z-the_graph- > *y)
By:
OrLeft
THEN
Unfold `last` -2
THEN
Subst (||p|| ~ 1) -2
Generated subgoals:
1
10.
p[(||p||-1)] = y
11.
1 < ||p||
||p|| ~ 1
1
step
 
2
10.
p[(1-1)] = y
11.
1 < ||p||
x = y
1
step
About:
(28steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc