Nuprl Definition : oal_merge
ps ++ qs ==
Y
(λoal_merge,ps,qs. if null(ps) then qs
if null(qs) then ps
if (fst(hd(qs))) <b (fst(hd(ps))) then [hd(ps) / (oal_merge tl(ps) qs)]
if (fst(hd(ps))) <b (fst(hd(qs))) then [hd(qs) / (oal_merge ps tl(qs))]
if ((snd(hd(ps))) * (snd(hd(qs)))) =b e then oal_merge tl(ps) tl(qs)
else [<fst(hd(ps)), (snd(hd(ps))) * (snd(hd(qs)))> / (oal_merge tl(ps) tl(qs))]
fi )
ps
qs
Definitions occuring in Statement :
hd: hd(l),
null: null(as),
tl: tl(l),
cons: [a / b],
ifthenelse: if b then t else f fi ,
infix_ap: x f y,
pi1: fst(t),
pi2: snd(t),
ycomb: Y,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
grp_id: e,
grp_op: *,
grp_eq: =b,
set_blt: a <b b
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
null: null(as),
set_blt: a <b b,
ifthenelse: if b then t else f fi ,
grp_eq: =b,
grp_id: e,
cons: [a / b],
pair: <a, b>,
pi1: fst(t),
infix_ap: x f y,
grp_op: *,
pi2: snd(t),
hd: hd(l),
apply: f a,
tl: tl(l)
Latex:
ps ++ qs ==
Y
(\mlambda{}oal$_{merge}$,ps,qs. if null(ps) then qs
if null(qs) then ps
if (fst(hd(qs))) <\msubb{} (fst(hd(ps))) then [hd(ps) / (oal$_{merge}\mbackslash{}ff\000C24 tl(ps) qs)]
if (fst(hd(ps))) <\msubb{} (fst(hd(qs))) then [hd(qs) / (oal$_{merge}\mbackslash{}ff\000C24 ps tl(qs))]
if ((snd(hd(ps))) * (snd(hd(qs)))) =\msubb{} e then oal$_{merge}$ tl\000C(ps) tl(qs)
else [<fst(hd(ps)), (snd(hd(ps))) * (snd(hd(qs)))> / (oal$_{merge\mbackslash{}ff7\000Cd$ tl(ps) tl(qs))]
fi )
ps
qs
Date html generated:
2016_05_16-AM-08_17_23
Last ObjectModification:
2015_09_23-AM-09_52_52
Theory : polynom_2
Home
Index