Nuprl Definition : coW-wfdd
coW-wfdd(a.B[a];w) ==
∀p:{p:n:ℕ ⟶ copath(a.B[a];w)|
∀i:ℕ
((copath-length(p i) = i ∈ ℤ)
⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ)
⇒ copathAgree(a.B[a];w;p i;p (i + 1)))}
(↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ)))
Definitions occuring in Statement :
copathAgree: copathAgree(a.B[a];w;x;y),
copath-length: copath-length(p),
copath: copath(a.B[a];w),
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
apply: f a,
copath-length: copath-length(p),
int: ℤ,
equal: s = t ∈ T,
not: ¬A,
nat: ℕ,
exists: ∃x:A. B[x],
squash: ↓T,
natural_number: $n,
add: n + m,
copathAgree: copathAgree(a.B[a];w;x;y),
implies: P ⇒ Q,
all: ∀x:A. B[x],
copath: copath(a.B[a];w),
function: x:A ⟶ B[x],
set: {x:A| B[x]}
FDL editor aliases :
coW-wfdd
Latex:
coW-wfdd(a.B[a];w) ==
\mforall{}p:\{p:n:\mBbbN{} {}\mrightarrow{} copath(a.B[a];w)|
\mforall{}i:\mBbbN{}
((copath-length(p i) = i)
{}\mRightarrow{} (copath-length(p (i + 1)) = (i + 1))
{}\mRightarrow{} copathAgree(a.B[a];w;p i;p (i + 1)))\}
(\mdownarrow{}\mexists{}i:\mBbbN{}. (\mneg{}(copath-length(p i) = i)))
Date html generated:
2018_07_25-PM-01_41_50
Last ObjectModification:
2018_07_23-PM-03_18_25
Theory : co-recursion
Home
Index