graph 1 3 Sections Graphs Doc

RankTheoremName
16 Thm* For any graph the_obj:GraphObject(the_graph), L:V List, s:Traversal, x:V. dfl-traversal(the_graph;L;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x))[dfs-dfl-traversal]
cites
15 Thm* For any graph the_obj:GraphObject(the_graph), P:(VTraversalTraversalProp), s:Traversal, i:V. (s:Traversal, i:V. (inl(i) s) (inr(i) s) P(i,s,nil)) (s1,s2,s3:Traversal, i,j:V. i-the_graph- > j paren(V;s2) (k:V. (inr(k) s2) j-the_graph- > *k) paren(V;s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)) (s1,s2:Traversal, i:V. (inr(i) s1) (inl(i) s1) paren(V;s2) l_disjoint(V+V;s2;s1) no_repeats(V+V;s2) (j:V. (inr(j) s2) i-the_graph- > *j) (j:V. i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1)) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])) (s':Traversal. P(i,s,s') & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & (j:V. (inr(j) s') i-the_graph- > *j) & dfs(the_obj;s;i) = (s' @ s))[dfs_induction4]
3 Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s'))[paren_balance2]
2 Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)[member_append]
1 Thm* l:T List, a,x:T. (x [a / l]) x = a (x l)[cons_member]
2 Thm* For any graph L:V List, i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) L-- > *i dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inr(i) / s])[dfl-traversal-consr]
0 Thm* as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs))[append_assoc]
2 Thm* For any graph L:V List, i:V, s:Traversal. (inr(i) s) dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inl(i) / s])[dfl-traversal-consl]
3 Thm* For any graph A,B:V List. B A A-- > *B[list-list-connect-iseg]
3 Thm* For any graph A,B,C:V List. A-- > *C B-- > *C A @ B-- > *C[list-list-connect-append2]
1 Thm* For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s)[dfl-traversal-connect]

graph 1 3 Sections Graphs Doc