1open HolKernel Parse boolLib testutils 2 3val _ = List.app convtest [ 4 ("bagSimps.CANCEL_CONV(1)", bagSimps.CANCEL_CONV, 5 ���b5 + (b1: 'a bag) + b2 + b4 - (b2 + b1)���, 6 ���(b4:'a bag) + b5 - {||}���), 7 ("bagSimps.CANCEL_CONV(2)", bagSimps.CANCEL_CONV, 8 ���b5 + (b1: 'a bag) + b2 + b4 = b2 + b6 + b1���, ���(b4:'a bag) + b5 = b6���), 9 ("bagSimps.CANCEL_CONV(3)", bagSimps.CANCEL_CONV, 10 ���SUB_BAG b2 (b5 + (b1: 'a bag) + b2 + b4)���, ���{||} <= b1 + b4 + b5���) 11]; 12