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 :
exists: ∃x:A. B[x],
sequence: sequence(T),
equal: s = t ∈ T,
sg-pos: Pos(g),
and: P ∧ Q,
nat: ℕ,
sg-legal1: Legal1(x;y),
add: n + m,
all: ∀x:A. B[x],
nat_plus: ℕ+,
implies: P ⇒ Q,
less_than: a < b,
seq-len: ||s||,
squash: ↓T,
sg-legal2: Legal2(x;y),
subtract: n - m,
seq-item: s[i],
multiply: n * m,
natural_number: $n
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:
2019_06_20-PM-00_52_50
Last ObjectModification:
2019_01_02-PM-01_32_11
Theory : co-recursion-2
Home
Index