Nuprl Definition : bag_remove1_aux

bag_remove1_aux(eq;checked;a;as) ==
  fix((λbag_remove1_aux,checked,as. case as of 
                                      [] => inr Ax  
                                      a'::as' =>
                                       if eq a' a then inl (checked @ as') else bag_remove1_aux [a' / checked] as' fi  
                                   esac)) 
  checked 
  as


Definitions occuring in Statement :  append: as @ bs,  list_ind: list_ind,  cons: [a / b],  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  inr: inr x ,  inl: inl x,  axiom: Ax
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  list_ind: list_ind,  inr: inr x ,  axiom: Ax,  ifthenelse: if b then t else f fi ,  inl: inl x,  append: as @ bs,  apply: f a,  cons: [a / b]
FDL editor aliases :  bag_remove1_aux
Latex:
bag\_remove1\_aux(eq;checked;a;as)  ==
    fix((\mlambda{}bag\_remove1$_{aux}$,checked,as.  case  as  of 
                                                                          []  =>  inr  Ax   
                                                                          a'::as'  =>
                                                                            if  eq  a'  a
                                                                          then  inl  (checked  @  as')
                                                                          else  bag\_remove1$_{aux}$  [a'  /  checked]  as'
                                                                          fi   
                                                                    esac)) 
    checked 
    as


Date html generated: 2016_05_15-PM-08_03_35
Last ObjectModification: 2015_09_23-AM-08_20_46

Theory : bags_2


Home Index