Nuprl - Proof: connect-iff

(28steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

For any graph (x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y))

By: Auto

Generated subgoals:

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. x-the_graph- > *y
x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > *y) 24 steps

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. x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > *y)
x-the_graph- > *y 3 steps

About:

(28steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

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. `x-the_graph- > y` `x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > y)`	24 steps

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. `x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > y)` `x-the_graph- > y`	3 steps