bag : 'a bagBAG_VAL : ('b -> 'a) -> 'b -> 'aLLCONS : 'a -> (unit -> 'a llist) -> 'a llistllcases : 'b -> ('a # 'a llist -> 'b) -> 'a llist -> 'b|- !b x. BAG_VAL b x = b x
|- !h t. LLCONS h t = h:::t ()
llcases_def|- !n c l.
l = [||] /\ llcases n c l = n \/
?h t. l = h:::t /\ llcases n c l = c (h,t)
|- (!b. b - {||} = b) /\ (!b. {||} - b = {||}) /\
(!x b y.
BAG_INSERT x b - {|y|} =
if x = y then b else BAG_INSERT x (b - {|y|})) /\
!b1 y b2. b1 - BAG_INSERT y b2 = b1 - {|y|} - b2
|- (!b. BAG_INTER {||} b = {||}) /\ (!b. BAG_INTER b {||} = {||}) /\
!x b1 b2.
BAG_INTER (BAG_INSERT x b1) b2 =
if x <: b2 then BAG_INSERT x (BAG_INTER b1 (b2 - {|x|}))
else BAG_INTER b1 b2
|- (!b. BAG_MERGE {||} b = b) /\ (!b. BAG_MERGE b {||} = b) /\
!x b1 b2.
BAG_MERGE (BAG_INSERT x b1) b2 =
BAG_INSERT x (BAG_MERGE b1 (b2 - {|x|}))
|- (!b. {||} <= b <=> T) /\
!x b1 b2. BAG_INSERT x b1 <= b2 <=> x <: b2 /\ b1 <= b2 - {|x|}