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 :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
copath: copath(a.B[a];w),
all: ∀x:A. B[x],
implies: P ⇒ Q,
copathAgree: copathAgree(a.B[a];w;x;y),
add: n + m,
natural_number: $n,
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
not: ¬A,
equal: s = t ∈ T,
int: ℤ,
copath-length: copath-length(p),
apply: f a
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:
2019_06_20-PM-00_57_15
Last ObjectModification:
2019_01_02-PM-01_34_14
Theory : co-recursion-2
Home
Index