Nuprl Definition : seq-append
seq-append(n;s;s') == λi.if i <z n then s i else s' (i - n) fi
Wellformedness Lemmas :
seq-append_wf_consistent,
seq-append_wf
Definitions occuring in Statement :
ifthenelse: if b then t else f fi
,
lt_int: i <z j
,
apply: f a
,
lambda: λx.A[x]
,
subtract: n - m
Definitions occuring in definition :
subtract: n - m
,
apply: f a
,
lt_int: i <z j
,
ifthenelse: if b then t else f fi
,
lambda: λx.A[x]
FDL editor aliases :
seq-append
Latex:
seq-append(n;s;s') == \mlambda{}i.if i <z n then s i else s' (i - n) fi
Date html generated:
2019_06_20-PM-02_46_46
Last ObjectModification:
2019_06_06-PM-02_25_46
Theory : fan-theorem
Home
Index