Nuprl Definition : list_accum2

list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y;as;bs)
==r if as is a pair then let a,as' = as 
                         in if bs is a pair then let b,bs' = bs 
                                                 in eval y' = f[y; a; b] in
                                                    list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y';as';bs')
                            otherwise if bs = Ax then eval y' = g[y; a] in
                                                      list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y';as';Ax) ot\000Cherwise ⊥
    otherwise if as = Ax then if bs is a pair then let b,bs' = bs 
                                                   in eval y' = h[y; b] in
                                                      list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y';Ax;bs')
                              otherwise if bs = Ax then y otherwise ⊥ otherwise ⊥
list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y;as;bs) ==
  fix((λlist_accum2,y,as,bs. if as is a pair then let a,as' = as 
                                                  in if bs is a pair then let b,bs' = bs 
                                                                          in eval y' = f[y; a; b] in
                                                                             list_accum2 y' as' bs'
                                                     otherwise if bs = Ax then eval y' = g[y; a] in
                                                                               list_accum2 y' as' Ax otherwise ⊥
                             otherwise if as = Ax then if bs is a pair then let b,bs' = bs 
                                                                            in eval y' = h[y; b] in
                                                                               list_accum2 y' Ax bs'
                                                       otherwise if bs = Ax then y otherwise ⊥ otherwise ⊥)) 
  y 
  as 
  bs


Definitions occuring in Statement :  bottom: ⊥,  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  isaxiom: if z = Ax then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  axiom: Ax
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ispair: if z is a pair then a otherwise b,  spread: spread def,  callbyvalue: callbyvalue,  apply: f a,  axiom: Ax,  isaxiom: if z = Ax then a otherwise b,  bottom: ⊥
FDL editor aliases :  list_accum2
Latex:
list\_accum2(x,a,b.f[x;  a;  b];x,a.g[x;  a];x,b.h[x;  b];y;as;bs)
==r  if  as  is  a  pair
        then  let  a,as'  =  as 
                  in  if  bs  is  a  pair  then  let  b,bs'  =  bs 
                                                                  in  eval  y'  =  f[y;  a;  b]  in
                                                                        list\_accum2(x,a,b.f[x;  a;  b];x,a.g[x;  a];x,b.h[x;  b];y';as';bs')
                        otherwise  if  bs  =  Ax
                                            then  eval  y'  =  g[y;  a]  in
                                                      list\_accum2(x,a,b.f[x;  a;  b];x,a.g[x;  a];x,b.h[x;  b];y';as';Ax)  otherwise\000C  \mbot{}
        otherwise  if  as  =  Ax
                            then  if  bs  is  a  pair
                                      then  let  b,bs'  =  bs 
                                                in  eval  y'  =  h[y;  b]  in
                                                      list\_accum2(x,a,b.f[x;  a;  b];x,a.g[x;  a];x,b.h[x;  b];y';Ax;bs')
                                      otherwise  if  bs  =  Ax  then  y  otherwise  \mbot{}  otherwise  \mbot{}
Latex:
list\_accum2(x,a,b.f[x;  a;  b];x,a.g[x;  a];x,b.h[x;  b];y;as;bs)  ==
    fix((\mlambda{}list$_{accum2}$,y,as,bs.  if  as  is  a  pair  then  let  a,as'  =  as 
                                                                                                  in  if  bs  is  a  pair  then  let  b,bs'  =  bs 
                                                                                                                                                  in  eval  y'  =  f[y;  a;  b]  in
                                                                                                                                                        list$_{accum\000C2}$  y'  as'  bs'
                                                                                                        otherwise  if  bs  =  Ax  then  eval  y'  =  g[y;  a]  in
                                                                                                                                                            list$_{acc\000Cum2}$  y'  as'  Ax  otherwise  \mbot{}
                                                        otherwise  if  as  =  Ax  then  if  bs  is  a  pair  then  let  b,bs'  =  bs 
                                                                                                                                                      in  eval  y'  =  h[y;  b]  in
                                                                                                                                                            list$_{acc\000Cum2}$  y'  Ax  bs'
                                                                                                            otherwise  if  bs  =  Ax  then  y  otherwise  \mbot{}
                                                                            otherwise  \mbot{})) 
    y 
    as 
    bs


Date html generated: 2017_09_29-PM-05_58_29
Last ObjectModification: 2017_04_24-PM-04_39_20

Theory : list_1


Home Index