Nuprl Definition : bag-remove1
bag-remove1(eq;bs;a) ==  bag_remove1_aux(eq;[];a;bs)
Definitions occuring in Statement : 
bag_remove1_aux: bag_remove1_aux(eq;checked;a;as)
, 
nil: []
Definitions occuring in definition : 
bag_remove1_aux: bag_remove1_aux(eq;checked;a;as)
, 
nil: []
FDL editor aliases : 
bag-remove1
Latex:
bag-remove1(eq;bs;a)  ==    bag\_remove1\_aux(eq;[];a;bs)
Date html generated:
2016_05_15-PM-08_03_47
Last ObjectModification:
2015_09_23-AM-08_20_47
Theory : bags_2
Home
Index