Nuprl Definition : lg-add

lg-add(g;a;b) ==
  mklist(||g||;λi.let lbl,L1,L2 = g[i] in 
                  <lbl
                  , if (i =z a) then if (i =z b) then <[i / L1], [i / L2]> else <L1, [b / L2]> fi 
                    if (i =z b) then <[a / L1], L2>
                    else <L1, L2>
                    fi 
                  >)


Definitions occuring in Statement :  mklist: mklist(n;f),  select: L[n],  length: ||as||,  cons: [a / b],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  spreadn: spread3,  lambda: λx.A[x],  pair: <a, b>
FDL editor aliases :  lg-add
Latex:
lg-add(g;a;b)  ==
    mklist(||g||;\mlambda{}i.let  lbl,L1,L2  =  g[i]  in 
                                    <lbl
                                    ,  if  (i  =\msubz{}  a)  then  if  (i  =\msubz{}  b)  then  <[i  /  L1],  [i  /  L2]>  else  <L1,  [b  /  L2]>  fi 
                                        if  (i  =\msubz{}  b)  then  <[a  /  L1],  L2>
                                        else  <L1,  L2>
                                        fi 
                                    >)


Date html generated: 2015_07_22-PM-00_28_36
Last ObjectModification: 2012_02_25-PM-03_34_28

Home Index