Nuprl - Proof: dfsl-traversal-nil 3

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

1. the_graph: Graph
2. i:Vertices(the_graph). nil-the_graph- > *i non-trivial-loop(the_graph;i)
3. L1: Vertices(the_graph) List
4. L2: Vertices(the_graph) List
5. nil = (L1 @ L2)

s1,s2:traversal(the_graph). nil = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j))

By: Thin 2 THEN Inst Thm* l1,l2:T List. (l1 @ l2) = nil l1 = nil & l2 = nil [Vertices(the_graph);L1;L2] THEN Analyze -1 THEN Thin -1 THEN Analyze -1 THEN Analyze -1 THEN RepeatFor 2 ((HypSubst -1 0) THEN (Thin -1)) THEN AllHyps Thin THEN InstConcl [nil;nil] THEN Reduce 0

Generated subgoals:

1 paren(Vertices(the_graph);nil) 1 step

2 paren(Vertices(the_graph);nil) 1 step

3 2. j: Vertices(the_graph)
3. (inl(j) nil)
nil-the_graph- > *j 1 step

4 2. j: Vertices(the_graph)
3. nil-the_graph- > *j
(inl(j) nil) 2 steps

5 2. j: Vertices(the_graph)
3. (inl(j) nil)
nil-the_graph- > *j 1 step

6 2. j: Vertices(the_graph)
3. (inl(j) nil)
nil-the_graph- > *j 1 step

About:

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

1	`paren(Vertices(the_graph);nil)`	1 step

2	`paren(Vertices(the_graph);nil)`	1 step

3	2. `j:` `Vertices(the_graph)` 3. `(inl(j) nil)` `nil-the_graph- > *j`	1 step

4	2. `j:` `Vertices(the_graph)` 3. `nil-the_graph- > *j` `(inl(j) nil)`	2 steps

5	2. `j:` `Vertices(the_graph)` 3. `(inl(j) nil)` `nil-the_graph- > *j`	1 step

6	2. `j:` `Vertices(the_graph)` 3. `(inl(j) nil)` `nil-the_graph- > *j`	1 step