Nuprl Definition : maximal-copath
maximal-copath(a.B[a];w) ==
{p:ℕ ⟶ copath(a.B[a];w)|
∀n:ℕ. ((∀i:ℕn. (copath-length(p i) = i ∈ ℤ)) ⇒ (∀i:ℕn - 1. copathAgree(a.B[a];w;p i;p (i + 1))))}
Definitions occuring in Statement :
copathAgree: copathAgree(a.B[a];w;x;y),
copath-length: copath-length(p),
copath: copath(a.B[a];w),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
natural_number: $n,
add: n + m,
apply: f a,
copathAgree: copathAgree(a.B[a];w;x;y),
subtract: n - m,
int_seg: {i..j-},
all: ∀x:A. B[x],
copath-length: copath-length(p),
int: ℤ,
equal: s = t ∈ T,
implies: P ⇒ Q,
nat: ℕ,
copath: copath(a.B[a];w),
function: x:A ⟶ B[x],
set: {x:A| B[x]}
FDL editor aliases :
maximal-copath
Latex:
maximal-copath(a.B[a];w) ==
\{p:\mBbbN{} {}\mrightarrow{} copath(a.B[a];w)|
\mforall{}n:\mBbbN{}. ((\mforall{}i:\mBbbN{}n. (copath-length(p i) = i)) {}\mRightarrow{} (\mforall{}i:\mBbbN{}n - 1. copathAgree(a.B[a];w;p i;p (i + 1))))\}
Date html generated:
2018_07_25-PM-01_49_08
Last ObjectModification:
2018_07_25-AM-10_04_21
Theory : co-recursion
Home
Index