Nuprl Definition : sg-reachable
sg-reachable(g;x;y) ==
∃f:sequence(Pos(g))
(0 < ||f||
∧ (f[0] = x ∈ Pos(g))
∧ (f[||f|| - 1] = y ∈ Pos(g))
∧ (∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1]))))
∧ (∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))))
Definitions occuring in Statement :
sg-legal2: Legal2(x;y),
sg-legal1: Legal1(x;y),
sg-pos: Pos(g),
seq-item: s[i],
seq-len: ||s||,
sequence: sequence(T),
nat_plus: ℕ+,
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
natural_number: $n,
multiply: n * m,
seq-item: s[i],
subtract: n - m,
sg-legal2: Legal2(x;y),
squash: ↓T,
seq-len: ||s||,
less_than: a < b,
implies: P ⇒ Q,
nat_plus: ℕ+,
all: ∀x:A. B[x],
add: n + m,
sg-legal1: Legal1(x;y),
nat: ℕ,
and: P ∧ Q,
sg-pos: Pos(g),
equal: s = t ∈ T,
sequence: sequence(T),
exists: ∃x:A. B[x]
FDL editor aliases :
sg-reachable
Latex:
sg-reachable(g;x;y) ==
\mexists{}f:sequence(Pos(g))
(0 < ||f||
\mwedge{} (f[0] = x)
\mwedge{} (f[||f|| - 1] = y)
\mwedge{} (\mforall{}i:\mBbbN{}. ((2 * i) + 1 < ||f|| {}\mRightarrow{} (\mdownarrow{}Legal1(f[2 * i];f[(2 * i) + 1]))))
\mwedge{} (\mforall{}i:\mBbbN{}\msupplus{}. (2 * i < ||f|| {}\mRightarrow{} (\mdownarrow{}Legal2(f[(2 * i) - 1];f[2 * i])))))
Date html generated:
2018_07_25-PM-01_33_42
Last ObjectModification:
2018_06_18-PM-05_02_53
Theory : co-recursion
Home
Index