Nuprl - Proof: connect weakening

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

For any graph x,y:V. x = y x-the_graph- > *y

By: Auto THEN Unfold `connect` 0 THEN InstConcl [[x]] THEN Reduce 0 THEN All (Unfold `path`) THEN Reduce 0

Generated subgoals:

1 1. the_graph: Graph
2. x: Vertices(the_graph)
3. y: Vertices(the_graph)
4. x = y
last([x]) = y 1 step

2 1. the_graph: Graph
2. x: Vertices(the_graph)
3. y: Vertices(the_graph)
4. x = y
5. p: Vertices(the_graph) List
6. 0 < ||p||
7. i:(||p||-1). p[i]-the_graph- > p[(i+1)]
null(p) 1 step

About:

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

1	1. `the_graph:` `Graph` 2. `x:` `Vertices(the_graph)` 3. `y:` `Vertices(the_graph)` 4. `x = y` `last([x]) = y`	1 step

2	1. `the_graph:` `Graph` 2. `x:` `Vertices(the_graph)` 3. `y:` `Vertices(the_graph)` 4. `x = y` 5. `p:` `Vertices(the_graph) List` 6. `0 < \|\|p\|\|` 7. `i:(\|\|p\|\|-1). p[i]-the_graph- > p[(i+1)]` `null(p)`	1 step