Nuprl - Proof: dfsl-traversal-append

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

For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s)

By: Auto THEN ParallelOp -1 THEN Analyze -1 THEN Analyze 0 THEN Try Trivial THEN Try (((Thin -1) THEN (RepeatFor 3 (ParallelOp -1)) THEN (RWO Thm* For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i 0)) THEN OrLeft) THEN ParallelOp -1 THEN Try ((RepeatFor 2 (ParallelOp -1)) THEN (RWO Thm* For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i 0) THEN OrLeft)

Generated subgoal:

1 1. the_graph: Graph
2. L1: Vertices(the_graph) List
3. L2: Vertices(the_graph) List
4. s: traversal(the_graph)
5. L1-the_graph- > *L2
6. df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s) L1-the_graph- > *i)
7. i:Vertices(the_graph). L1 @ L2-the_graph- > *i non-trivial-loop(the_graph;i)
8. L1@0,L2:Vertices(the_graph) List. L1 = (L1@0 @ L2) (s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1@0-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1@0-the_graph- > *j)))
L1@0,L2@0:Vertices(the_graph) List. (L1 @ L2) = (L1@0 @ L2@0) (s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1@0-the_graph- > *j) & ((inl(j) s2) L2@0-the_graph- > *j & L1@0-the_graph- > *j))) 18 steps

About:

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