Nuprl Definition : s-sub
s-sub(T;s;t) == ∃f:ℕ ⟶ ℕ. ((∀i:ℕ. f i < f (i + 1)) ∧ (∀i:ℕ. (s-nth(i;t) = s-nth(f i;s) ∈ T)))
Definitions occuring in Statement :
s-nth: s-nth(n;s),
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
and: P ∧ Q,
less_than: a < b,
add: n + m,
natural_number: $n,
all: ∀x:A. B[x],
nat: ℕ,
equal: s = t ∈ T,
s-nth: s-nth(n;s),
apply: f a
FDL editor aliases :
s-sub
Latex:
s-sub(T;s;t) == \mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}i:\mBbbN{}. f i < f (i + 1)) \mwedge{} (\mforall{}i:\mBbbN{}. (s-nth(i;t) = s-nth(f i;s))))
Date html generated:
2019_06_20-PM-00_37_50
Last ObjectModification:
2018_11_29-PM-05_17_22
Theory : co-recursion
Home
Index