Nuprl - graph_1_2 Citations of l

graph 1 2 Sections Graphs Doc

Def (x

l) ==

. i < ||l|| & x = l[i]

is mentioned by

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]

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]

Thm* For any graph i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;s) df-traversal(the_graph;[inr(i) / s]) [df-traversal-cons2]

Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s))) [decidable__l_member_paren]

Thm* s:(T+T) List. paren(T;s) (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)) [paren_order1]

Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) [paren_balance2]

Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-left-paren(x,y.E(x,y);i;s) (inl(i) s)) [assert-member-left-paren]

Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-right-paren(x,y.E(x,y);i;s) (inr(i) s)) [assert-member-right-paren]

Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s)) [assert-member-paren]

Thm* s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s')) [paren_balance1]

Def dfsl-traversal(the_graph;L;s) == df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s) L-the_graph- > *i) & ((i:Vertices(the_graph). L-the_graph- > *i non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ 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-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j))))) [dfsl-traversal]

Def dfl-traversal(the_graph;L;s) == (i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)) & (j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j) & (i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > *i) [dfl-traversal]

Def depthfirst-traversal(the_graph;s) == i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). j = i i-the_graph- > *j (inl(j) s2)) [depthfirst-traversal]

Def df-traversal(G;s) == (i:Vertices(G), s1,s2:traversal(G). s = (s1 @ [inr(i)] @ s2) traversal(G) (j:Vertices(G). (inr(j) s2) (inl(j) s2) j-G- > *i)) & (i:Vertices(G), s1,s2:traversal(G). (j:Vertices(G). i-G- > *j non-trivial-loop(G;j)) s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2))) [df-traversal]

In prior sections: mb list 1 mb list 2 graph 1 1

Try larger context: Graphs

graph 1 2 Sections Graphs Doc

`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]
`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]
`Thm* For any graph i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;s) df-traversal(the_graph;[inr(i) / s])`	[df-traversal-cons2]
`Thm* (x,y:T. Dec(x = y)) (s:(T+T) List, i:T. Dec((inl(i) s)))`	[decidable__l_member_paren]
`Thm* s:(T+T) List. paren(T;s) (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2))`	[paren_order1]
`Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s'))`	[paren_balance2]
`Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-left-paren(x,y.E(x,y);i;s) (inl(i) s))`	[assert-member-left-paren]
`Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-right-paren(x,y.E(x,y);i;s) (inr(i) s))`	[assert-member-right-paren]
`Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s))`	[assert-member-paren]
`Thm* s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s'))`	[paren_balance1]
Def dfsl-traversal(the_graph;L;s) == df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s) L-the_graph- > i) & ((i:Vertices(the_graph). L-the_graph- > i non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ 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-the_graph- > j) & ((inl(j) s2) L2-the_graph- > j & L1-the_graph- > *j)))))	[dfsl-traversal]
`Def dfl-traversal(the_graph;L;s) == (i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > i)) & (j:Vertices(the_graph). (inr(j) s) L-the_graph- > j) & (i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > i)`	[dfl-traversal]
`Def depthfirst-traversal(the_graph;s) == i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > j non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). j = i i-the_graph- > j (inl(j) s2))`	[depthfirst-traversal]
`Def df-traversal(G;s) == (i:Vertices(G), s1,s2:traversal(G). s = (s1 @ [inr(i)] @ s2) traversal(G) (j:Vertices(G). (inr(j) s2) (inl(j) s2) j-G- > i)) & (i:Vertices(G), s1,s2:traversal(G). (j:Vertices(G). i-G- > j non-trivial-loop(G;j)) s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2)))`	[df-traversal]