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