Nuprl - Proof: dfl-traversal-consl 1

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

1. the_graph: Graph
2. L: Vertices(the_graph) List
3. i: Vertices(the_graph)
4. s: traversal(the_graph)
5. (inr(i) s)
6. dfl-traversal(the_graph;L;s)
7. i@0: Vertices(the_graph)
8. s1: traversal(the_graph)
9. s2: traversal(the_graph)
10. [inl(i) / s] = (s1 @ [inr(i@0)] @ s2) traversal(the_graph)
11. j: Vertices(the_graph)
12. (inr(j) s2)
13. (inl(j) s2)

j-the_graph- > *i@0

By: Analyze -6 THEN All Reduce THEN SplitCons -4 THEN Try ((Reduce 0) THEN (Unfold `label` 0) THEN (Reduce 0))

Generated subgoals:

1 8. s2: traversal(the_graph)
9. j: Vertices(the_graph)
10. (inr(j) s2)
11. (inl(j) s2)
12. inl(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)
13. s = s2
j-the_graph- > *i@0 1 step

2 8. u: Vertices(the_graph)+Vertices(the_graph)
9. v: (Vertices(the_graph)+Vertices(the_graph)) List
10. s2: traversal(the_graph)
11. j: Vertices(the_graph)
12. (inr(j) s2)
13. (inl(j) s2)
14. inl(i) = u
15. s = (v @ [inr(i@0) / s2]) traversal(the_graph)
j-the_graph- > *i@0 1 step

About:

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

1	8. `s2:` `traversal(the_graph)` 9. `j:` `Vertices(the_graph)` 10. `(inr(j) s2)` 11. `(inl(j) s2)` 12. `inl(i) = inr(i@0) Vertices(the_graph)+Vertices(the_graph)` 13. `s = s2` `j-the_graph- > *i@0`	1 step

2	8. `u:` `Vertices(the_graph)+Vertices(the_graph)` 9. `v:` `(Vertices(the_graph)+Vertices(the_graph)) List` 10. `s2:` `traversal(the_graph)` 11. `j:` `Vertices(the_graph)` 12. `(inr(j) s2)` 13. `(inl(j) s2)` 14. `inl(i) = u` 15. `s = (v @ [inr(i@0) / s2]) traversal(the_graph)` `j-the_graph- > *i@0`	1 step