Nuprl Definition : seq-append
seq-append(n;m;s1;s2) == λi.if (i) < (n) then s1 i else if (i) < (n + m) then s2 (i - n) else ⊥
Definitions occuring in Statement :
bottom: ⊥,
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
add: n + m
Definitions occuring in definition :
lambda: λx.A[x],
less: if (a) < (b) then c else d,
add: n + m,
apply: f a,
subtract: n - m,
bottom: ⊥
FDL editor aliases :
seq-append
Latex:
seq-append(n;m;s1;s2) == \mlambda{}i.if (i) < (n) then s1 i else if (i) < (n + m) then s2 (i - n) else \mbot{}
Date html generated:
2016_05_13-PM-03_48_26
Last ObjectModification:
2015_09_22-PM-05_45_17
Theory : bar-induction
Home
Index