Nuprl Definition : coterm-size
coterm-size(t) == fix((λsz,t. case t of inl(v) => 1 | inr(p) => let opr,bts = p in 1 + Σ(sz (snd(bt)) | bt ∈ bts))) t
Definitions occuring in Statement :
lsum: Σ(f[x] | x ∈ L),
pi2: snd(t),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spread: spread def,
add: n + m,
natural_number: $n,
lsum: Σ(f[x] | x ∈ L),
apply: f a,
pi2: snd(t)
FDL editor aliases :
coterm-size
Latex:
coterm-size(t) ==
fix((\mlambda{}sz,t. case t of inl(v) => 1 | inr(p) => let opr,bts = p in 1 + \mSigma{}(sz (snd(bt)) | bt \mmember{} bts))) \000Ct
Date html generated:
2020_05_19-PM-09_53_28
Last ObjectModification:
2020_03_12-AM-10_51_25
Theory : terms
Home
Index