tt('const/bag/BAG_ALL_DISTINCT', ty, ![A : $t]: ((A > 'type/num/num') > $o)).
tt('const/bag/BAG_CARD', ty, ![A : $t]: ((A > 'type/num/num') > 'type/num/num')).
tt('const/bag/BAG_CARD_RELn', ty, ![A : $t]: ((A > 'type/num/num') > ('type/num/num' > $o))).
tt('const/bag/BAG_CHOICE', ty, ![A : $t]: ((A > 'type/num/num') > A)).
tt('const/bag/BAG_DELETE', ty, ![A : $t]: ((A > 'type/num/num') > (A > ((A > 'type/num/num') > $o)))).
tt('const/bag/BAG_DIFF', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BAG_DISJOINT', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > $o))).
tt('const/bag/BAG_EVERY', ty, ![A : $t]: ((A > $o) > ((A > 'type/num/num') > $o))).
tt('const/bag/BAG_FILTER', ty, ![A : $t]: ((A > $o) > ((A > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BAG_GEN_PROD', ty, (('type/num/num' > 'type/num/num') > ('type/num/num' > 'type/num/num'))).
tt('const/bag/BAG_GEN_SUM', ty, (('type/num/num' > 'type/num/num') > ('type/num/num' > 'type/num/num'))).
tt('const/bag/BAG_IMAGE', ty, ![A : $t, B : $t]: ((B > A) > ((B > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BAG_IN', ty, ![A : $t]: (A > ((A > 'type/num/num') > $o))).
tt('const/bag/BAG_INN', ty, ![A : $t]: (A > ('type/num/num' > ((A > 'type/num/num') > $o)))).
tt('const/bag/BAG_INSERT', ty, ![A : $t]: (A > ((A > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BAG_INTER', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BAG_MERGE', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BAG_OF_SET', ty, ![A : $t]: ((A > $o) > (A > 'type/num/num'))).
tt('const/bag/BAG_REST', ty, ![A : $t]: ((A > 'type/num/num') > (A > 'type/num/num'))).
tt('const/bag/BAG_UNION', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > (A > 'type/num/num')))).
tt('const/bag/BIG_BAG_UNION', ty, ![A : $t]: (((A > 'type/num/num') > $o) > (A > 'type/num/num'))).
tt('const/bag/EL_BAG', ty, ![A : $t]: (A > (A > 'type/num/num'))).
tt('const/bag/EMPTY_BAG', ty, ![A : $t]: (A > 'type/num/num')).
tt('const/bag/FINITE_BAG', ty, ![A : $t]: ((A > 'type/num/num') > $o)).
tt('const/bag/ITBAG', ty, ![A : $t, B : $t]: ((A > (B > B)) > ((A > 'type/num/num') > (B > B)))).
tt('const/bag/ITBAG_tupled', ty, ![A : $t, B : $t]: ((A > (B > B)) > (('type/pair/prod' (A > 'type/num/num') B) > B))).
tt('const/bag/PSUB_BAG', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > $o))).
tt('const/bag/SET_OF_BAG', ty, ![A : $t]: ((A > 'type/num/num') > (A > $o))).
tt('const/bag/SING_BAG', ty, ![A : $t]: ((A > 'type/num/num') > $o)).
tt('const/bag/SUB_BAG', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > $o))).
tt('const/bag/bag_size', ty, ![A : $t]: ((A > 'type/num/num') > ((A > 'type/num/num') > 'type/num/num'))).
tt('const/bag/dominates', ty, ![A : $t, B : $t]: ((A > (B > $o)) > ((A > $o) > ((B > $o) > $o)))).
tt('const/bag/mlt1', ty, ![A : $t]: ((A > (A > $o)) > ((A > 'type/num/num') > ((A > 'type/num/num') > $o)))).
tt('thm/bag/EMPTY_BAG_', def, ![A : $t]: (('const/bag/EMPTY_BAG' A) = (('const/combin/K' 'type/num/num' A) 'const/num/0'))).
tt('thm/bag/EMPTY_BAG_alt_', ax, ![A : $t]: (('const/bag/EMPTY_BAG' A) = (^[x : A]: 'const/num/0'))).
tt('thm/bag/BAG_INN_', def, ![A : $t]: (![e : A, n : 'type/num/num', b : (A > 'type/num/num')]: ((('const/bag/BAG_INN' A) e n b) = ('const/arithmetic/>=' (b e) n)))).
tt('thm/bag/SUB_BAG_', def, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) = (![x : A, n : 'type/num/num']: ((('const/bag/BAG_INN' A) x n b1) => (('const/bag/BAG_INN' A) x n b2)))))).
tt('thm/bag/PSUB_BAG_', def, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/PSUB_BAG' A) b1 b2) = ((('const/bag/SUB_BAG' A) b1 b2) & (~ (b1 = b2)))))).
tt('thm/bag/BAG_IN_', def, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/BAG_IN' A) e b) = (('const/bag/BAG_INN' A) e ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) b)))).
tt('thm/bag/BAG_UNION_', def, ![A : $t]: (![b : (A > 'type/num/num'), c : (A > 'type/num/num')]: ((('const/bag/BAG_UNION' A) b c) = (^[x : A]: ('const/arithmetic/+' (b x) (c x)))))).
tt('thm/bag/BAG_DIFF_', def, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) b1 b2) = (^[x : A]: ('const/arithmetic/-' (b1 x) (b2 x)))))).
tt('thm/bag/BAG_INSERT_', def, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/BAG_INSERT' A) e b) = (^[x : A]: (('const/bool/COND' 'type/num/num') (x = e) ('const/arithmetic/+' (b e) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (b x)))))).
tt('thm/bag/BAG_cases_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((b = ('const/bag/EMPTY_BAG' A)) | (?[b0 : (A > 'type/num/num'), e : A]: (b = (('const/bag/BAG_INSERT' A) e b0)))))).
tt('thm/bag/BAG_INTER_', def, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_INTER' A) b1 b2) = (^[x : A]: (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' (b1 x) (b2 x)) (b1 x) (b2 x)))))).
tt('thm/bag/BAG_MERGE_', def, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_MERGE' A) b1 b2) = (^[x : A]: (('const/bool/COND' 'type/num/num') ('const/prim_rec/<' (b1 x) (b2 x)) (b2 x) (b1 x)))))).
tt('thm/bag/BAG_MERGE_IDEM_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_MERGE' A) b b) = b))).
tt('thm/bag/BAG_INN_0_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e : A]: (('const/bag/BAG_INN' A) e 'const/num/0' b))).
tt('thm/bag/BAG_INN_LESS_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e : A, n : 'type/num/num', m : 'type/num/num']: (((('const/bag/BAG_INN' A) e n b) & ('const/prim_rec/<' m n)) => (('const/bag/BAG_INN' A) e m b)))).
tt('thm/bag/BAG_IN_BAG_INSERT_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e1 : A, e2 : A]: ((('const/bag/BAG_IN' A) e1 (('const/bag/BAG_INSERT' A) e2 b)) = ((e1 = e2) | (('const/bag/BAG_IN' A) e1 b))))).
tt('thm/bag/BAG_INN_BAG_INSERT_', ax, ![A : $t]: (![n : 'type/num/num', b : (A > 'type/num/num'), e1 : A, e2 : A]: ((('const/bag/BAG_INN' A) e1 n (('const/bag/BAG_INSERT' A) e2 b)) = (((('const/bag/BAG_INN' A) e1 ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) b) & (e1 = e2)) | (('const/bag/BAG_INN' A) e1 n b))))).
tt('thm/bag/BAG_INN_BAG_INSERT_STRONG_', ax, ![A : $t]: (![b : (A > 'type/num/num'), n : 'type/num/num', e1 : A, e2 : A]: ((('const/bag/BAG_INN' A) e1 n (('const/bag/BAG_INSERT' A) e2 b)) = (((('const/bag/BAG_INN' A) e1 ('const/arithmetic/-' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) b) & (e1 = e2)) | ((('const/bag/BAG_INN' A) e1 n b) & (~ (e1 = e2))))))).
tt('thm/bag/BAG_UNION_EQ_LCANCEL1_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((b = (('const/bag/BAG_UNION' A) b c)) = (c = ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/BAG_UNION_EQ_RCANCEL1_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((b = (('const/bag/BAG_UNION' A) c b)) = (c = ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/BAG_IN_BAG_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_IN' A) e (('const/bag/BAG_UNION' A) b1 b2)) = ((('const/bag/BAG_IN' A) e b1) | (('const/bag/BAG_IN' A) e b2))))).
tt('thm/bag/BAG_INN_BAG_UNION_', ax, ![A : $t]: (![n : 'type/num/num', e : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_INN' A) e n (('const/bag/BAG_UNION' A) b1 b2)) = (?[m1 : 'type/num/num', m2 : 'type/num/num']: ((n = ('const/arithmetic/+' m1 m2)) & ((('const/bag/BAG_INN' A) e m1 b1) & (('const/bag/BAG_INN' A) e m2 b2))))))).
tt('thm/bag/BAG_INN_BAG_MERGE_', ax, ![A : $t]: (![n : 'type/num/num', e : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_INN' A) e n (('const/bag/BAG_MERGE' A) b1 b2)) = ((('const/bag/BAG_INN' A) e n b1) | (('const/bag/BAG_INN' A) e n b2))))).
tt('thm/bag/BAG_IN_BAG_MERGE_', ax, ![A : $t]: (![e : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_IN' A) e (('const/bag/BAG_MERGE' A) b1 b2)) = ((('const/bag/BAG_IN' A) e b1) | (('const/bag/BAG_IN' A) e b2))))).
tt('thm/bag/BAG_EXTENSION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((b1 = b2) = (![n : 'type/num/num', e : A]: ((('const/bag/BAG_INN' A) e n b1) = (('const/bag/BAG_INN' A) e n b2)))))).
tt('thm/bag/BAG_UNION_INSERT_0', ax, ![A : $t]: (![e : A, b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_UNION' A) (('const/bag/BAG_INSERT' A) e b1) b2) = (('const/bag/BAG_INSERT' A) e (('const/bag/BAG_UNION' A) b1 b2))))).
tt('thm/bag/BAG_UNION_INSERT_e1', ax, ![A : $t]: (![e : A, b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_UNION' A) b1 (('const/bag/BAG_INSERT' A) e b2)) = (('const/bag/BAG_INSERT' A) e (('const/bag/BAG_UNION' A) b1 b2))))).
tt('thm/bag/BAG_INSERT_DIFF_', ax, ![A : $t]: (![x : A, b : (A > 'type/num/num')]: (~ ((('const/bag/BAG_INSERT' A) x b) = b)))).
tt('thm/bag/BAG_INSERT_NOT_EMPTY_', ax, ![A : $t]: (![x : A, b : (A > 'type/num/num')]: (~ ((('const/bag/BAG_INSERT' A) x b) = ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/BAG_INSERT_ONE_ONE_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), x : A]: (((('const/bag/BAG_INSERT' A) x b1) = (('const/bag/BAG_INSERT' A) x b2)) = (b1 = b2)))).
tt('thm/bag/C_BAG_INSERT_ONE_ONE_', ax, ![A : $t]: (![x : A, y : A, b : (A > 'type/num/num')]: (((('const/bag/BAG_INSERT' A) x b) = (('const/bag/BAG_INSERT' A) y b)) = (x = y)))).
tt('thm/bag/BAG_INSERT_commutes_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e1 : A, e2 : A]: ((('const/bag/BAG_INSERT' A) e1 (('const/bag/BAG_INSERT' A) e2 b)) = (('const/bag/BAG_INSERT' A) e2 (('const/bag/BAG_INSERT' A) e1 b))))).
tt('thm/bag/BAG_DECOMPOSE_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/BAG_IN' A) e b) => (?['b\'' : (A > 'type/num/num')]: (b = (('const/bag/BAG_INSERT' A) e 'b\'')))))).
tt('thm/bag/BAG_UNION_LEFT_CANCEL_', ax, ![A : $t]: (![b : (A > 'type/num/num'), b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/BAG_UNION' A) b b1) = (('const/bag/BAG_UNION' A) b b2)) = (b1 = b2)))).
tt('thm/bag/COMM_BAG_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_UNION' A) b1 b2) = (('const/bag/BAG_UNION' A) b2 b1)))).
tt('thm/bag/BAG_UNION_RIGHT_CANCEL_', ax, ![A : $t]: (![b : (A > 'type/num/num'), b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/BAG_UNION' A) b1 b) = (('const/bag/BAG_UNION' A) b2 b)) = (b1 = b2)))).
tt('thm/bag/ASSOC_BAG_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/BAG_UNION' A) b1 (('const/bag/BAG_UNION' A) b2 b3)) = (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b1 b2) b3)))).
tt('thm/bag/BAG_UNION_EMPTY_0', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_UNION' A) b ('const/bag/EMPTY_BAG' A)) = b))).
tt('thm/bag/BAG_UNION_EMPTY_1', ax, ![B : $t]: (![b : (B > 'type/num/num')]: ((('const/bag/BAG_UNION' B) ('const/bag/EMPTY_BAG' B) b) = b))).
tt('thm/bag/BAG_UNION_EMPTY_e2', ax, ![C : $t]: (![b1 : (C > 'type/num/num'), b2 : (C > 'type/num/num')]: (((('const/bag/BAG_UNION' C) b1 b2) = ('const/bag/EMPTY_BAG' C)) = ((b1 = ('const/bag/EMPTY_BAG' C)) & (b2 = ('const/bag/EMPTY_BAG' C)))))).
tt('thm/bag/BAG_DELETE_', def, ![A : $t]: (![b0 : (A > 'type/num/num'), e : A, b : (A > 'type/num/num')]: ((('const/bag/BAG_DELETE' A) b0 e b) = (b0 = (('const/bag/BAG_INSERT' A) e b))))).
tt('thm/bag/BAG_DELETE_EMPTY_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: (~ (('const/bag/BAG_DELETE' A) ('const/bag/EMPTY_BAG' A) e b)))).
tt('thm/bag/BAG_DELETE_commutes_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), e1 : A, e2 : A]: (((('const/bag/BAG_DELETE' A) b0 e1 b1) & (('const/bag/BAG_DELETE' A) b1 e2 b2)) => (?['b\'' : (A > 'type/num/num')]: ((('const/bag/BAG_DELETE' A) b0 e2 'b\'') & (('const/bag/BAG_DELETE' A) 'b\'' e1 b2)))))).
tt('thm/bag/BAG_DELETE_11_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), e1 : A, e2 : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/BAG_DELETE' A) b0 e1 b1) & (('const/bag/BAG_DELETE' A) b0 e2 b2)) => ((e1 = e2) = (b1 = b2))))).
tt('thm/bag/BAG_INN_BAG_DELETE_', ax, ![A : $t]: (![b : (A > 'type/num/num'), n : 'type/num/num', e : A]: (((('const/bag/BAG_INN' A) e n b) & ('const/arithmetic/>' n 'const/num/0')) => (?['b\'' : (A > 'type/num/num')]: (('const/bag/BAG_DELETE' A) b e 'b\''))))).
tt('thm/bag/BAG_IN_BAG_DELETE_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_IN' A) e b) => (?['b\'' : (A > 'type/num/num')]: (('const/bag/BAG_DELETE' A) b e 'b\''))))).
tt('thm/bag/BAG_DELETE_INSERT_', ax, ![A : $t]: (![x : A, y : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_DELETE' A) (('const/bag/BAG_INSERT' A) x b1) y b2) => (((x = y) & (b1 = b2)) | ((?[b3 : (A > 'type/num/num')]: (('const/bag/BAG_DELETE' A) b1 y b3)) & (~ (x = y))))))).
tt('thm/bag/BAG_DELETE_BAG_IN_up_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), b : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_DELETE' A) b0 e b) => (!['e\'' : A]: ((('const/bag/BAG_IN' A) 'e\'' b) => (('const/bag/BAG_IN' A) 'e\'' b0)))))).
tt('thm/bag/BAG_DELETE_BAG_IN_down_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), b : (A > 'type/num/num'), e1 : A, e2 : A]: (((('const/bag/BAG_DELETE' A) b0 e1 b) & ((~ (e1 = e2)) & (('const/bag/BAG_IN' A) e2 b0))) => (('const/bag/BAG_IN' A) e2 b)))).
tt('thm/bag/BAG_DELETE_BAG_IN_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), b : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_DELETE' A) b0 e b) => (('const/bag/BAG_IN' A) e b0)))).
tt('thm/bag/BAG_DELETE_concrete_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), b : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_DELETE' A) b0 e b) = (('const/arithmetic/>' (b0 e) 'const/num/0') & (b = (^[x : A]: (('const/bool/COND' 'type/num/num') (x = e) ('const/arithmetic/-' (b0 e) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) (b0 x)))))))).
tt('thm/bag/BAG_UNION_DIFF_eliminate_0', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) b c) c) = b))).
tt('thm/bag/BAG_UNION_DIFF_eliminate_e1', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) c b) c) = b))).
tt('thm/bag/BAG_INSERT_EQUAL_', ax, ![A : $t]: (![b : A, a : A, N : (A > 'type/num/num'), M : (A > 'type/num/num')]: (((('const/bag/BAG_INSERT' A) a M) = (('const/bag/BAG_INSERT' A) b N)) = (((M = N) & (a = b)) | (?[k : (A > 'type/num/num')]: ((M = (('const/bag/BAG_INSERT' A) b k)) & (N = (('const/bag/BAG_INSERT' A) a k)))))))).
tt('thm/bag/BAG_DELETE_TWICE_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), e1 : A, e2 : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/BAG_DELETE' A) b0 e1 b1) & ((('const/bag/BAG_DELETE' A) b0 e2 b2) & (~ (b1 = b2)))) => (?[b : (A > 'type/num/num')]: ((('const/bag/BAG_DELETE' A) b1 e2 b) & (('const/bag/BAG_DELETE' A) b2 e1 b)))))).
tt('thm/bag/SING_BAG_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/SING_BAG' A) b) = (?[x : A]: (b = (('const/bag/BAG_INSERT' A) x ('const/bag/EMPTY_BAG' A))))))).
tt('thm/bag/SING_BAG_THM_', ax, ![A : $t]: (![e : A]: (('const/bag/SING_BAG' A) (('const/bag/BAG_INSERT' A) e ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/EL_BAG_', def, ![A : $t]: (![e : A]: ((('const/bag/EL_BAG' A) e) = (('const/bag/BAG_INSERT' A) e ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/EL_BAG_11_', ax, ![A : $t]: (![x : A, y : A]: (((('const/bag/EL_BAG' A) x) = (('const/bag/EL_BAG' A) y)) => (x = y)))).
tt('thm/bag/EL_BAG_INSERT_squeeze_', ax, ![A : $t]: (![x : A, b : (A > 'type/num/num'), y : A]: (((('const/bag/EL_BAG' A) x) = (('const/bag/BAG_INSERT' A) y b)) => ((x = y) & (b = ('const/bag/EMPTY_BAG' A)))))).
tt('thm/bag/SING_EL_BAG_', ax, ![A : $t]: (![e : A]: (('const/bag/SING_BAG' A) (('const/bag/EL_BAG' A) e)))).
tt('thm/bag/BAG_INSERT_UNION_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_INSERT' A) e b) = (('const/bag/BAG_UNION' A) (('const/bag/EL_BAG' A) e) b)))).
tt('thm/bag/BAG_INSERT_EQ_UNION_', ax, ![A : $t]: (![e : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b : (A > 'type/num/num')]: (((('const/bag/BAG_INSERT' A) e b) = (('const/bag/BAG_UNION' A) b1 b2)) => ((('const/bag/BAG_IN' A) e b1) | (('const/bag/BAG_IN' A) e b2))))).
tt('thm/bag/BAG_DELETE_SING_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_DELETE' A) b e ('const/bag/EMPTY_BAG' A)) => (('const/bag/SING_BAG' A) b)))).
tt('thm/bag/NOT_IN_EMPTY_BAG_', ax, ![A : $t]: (![x : A]: (~ (('const/bag/BAG_IN' A) x ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/BAG_INN_EMPTY_BAG_', ax, ![A : $t]: (![e : A, n : 'type/num/num']: ((('const/bag/BAG_INN' A) e n ('const/bag/EMPTY_BAG' A)) = (n = 'const/num/0')))).
tt('thm/bag/MEMBER_NOT_EMPTY_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((?[x : A]: (('const/bag/BAG_IN' A) x b)) = (~ (b = ('const/bag/EMPTY_BAG' A)))))).
tt('thm/bag/SUB_BAG_LEQ_', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) = (![x : A]: ('const/arithmetic/<=' (b1 x) (b2 x)))))).
tt('thm/bag/SUB_BAG_EMPTY_0', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) ('const/bag/EMPTY_BAG' A) b))).
tt('thm/bag/SUB_BAG_EMPTY_e1', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b ('const/bag/EMPTY_BAG' A)) = (b = ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/SUB_BAG_REFL_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b b))).
tt('thm/bag/PSUB_BAG_IRREFL_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (~ (('const/bag/PSUB_BAG' A) b b)))).
tt('thm/bag/SUB_BAG_ANTISYM_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/SUB_BAG' A) b1 b2) & (('const/bag/SUB_BAG' A) b2 b1)) => (b1 = b2)))).
tt('thm/bag/PSUB_BAG_ANTISYM_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (~ ((('const/bag/PSUB_BAG' A) b1 b2) & (('const/bag/PSUB_BAG' A) b2 b1))))).
tt('thm/bag/SUB_BAG_TRANS_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: (((('const/bag/SUB_BAG' A) b1 b2) & (('const/bag/SUB_BAG' A) b2 b3)) => (('const/bag/SUB_BAG' A) b1 b3)))).
tt('thm/bag/PSUB_BAG_TRANS_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: (((('const/bag/PSUB_BAG' A) b1 b2) & (('const/bag/PSUB_BAG' A) b2 b3)) => (('const/bag/PSUB_BAG' A) b1 b3)))).
tt('thm/bag/PSUB_BAG_SUB_BAG_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/PSUB_BAG' A) b1 b2) => (('const/bag/SUB_BAG' A) b1 b2)))).
tt('thm/bag/PSUB_BAG_NOT_EQ_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/PSUB_BAG' A) b1 b2) => (~ (b1 = b2))))).
tt('thm/bag/BAG_DIFF_EMPTY_0', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) b b) = ('const/bag/EMPTY_BAG' A)))).
tt('thm/bag/BAG_DIFF_EMPTY_1', ax, ![B : $t]: (![b : (B > 'type/num/num')]: ((('const/bag/BAG_DIFF' B) b ('const/bag/EMPTY_BAG' B)) = b))).
tt('thm/bag/BAG_DIFF_EMPTY_2', ax, ![C : $t]: (![b : (C > 'type/num/num')]: ((('const/bag/BAG_DIFF' C) ('const/bag/EMPTY_BAG' C) b) = ('const/bag/EMPTY_BAG' C)))).
tt('thm/bag/BAG_DIFF_EMPTY_e3', ax, ![D : $t]: (![b1 : (D > 'type/num/num'), b2 : (D > 'type/num/num')]: ((('const/bag/SUB_BAG' D) b1 b2) => ((('const/bag/BAG_DIFF' D) b1 b2) = ('const/bag/EMPTY_BAG' D))))).
tt('thm/bag/BAG_DIFF_EMPTY_simple_0', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) b b) = ('const/bag/EMPTY_BAG' A)))).
tt('thm/bag/BAG_DIFF_EMPTY_simple_1', ax, ![B : $t]: (![b : (B > 'type/num/num')]: ((('const/bag/BAG_DIFF' B) b ('const/bag/EMPTY_BAG' B)) = b))).
tt('thm/bag/BAG_DIFF_EMPTY_simple_e2', ax, ![C : $t]: (![b : (C > 'type/num/num')]: ((('const/bag/BAG_DIFF' C) ('const/bag/EMPTY_BAG' C) b) = ('const/bag/EMPTY_BAG' C)))).
tt('thm/bag/BAG_DIFF_EQ_EMPTY_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num')]: (((('const/bag/BAG_DIFF' A) b c) = ('const/bag/EMPTY_BAG' A)) = (('const/bag/SUB_BAG' A) b c)))).
tt('thm/bag/BAG_DIFF_INSERT_same_', ax, ![A : $t]: (![x : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_INSERT' A) x b1) (('const/bag/BAG_INSERT' A) x b2)) = (('const/bag/BAG_DIFF' A) b1 b2)))).
tt('thm/bag/BAG_DIFF_INSERT_', ax, ![A : $t]: (![x : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((~ (('const/bag/BAG_IN' A) x b1)) => ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_INSERT' A) x b2) b1) = (('const/bag/BAG_INSERT' A) x (('const/bag/BAG_DIFF' A) b2 b1)))))).
tt('thm/bag/NOT_IN_BAG_DIFF_', ax, ![A : $t]: (![x : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((~ (('const/bag/BAG_IN' A) x b1)) => ((('const/bag/BAG_DIFF' A) b1 (('const/bag/BAG_INSERT' A) x b2)) = (('const/bag/BAG_DIFF' A) b1 b2))))).
tt('thm/bag/BAG_IN_DIFF_I_', ax, ![A : $t]: (![e : A, b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: (((('const/bag/BAG_IN' A) e b1) & (~ (('const/bag/BAG_IN' A) e b2))) => (('const/bag/BAG_IN' A) e (('const/bag/BAG_DIFF' A) b1 b2))))).
tt('thm/bag/BAG_IN_DIFF_E_', ax, ![A : $t]: (![e : A, b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_IN' A) e (('const/bag/BAG_DIFF' A) b1 b2)) => (('const/bag/BAG_IN' A) e b1)))).
tt('thm/bag/BAG_UNION_DIFF_', ax, ![A : $t]: (![X : (A > 'type/num/num'), Y : (A > 'type/num/num'), Z : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) Z Y) => (((('const/bag/BAG_UNION' A) X (('const/bag/BAG_DIFF' A) Y Z)) = (('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) X Y) Z)) & ((('const/bag/BAG_UNION' A) (('const/bag/BAG_DIFF' A) Y Z) X) = (('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) X Y) Z)))))).
tt('thm/bag/BAG_DIFF_2L_', ax, ![A : $t]: (![X : (A > 'type/num/num'), Y : (A > 'type/num/num'), Z : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_DIFF' A) X Y) Z) = (('const/bag/BAG_DIFF' A) X (('const/bag/BAG_UNION' A) Y Z))))).
tt('thm/bag/BAG_DIFF_2R_', ax, ![A : $t]: (![A0 : (A > 'type/num/num'), B : (A > 'type/num/num'), C : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) C B) => ((('const/bag/BAG_DIFF' A) A0 (('const/bag/BAG_DIFF' A) B C)) = (('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) A0 C) B))))).
tt('thm/bag/SUB_BAG_BAG_DIFF_', ax, ![A : $t]: (![X : (A > 'type/num/num'), Y : (A > 'type/num/num'), 'Y\'' : (A > 'type/num/num'), Z : (A > 'type/num/num'), W : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_DIFF' A) X Y) (('const/bag/BAG_DIFF' A) Z W)) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_DIFF' A) X (('const/bag/BAG_UNION' A) Y 'Y\'')) (('const/bag/BAG_DIFF' A) Z (('const/bag/BAG_UNION' A) W 'Y\'')))))).
tt('thm/bag/BAG_DIFF_UNION_eliminate_0', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) b1 b3)) = (('const/bag/BAG_DIFF' A) b2 b3)))).
tt('thm/bag/BAG_DIFF_UNION_eliminate_1', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) b3 b1)) = (('const/bag/BAG_DIFF' A) b2 b3)))).
tt('thm/bag/BAG_DIFF_UNION_eliminate_2', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b1 b3)) = (('const/bag/BAG_DIFF' A) b2 b3)))).
tt('thm/bag/BAG_DIFF_UNION_eliminate_e3', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b3 b1)) = (('const/bag/BAG_DIFF' A) b2 b3)))).
tt('thm/bag/SUB_BAG_UNION_eliminate_0', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) b1 b3)) = (('const/bag/SUB_BAG' A) b2 b3)))).
tt('thm/bag/SUB_BAG_UNION_eliminate_1', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) b3 b1)) = (('const/bag/SUB_BAG' A) b2 b3)))).
tt('thm/bag/SUB_BAG_UNION_eliminate_2', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b1 b3)) = (('const/bag/SUB_BAG' A) b2 b3)))).
tt('thm/bag/SUB_BAG_UNION_eliminate_e3', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b3 b1)) = (('const/bag/SUB_BAG' A) b2 b3)))).
tt('thm/bag/move_BAG_UNION_over_eq_', ax, ![A : $t]: (![X : (A > 'type/num/num'), Y : (A > 'type/num/num'), Z : (A > 'type/num/num')]: (((('const/bag/BAG_UNION' A) X Y) = Z) => (X = (('const/bag/BAG_DIFF' A) Z Y))))).
tt('thm/bag/SUB_BAG_UNION_0', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) => (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b2 b)))))).
tt('thm/bag/SUB_BAG_UNION_1', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) => (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b b2)))))).
tt('thm/bag/SUB_BAG_UNION_2', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b2 b3)) => (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b2 b) b3)))))).
tt('thm/bag/SUB_BAG_UNION_3', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b2 b3)) => (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b b2) b3)))))).
tt('thm/bag/SUB_BAG_UNION_4', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b3 b2)) => (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b3 (('const/bag/BAG_UNION' A) b2 b))))))).
tt('thm/bag/SUB_BAG_UNION_5', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b3 b2)) => (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b3 (('const/bag/BAG_UNION' A) b b2))))))).
tt('thm/bag/SUB_BAG_UNION_6', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b3) => ((('const/bag/SUB_BAG' A) b2 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) b3 b4)))))).
tt('thm/bag/SUB_BAG_UNION_7', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b4) => ((('const/bag/SUB_BAG' A) b2 b3) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) b3 b4)))))).
tt('thm/bag/SUB_BAG_UNION_8', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b3 b5)) => ((('const/bag/SUB_BAG' A) b2 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b3 b4) b5)))))).
tt('thm/bag/SUB_BAG_UNION_9', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b4 b5)) => ((('const/bag/SUB_BAG' A) b2 b3) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b3 b4) b5)))))).
tt('thm/bag/SUB_BAG_UNION_10', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b2 (('const/bag/BAG_UNION' A) b3 b5)) => ((('const/bag/SUB_BAG' A) b1 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b3 b4) b5)))))).
tt('thm/bag/SUB_BAG_UNION_11', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b2 (('const/bag/BAG_UNION' A) b4 b5)) => ((('const/bag/SUB_BAG' A) b1 b3) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b3 b4) b5)))))).
tt('thm/bag/SUB_BAG_UNION_12', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b5 b3)) => ((('const/bag/SUB_BAG' A) b2 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b5 (('const/bag/BAG_UNION' A) b3 b4))))))).
tt('thm/bag/SUB_BAG_UNION_13', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_UNION' A) b5 b4)) => ((('const/bag/SUB_BAG' A) b2 b3) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b5 (('const/bag/BAG_UNION' A) b3 b4))))))).
tt('thm/bag/SUB_BAG_UNION_14', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b2 (('const/bag/BAG_UNION' A) b5 b3)) => ((('const/bag/SUB_BAG' A) b1 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b5 (('const/bag/BAG_UNION' A) b3 b4))))))).
tt('thm/bag/SUB_BAG_UNION_15', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b2 (('const/bag/BAG_UNION' A) b5 b4)) => ((('const/bag/SUB_BAG' A) b1 b3) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) (('const/bag/BAG_UNION' A) b5 (('const/bag/BAG_UNION' A) b3 b4))))))).
tt('thm/bag/SUB_BAG_UNION_16', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) b4) => ((('const/bag/SUB_BAG' A) b3 b5) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b1 b3) b2) (('const/bag/BAG_UNION' A) b4 b5)))))).
tt('thm/bag/SUB_BAG_UNION_17', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) b5) => ((('const/bag/SUB_BAG' A) b3 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b1 b3) b2) (('const/bag/BAG_UNION' A) b4 b5)))))).
tt('thm/bag/SUB_BAG_UNION_18', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b3 b2) b4) => ((('const/bag/SUB_BAG' A) b1 b5) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b1 b3) b2) (('const/bag/BAG_UNION' A) b4 b5)))))).
tt('thm/bag/SUB_BAG_UNION_19', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b3 b2) b5) => ((('const/bag/SUB_BAG' A) b1 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) (('const/bag/BAG_UNION' A) b1 b3) b2) (('const/bag/BAG_UNION' A) b4 b5)))))).
tt('thm/bag/SUB_BAG_UNION_20', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) b4) => ((('const/bag/SUB_BAG' A) b3 b5) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 (('const/bag/BAG_UNION' A) b1 b3)) (('const/bag/BAG_UNION' A) b5 b4)))))).
tt('thm/bag/SUB_BAG_UNION_21', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b1) b5) => ((('const/bag/SUB_BAG' A) b3 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 (('const/bag/BAG_UNION' A) b1 b3)) (('const/bag/BAG_UNION' A) b5 b4)))))).
tt('thm/bag/SUB_BAG_UNION_22', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b3) b4) => ((('const/bag/SUB_BAG' A) b1 b5) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 (('const/bag/BAG_UNION' A) b1 b3)) (('const/bag/BAG_UNION' A) b5 b4)))))).
tt('thm/bag/SUB_BAG_UNION_e23', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num'), b5 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 b3) b5) => ((('const/bag/SUB_BAG' A) b1 b4) => (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b2 (('const/bag/BAG_UNION' A) b1 b3)) (('const/bag/BAG_UNION' A) b5 b4)))))).
tt('thm/bag/SUB_BAG_EL_BAG_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/EL_BAG' A) e) b) = (('const/bag/BAG_IN' A) e b)))).
tt('thm/bag/SUB_BAG_INSERT_', ax, ![A : $t]: (![e : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_INSERT' A) e b1) (('const/bag/BAG_INSERT' A) e b2)) = (('const/bag/SUB_BAG' A) b1 b2)))).
tt('thm/bag/SUB_BAG_INSERT_I_', ax, ![A : $t]: (![b : (A > 'type/num/num'), c : (A > 'type/num/num'), e : A]: ((('const/bag/SUB_BAG' A) b c) => (('const/bag/SUB_BAG' A) b (('const/bag/BAG_INSERT' A) e c))))).
tt('thm/bag/NOT_IN_SUB_BAG_INSERT_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), e : A]: ((~ (('const/bag/BAG_IN' A) e b1)) => ((('const/bag/SUB_BAG' A) b1 (('const/bag/BAG_INSERT' A) e b2)) = (('const/bag/SUB_BAG' A) b1 b2))))).
tt('thm/bag/SUB_BAG_BAG_IN_', ax, ![A : $t]: (![x : A, b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_INSERT' A) x b1) b2) => (('const/bag/BAG_IN' A) x b2)))).
tt('thm/bag/SUB_BAG_EXISTS_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) = (?[b : (A > 'type/num/num')]: (b2 = (('const/bag/BAG_UNION' A) b1 b)))))).
tt('thm/bag/SUB_BAG_UNION_DIFF_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b3) => ((('const/bag/SUB_BAG' A) b2 (('const/bag/BAG_DIFF' A) b3 b1)) = (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) b3))))).
tt('thm/bag/SUB_BAG_UNION_down_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b2) b3) => ((('const/bag/SUB_BAG' A) b1 b3) & (('const/bag/SUB_BAG' A) b2 b3))))).
tt('thm/bag/SUB_BAG_DIFF_0', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) => (![b3 : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) (('const/bag/BAG_DIFF' A) b1 b3) b2))))).
tt('thm/bag/SUB_BAG_DIFF_e1', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b3 : (A > 'type/num/num'), b4 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b2 b1) => ((('const/bag/SUB_BAG' A) b4 b3) => ((('const/bag/SUB_BAG' A) (('const/bag/BAG_DIFF' A) b1 b2) (('const/bag/BAG_DIFF' A) b3 b4)) = (('const/bag/SUB_BAG' A) (('const/bag/BAG_UNION' A) b1 b4) (('const/bag/BAG_UNION' A) b2 b3))))))).
tt('thm/bag/SUB_BAG_PSUB_BAG_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) = ((('const/bag/PSUB_BAG' A) b1 b2) | (b1 = b2))))).
tt('thm/bag/BAG_DELETE_PSUB_BAG_', ax, ![A : $t]: (![b0 : (A > 'type/num/num'), e : A, b : (A > 'type/num/num')]: ((('const/bag/BAG_DELETE' A) b0 e b) => (('const/bag/PSUB_BAG' A) b b0)))).
tt('thm/bag/SET_OF_BAG_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/SET_OF_BAG' A) b) = (^[x : A]: (('const/bag/BAG_IN' A) x b))))).
tt('thm/bag/BAG_OF_SET_', def, ![A : $t]: (![P : (A > $o)]: ((('const/bag/BAG_OF_SET' A) P) = (^[x : A]: (('const/bool/COND' 'type/num/num') (('const/bool/IN' A) x P) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) 'const/num/0'))))).
tt('thm/bag/SET_OF_EMPTY_', ax, ![A : $t]: ((('const/bag/BAG_OF_SET' A) ('const/pred_set/EMPTY' A)) = ('const/bag/EMPTY_BAG' A))).
tt('thm/bag/BAG_IN_BAG_OF_SET_', ax, ![A : $t]: (![P : (A > $o), p : A]: ((('const/bag/BAG_IN' A) p (('const/bag/BAG_OF_SET' A) P)) = (('const/bool/IN' A) p P)))).
tt('thm/bag/BAG_OF_EMPTY_', ax, ![A : $t]: ((('const/bag/SET_OF_BAG' A) ('const/bag/EMPTY_BAG' A)) = ('const/pred_set/EMPTY' A))).
tt('thm/bag/SET_BAG_I_', ax, ![A : $t]: (![s : (A > $o)]: ((('const/bag/SET_OF_BAG' A) (('const/bag/BAG_OF_SET' A) s)) = s))).
tt('thm/bag/SUB_BAG_SET_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) => (('const/pred_set/SUBSET' A) (('const/bag/SET_OF_BAG' A) b1) (('const/bag/SET_OF_BAG' A) b2))))).
tt('thm/bag/SET_OF_BAG_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SET_OF_BAG' A) (('const/bag/BAG_UNION' A) b1 b2)) = (('const/pred_set/UNION' A) (('const/bag/SET_OF_BAG' A) b1) (('const/bag/SET_OF_BAG' A) b2))))).
tt('thm/bag/SET_OF_BAG_MERGE_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SET_OF_BAG' A) (('const/bag/BAG_MERGE' A) b1 b2)) = (('const/pred_set/UNION' A) (('const/bag/SET_OF_BAG' A) b1) (('const/bag/SET_OF_BAG' A) b2))))).
tt('thm/bag/SET_OF_BAG_INSERT_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/SET_OF_BAG' A) (('const/bag/BAG_INSERT' A) e b)) = (('const/pred_set/INSERT' A) e (('const/bag/SET_OF_BAG' A) b))))).
tt('thm/bag/SET_OF_EL_BAG_', ax, ![A : $t]: (![e : A]: ((('const/bag/SET_OF_BAG' A) (('const/bag/EL_BAG' A) e)) = (('const/pred_set/INSERT' A) e ('const/pred_set/EMPTY' A))))).
tt('thm/bag/SET_OF_BAG_DIFF_SUBSET_down_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (('const/pred_set/SUBSET' A) (('const/pred_set/DIFF' A) (('const/bag/SET_OF_BAG' A) b1) (('const/bag/SET_OF_BAG' A) b2)) (('const/bag/SET_OF_BAG' A) (('const/bag/BAG_DIFF' A) b1 b2))))).
tt('thm/bag/SET_OF_BAG_DIFF_SUBSET_up_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (('const/pred_set/SUBSET' A) (('const/bag/SET_OF_BAG' A) (('const/bag/BAG_DIFF' A) b1 b2)) (('const/bag/SET_OF_BAG' A) b1)))).
tt('thm/bag/IN_SET_OF_BAG_', ax, ![A : $t]: (![x : A, b : (A > 'type/num/num')]: ((('const/bool/IN' A) x (('const/bag/SET_OF_BAG' A) b)) = (('const/bag/BAG_IN' A) x b)))).
tt('thm/bag/SET_OF_BAG_EQ_EMPTY_0', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/pred_set/EMPTY' A) = (('const/bag/SET_OF_BAG' A) b)) = (b = ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/SET_OF_BAG_EQ_EMPTY_e1', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (((('const/bag/SET_OF_BAG' A) b) = ('const/pred_set/EMPTY' A)) = (b = ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/BAG_DISJOINT_', def, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_DISJOINT' A) b1 b2) = (('const/pred_set/DISJOINT' A) (('const/bag/SET_OF_BAG' A) b1) (('const/bag/SET_OF_BAG' A) b2))))).
tt('thm/bag/BAG_DISJOINT_EMPTY_0', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (('const/bag/BAG_DISJOINT' A) b ('const/bag/EMPTY_BAG' A)))).
tt('thm/bag/BAG_DISJOINT_EMPTY_e1', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (('const/bag/BAG_DISJOINT' A) ('const/bag/EMPTY_BAG' A) b))).
tt('thm/bag/BAG_DISJOINT_DIFF_', ax, ![A : $t]: (![B1 : (A > 'type/num/num'), B2 : (A > 'type/num/num')]: (('const/bag/BAG_DISJOINT' A) (('const/bag/BAG_DIFF' A) B1 B2) (('const/bag/BAG_DIFF' A) B2 B1)))).
tt('thm/bag/BAG_DISJOINT_BAG_IN_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_DISJOINT' A) b1 b2) = (![e : A]: ((~ (('const/bag/BAG_IN' A) e b1)) | (~ (('const/bag/BAG_IN' A) e b2))))))).
tt('thm/bag/BAG_DISJOINT_BAG_INSERT_0', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), e1 : A]: ((('const/bag/BAG_DISJOINT' A) (('const/bag/BAG_INSERT' A) e1 b1) b2) = ((~ (('const/bag/BAG_IN' A) e1 b2)) & (('const/bag/BAG_DISJOINT' A) b1 b2))))).
tt('thm/bag/BAG_DISJOINT_BAG_INSERT_e1', ax, ![B : $t]: (![b1 : (B > 'type/num/num'), b2 : (B > 'type/num/num'), e2 : B]: ((('const/bag/BAG_DISJOINT' B) b1 (('const/bag/BAG_INSERT' B) e2 b2)) = ((~ (('const/bag/BAG_IN' B) e2 b1)) & (('const/bag/BAG_DISJOINT' B) b1 b2))))).
tt('thm/bag/BAG_DISJOINT_BAG_UNION_0', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_DISJOINT' A) b1 (('const/bag/BAG_UNION' A) b2 b3)) = ((('const/bag/BAG_DISJOINT' A) b1 b2) & (('const/bag/BAG_DISJOINT' A) b1 b3))))).
tt('thm/bag/BAG_DISJOINT_BAG_UNION_e1', ax, ![A : $t]: (![b3 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: ((('const/bag/BAG_DISJOINT' A) (('const/bag/BAG_UNION' A) b1 b2) b3) = ((('const/bag/BAG_DISJOINT' A) b1 b3) & (('const/bag/BAG_DISJOINT' A) b2 b3))))).
tt('thm/bag/FINITE_BAG_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) = (![P : ((A > 'type/num/num') > $o)]: (((P ('const/bag/EMPTY_BAG' A)) & (![b0 : (A > 'type/num/num')]: ((P b0) => (![e : A]: (P (('const/bag/BAG_INSERT' A) e b0)))))) => (P b)))))).
tt('thm/bag/FINITE_EMPTY_BAG_', ax, ![A : $t]: (('const/bag/FINITE_BAG' A) ('const/bag/EMPTY_BAG' A))).
tt('thm/bag/FINITE_BAG_INSERT_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (![e : A]: (('const/bag/FINITE_BAG' A) (('const/bag/BAG_INSERT' A) e b)))))).
tt('thm/bag/FINITE_BAG_INDUCT_', ax, ![A : $t]: (![P : ((A > 'type/num/num') > $o)]: (((P ('const/bag/EMPTY_BAG' A)) & (![b : (A > 'type/num/num')]: ((P b) => (![e : A]: (P (('const/bag/BAG_INSERT' A) e b)))))) => (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (P b)))))).
tt('thm/bag/STRONG_FINITE_BAG_INDUCT_', ax, ![A : $t]: (![P : ((A > 'type/num/num') > $o)]: (((P ('const/bag/EMPTY_BAG' A)) & (![b : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b) & (P b)) => (![e : A]: (P (('const/bag/BAG_INSERT' A) e b)))))) => (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (P b)))))).
tt('thm/bag/FINITE_BAG_THM_0', ax, ![A : $t]: (('const/bag/FINITE_BAG' A) ('const/bag/EMPTY_BAG' A))).
tt('thm/bag/FINITE_BAG_THM_e1', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) (('const/bag/BAG_INSERT' A) e b)) = (('const/bag/FINITE_BAG' A) b)))).
tt('thm/bag/FINITE_BAG_DIFF_', ax, ![A : $t]: (![b1 : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b1) => (![b2 : (A > 'type/num/num')]: (('const/bag/FINITE_BAG' A) (('const/bag/BAG_DIFF' A) b1 b2)))))).
tt('thm/bag/FINITE_BAG_DIFF_dual_', ax, ![A : $t]: (![b1 : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b1) => (![b2 : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) (('const/bag/BAG_DIFF' A) b2 b1)) => (('const/bag/FINITE_BAG' A) b2)))))).
tt('thm/bag/FINITE_BAG_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) (('const/bag/BAG_UNION' A) b1 b2)) = ((('const/bag/FINITE_BAG' A) b1) & (('const/bag/FINITE_BAG' A) b2))))).
tt('thm/bag/FINITE_SUB_BAG_', ax, ![A : $t]: (![b1 : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b1) => (![b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b2 b1) => (('const/bag/FINITE_BAG' A) b2)))))).
tt('thm/bag/BAG_CARD_RELn_', def, ![A : $t]: (![b : (A > 'type/num/num'), n : 'type/num/num']: ((('const/bag/BAG_CARD_RELn' A) b n) = (![P : ((A > 'type/num/num') > ('type/num/num' > $o))]: (((P ('const/bag/EMPTY_BAG' A) 'const/num/0') & (![b0 : (A > 'type/num/num'), n0 : 'type/num/num']: ((P b0 n0) => (![e : A]: (P (('const/bag/BAG_INSERT' A) e b0) ('const/num/SUC' n0)))))) => (P b n)))))).
tt('thm/bag/BAG_CARD_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (('const/bag/BAG_CARD_RELn' A) b (('const/bag/BAG_CARD' A) b))))).
tt('thm/bag/BAG_CARD_EMPTY_', ax, ![A : $t]: ((('const/bag/BAG_CARD' A) ('const/bag/EMPTY_BAG' A)) = 'const/num/0')).
tt('thm/bag/BCARD_0_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (((('const/bag/BAG_CARD' A) b) = 'const/num/0') = (b = ('const/bag/EMPTY_BAG' A)))))).
tt('thm/bag/BAG_CARD_THM_0', ax, ![A : $t]: ((('const/bag/BAG_CARD' A) ('const/bag/EMPTY_BAG' A)) = 'const/num/0')).
tt('thm/bag/BAG_CARD_THM_e1', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (![e : A]: ((('const/bag/BAG_CARD' A) (('const/bag/BAG_INSERT' A) e b)) = ('const/arithmetic/+' (('const/bag/BAG_CARD' A) b) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/bag/BAG_CARD_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b1) & (('const/bag/FINITE_BAG' A) b2)) => ((('const/bag/BAG_CARD' A) (('const/bag/BAG_UNION' A) b1 b2)) = ('const/arithmetic/+' (('const/bag/BAG_CARD' A) b1) (('const/bag/BAG_CARD' A) b2)))))).
tt('thm/bag/BCARD_SUC_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (![n : 'type/num/num']: (((('const/bag/BAG_CARD' A) b) = ('const/num/SUC' n)) = (?[b0 : (A > 'type/num/num'), e : A]: ((b = (('const/bag/BAG_INSERT' A) e b0)) & ((('const/bag/BAG_CARD' A) b0) = n)))))))).
tt('thm/bag/BAG_CARD_BAG_INN_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (![n : 'type/num/num', e : A]: ((('const/bag/BAG_INN' A) e n b) => ('const/arithmetic/<=' n (('const/bag/BAG_CARD' A) b))))))).
tt('thm/bag/SUB_BAG_DIFF_EQ_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b1 b2) => (b2 = (('const/bag/BAG_UNION' A) b1 (('const/bag/BAG_DIFF' A) b2 b1)))))).
tt('thm/bag/SUB_BAG_CARD_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b2) & (('const/bag/SUB_BAG' A) b1 b2)) => ('const/arithmetic/<=' (('const/bag/BAG_CARD' A) b1) (('const/bag/BAG_CARD' A) b2))))).
tt('thm/bag/BAG_CARD_DIFF_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (![c : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) c b) => ((('const/bag/BAG_CARD' A) (('const/bag/BAG_DIFF' A) b c)) = ('const/arithmetic/-' (('const/bag/BAG_CARD' A) b) (('const/bag/BAG_CARD' A) c)))))))).
tt('thm/bag/BAG_FILTER_DEF_', def, ![A : $t]: (![P : (A > $o), b : (A > 'type/num/num')]: ((('const/bag/BAG_FILTER' A) P b) = (^[e : A]: (('const/bool/COND' 'type/num/num') (P e) (b e) 'const/num/0'))))).
tt('thm/bag/BAG_FILTER_EMPTY_', ax, ![A : $t]: (![P : (A > $o)]: ((('const/bag/BAG_FILTER' A) P ('const/bag/EMPTY_BAG' A)) = ('const/bag/EMPTY_BAG' A)))).
tt('thm/bag/BAG_FILTER_BAG_INSERT_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num'), P : (A > $o)]: ((('const/bag/BAG_FILTER' A) P (('const/bag/BAG_INSERT' A) e b)) = (('const/bool/COND' (A > 'type/num/num')) (P e) (('const/bag/BAG_INSERT' A) e (('const/bag/BAG_FILTER' A) P b)) (('const/bag/BAG_FILTER' A) P b))))).
tt('thm/bag/FINITE_BAG_FILTER_', ax, ![A : $t]: (![P : (A > $o), b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (('const/bag/FINITE_BAG' A) (('const/bag/BAG_FILTER' A) P b))))).
tt('thm/bag/BAG_INN_BAG_FILTER_', ax, ![A : $t]: (![n : 'type/num/num', e : A, b : (A > 'type/num/num'), P : (A > $o)]: ((('const/bag/BAG_INN' A) e n (('const/bag/BAG_FILTER' A) P b)) = ((n = 'const/num/0') | ((P e) & (('const/bag/BAG_INN' A) e n b)))))).
tt('thm/bag/BAG_IN_BAG_FILTER_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num'), P : (A > $o)]: ((('const/bag/BAG_IN' A) e (('const/bag/BAG_FILTER' A) P b)) = ((P e) & (('const/bag/BAG_IN' A) e b))))).
tt('thm/bag/BAG_FILTER_FILTER_', ax, ![A : $t]: (![b : (A > 'type/num/num'), Q : (A > $o), P : (A > $o)]: ((('const/bag/BAG_FILTER' A) P (('const/bag/BAG_FILTER' A) Q b)) = (('const/bag/BAG_FILTER' A) (^[a : A]: ((P a) & (Q a))) b)))).
tt('thm/bag/BAG_FILTER_SUB_BAG_', ax, ![A : $t]: (![P : (A > $o), b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) (('const/bag/BAG_FILTER' A) P b) b))).
tt('thm/bag/SET_OF_BAG_EQ_INSERT_', ax, ![A : $t]: (![b : (A > 'type/num/num'), e : A, s : (A > $o)]: (((('const/pred_set/INSERT' A) e s) = (('const/bag/SET_OF_BAG' A) b)) = (?[b0 : (A > 'type/num/num'), eb : (A > 'type/num/num')]: ((b = (('const/bag/BAG_UNION' A) eb b0)) & ((s = (('const/bag/SET_OF_BAG' A) b0)) & ((!['e\'' : A]: ((('const/bag/BAG_IN' A) 'e\'' eb) => ('e\'' = e))) & ((~ (('const/bool/IN' A) e s)) => (('const/bag/BAG_IN' A) e eb))))))))).
tt('thm/bag/FINITE_SET_OF_BAG_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/pred_set/FINITE' A) (('const/bag/SET_OF_BAG' A) b)) = (('const/bag/FINITE_BAG' A) b)))).
tt('thm/bag/BAG_IMAGE_DEF_', def, ![B : $t, A : $t]: (![f : (B > A), b : (B > 'type/num/num')]: ((('const/bag/BAG_IMAGE' A B) f b) = (^[e : A]: (('const/bool/LET' (B > 'type/num/num') 'type/num/num') (^[sb : (B > 'type/num/num')]: (('const/bool/COND' 'type/num/num') (('const/bag/FINITE_BAG' B) sb) (('const/bag/BAG_CARD' B) sb) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/bag/BAG_FILTER' B) (^[e0 : B]: ((f e0) = e)) b)))))).
tt('thm/bag/BAG_IMAGE_EMPTY_', ax, ![B : $t, A : $t]: (![f : (A > B)]: ((('const/bag/BAG_IMAGE' B A) f ('const/bag/EMPTY_BAG' A)) = ('const/bag/EMPTY_BAG' B)))).
tt('thm/bag/BAG_IMAGE_FINITE_INSERT_', ax, ![A : $t, B : $t]: (![b : (A > 'type/num/num'), f : (A > B), e : A]: ((('const/bag/FINITE_BAG' A) b) => ((('const/bag/BAG_IMAGE' B A) f (('const/bag/BAG_INSERT' A) e b)) = (('const/bag/BAG_INSERT' B) (f e) (('const/bag/BAG_IMAGE' B A) f b)))))).
tt('thm/bag/BAG_IMAGE_FINITE_UNION_', ax, ![A : $t, B : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), f : (A > B)]: (((('const/bag/FINITE_BAG' A) b1) & (('const/bag/FINITE_BAG' A) b2)) => ((('const/bag/BAG_IMAGE' B A) f (('const/bag/BAG_UNION' A) b1 b2)) = (('const/bag/BAG_UNION' B) (('const/bag/BAG_IMAGE' B A) f b1) (('const/bag/BAG_IMAGE' B A) f b2)))))).
tt('thm/bag/BAG_IMAGE_FINITE_', ax, ![A : $t, B : $t]: (![f : (A > B), b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (('const/bag/FINITE_BAG' B) (('const/bag/BAG_IMAGE' B A) f b))))).
tt('thm/bag/BAG_IMAGE_COMPOSE_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), g : (C > A), b : (C > 'type/num/num')]: ((('const/bag/FINITE_BAG' C) b) => ((('const/bag/BAG_IMAGE' B C) (('const/combin/o' C B A) f g) b) = (('const/bag/BAG_IMAGE' B A) f (('const/bag/BAG_IMAGE' A C) g b)))))).
tt('thm/bag/BAG_IMAGE_FINITE_I_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => ((('const/bag/BAG_IMAGE' A A) ('const/combin/I' A) b) = b)))).
tt('thm/bag/BAG_IN_FINITE_BAG_IMAGE_', ax, ![A : $t, B : $t]: (![x : B, f : (A > B), b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => ((('const/bag/BAG_IN' B) x (('const/bag/BAG_IMAGE' B A) f b)) = (?[y : A]: (((f y) = x) & (('const/bag/BAG_IN' A) y b))))))).
tt('thm/bag/BAG_IMAGE_EQ_EMPTY_', ax, ![A : $t, B : $t]: (![f : (A > B), b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => (((('const/bag/BAG_IMAGE' B A) f b) = ('const/bag/EMPTY_BAG' B)) = (b = ('const/bag/EMPTY_BAG' A)))))).
tt('thm/bag/BAG_CHOICE_DEF_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((~ (b = ('const/bag/EMPTY_BAG' A))) => (('const/bag/BAG_IN' A) (('const/bag/BAG_CHOICE' A) b) b)))).
tt('thm/bag/BAG_REST_DEF_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_REST' A) b) = (('const/bag/BAG_DIFF' A) b (('const/bag/EL_BAG' A) (('const/bag/BAG_CHOICE' A) b)))))).
tt('thm/bag/BAG_INSERT_CHOICE_REST_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((~ (b = ('const/bag/EMPTY_BAG' A))) => (b = (('const/bag/BAG_INSERT' A) (('const/bag/BAG_CHOICE' A) b) (('const/bag/BAG_REST' A) b)))))).
tt('thm/bag/BAG_CHOICE_SING_', ax, ![A : $t]: (![x : A]: ((('const/bag/BAG_CHOICE' A) (('const/bag/BAG_INSERT' A) x ('const/bag/EMPTY_BAG' A))) = x))).
tt('thm/bag/BAG_REST_SING_', ax, ![A : $t]: (![x : A]: ((('const/bag/BAG_REST' A) (('const/bag/BAG_INSERT' A) x ('const/bag/EMPTY_BAG' A))) = ('const/bag/EMPTY_BAG' A)))).
tt('thm/bag/SUB_BAG_REST_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) (('const/bag/BAG_REST' A) b) b))).
tt('thm/bag/PSUB_BAG_REST_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((~ (b = ('const/bag/EMPTY_BAG' A))) => (('const/bag/PSUB_BAG' A) (('const/bag/BAG_REST' A) b) b)))).
tt('thm/bag/SUB_BAG_UNION_MONO_0', ax, ![A : $t]: (![x : (A > 'type/num/num'), y : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) x (('const/bag/BAG_UNION' A) x y)))).
tt('thm/bag/SUB_BAG_UNION_MONO_e1', ax, ![A : $t]: (![x : (A > 'type/num/num'), y : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) x (('const/bag/BAG_UNION' A) y x)))).
tt('thm/bag/PSUB_BAG_CARD_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b2) & (('const/bag/PSUB_BAG' A) b1 b2)) => ('const/prim_rec/<' (('const/bag/BAG_CARD' A) b1) (('const/bag/BAG_CARD' A) b2))))).
tt('thm/bag/EL_BAG_BAG_INSERT_', ax, ![A : $t]: (![y : A, x : A, b : (A > 'type/num/num')]: (((('const/bag/BAG_INSERT' A) x ('const/bag/EMPTY_BAG' A)) = (('const/bag/BAG_INSERT' A) y b)) = ((x = y) & (b = ('const/bag/EMPTY_BAG' A)))))).
tt('thm/bag/EL_BAG_SUB_BAG_', ax, ![A : $t]: (![x : A, b : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_INSERT' A) x ('const/bag/EMPTY_BAG' A)) b) = (('const/bag/BAG_IN' A) x b)))).
tt('thm/bag/ITBAG_tupled_primitive_def_', def, ![B : $t, A : $t]: (![f : (A > (B > B))]: ((('const/bag/ITBAG_tupled' A B) f) = (('const/relation/WFREC' ('type/pair/prod' (A > 'type/num/num') B) B) (('const/min/@' (('type/pair/prod' (A > 'type/num/num') B) > (('type/pair/prod' (A > 'type/num/num') B) > $o))) (^[R : (('type/pair/prod' (A > 'type/num/num') B) > (('type/pair/prod' (A > 'type/num/num') B) > $o))]: ((('const/relation/WF' ('type/pair/prod' (A > 'type/num/num') B)) R) & (![acc : B, b : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b) & (~ (b = ('const/bag/EMPTY_BAG' A)))) => (R (('const/pair/,' (A > 'type/num/num') B) (('const/bag/BAG_REST' A) b) (f (('const/bag/BAG_CHOICE' A) b) acc)) (('const/pair/,' (A > 'type/num/num') B) b acc))))))) (^[ITBAG_tupled : (('type/pair/prod' (A > 'type/num/num') B) > B), a : ('type/pair/prod' (A > 'type/num/num') B)]: (('const/pair/pair_CASE' B (A > 'type/num/num') B) a (^[b : (A > 'type/num/num'), acc : B]: (('const/combin/I' B) (('const/bool/COND' B) (('const/bag/FINITE_BAG' A) b) (('const/bool/COND' B) (b = ('const/bag/EMPTY_BAG' A)) acc (ITBAG_tupled (('const/pair/,' (A > 'type/num/num') B) (('const/bag/BAG_REST' A) b) (f (('const/bag/BAG_CHOICE' A) b) acc)))) ('const/bool/ARB' B)))))))))).
tt('thm/bag/ITBAG_curried_def_', def, ![B : $t, A : $t]: (![f : (A > (B > B)), x : (A > 'type/num/num'), x1 : B]: ((('const/bag/ITBAG' A B) f x x1) = (('const/bag/ITBAG_tupled' A B) f (('const/pair/,' (A > 'type/num/num') B) x x1))))).
tt('thm/bag/ITBAG_IND_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), P : ((A > 'type/num/num') > (B > $o))]: ((![b : (A > 'type/num/num'), acc : B]: ((((('const/bag/FINITE_BAG' A) b) & (~ (b = ('const/bag/EMPTY_BAG' A)))) => (P (('const/bag/BAG_REST' A) b) (f (('const/bag/BAG_CHOICE' A) b) acc))) => (P b acc))) => (![v : (A > 'type/num/num'), v1 : B]: (P v v1))))).
tt('thm/bag/ITBAG_THM_', ax, ![B : $t, A : $t]: (![b : (A > 'type/num/num'), f : (A > (B > B)), acc : B]: ((('const/bag/FINITE_BAG' A) b) => ((('const/bag/ITBAG' A B) f b acc) = (('const/bool/COND' B) (b = ('const/bag/EMPTY_BAG' A)) acc (('const/bag/ITBAG' A B) f (('const/bag/BAG_REST' A) b) (f (('const/bag/BAG_CHOICE' A) b) acc))))))).
tt('thm/bag/ITBAG_EMPTY_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), acc : B]: ((('const/bag/ITBAG' A B) f ('const/bag/EMPTY_BAG' A) acc) = acc))).
tt('thm/bag/ITBAG_INSERT_', ax, ![B : $t, A : $t]: (![x : A, b : (A > 'type/num/num'), f : (A > (B > B)), acc : B]: ((('const/bag/FINITE_BAG' A) b) => ((('const/bag/ITBAG' A B) f (('const/bag/BAG_INSERT' A) x b) acc) = (('const/bag/ITBAG' A B) f (('const/bag/BAG_REST' A) (('const/bag/BAG_INSERT' A) x b)) (f (('const/bag/BAG_CHOICE' A) (('const/bag/BAG_INSERT' A) x b)) acc)))))).
tt('thm/bag/COMMUTING_ITBAG_INSERT_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), b : (A > 'type/num/num')]: (((![x : A, y : A, z : B]: ((f x (f y z)) = (f y (f x z)))) & (('const/bag/FINITE_BAG' A) b)) => (![x : A, a : B]: ((('const/bag/ITBAG' A B) f (('const/bag/BAG_INSERT' A) x b) a) = (('const/bag/ITBAG' A B) f b (f x a))))))).
tt('thm/bag/COMMUTING_ITBAG_RECURSES_', ax, ![B : $t, A : $t]: (![f : (A > (B > B)), e : A, b : (A > 'type/num/num'), a : B]: (((![x : A, y : A, z : B]: ((f x (f y z)) = (f y (f x z)))) & (('const/bag/FINITE_BAG' A) b)) => ((('const/bag/ITBAG' A B) f (('const/bag/BAG_INSERT' A) e b) a) = (f e (('const/bag/ITBAG' A B) f b a)))))).
tt('thm/bag/BAG_GEN_SUM_def_', def, (![bag : ('type/num/num' > 'type/num/num'), n : 'type/num/num']: (('const/bag/BAG_GEN_SUM' bag n) = (('const/bag/ITBAG' 'type/num/num' 'type/num/num') 'const/arithmetic/+' bag n)))).
tt('thm/bag/BAG_GEN_PROD_def_', def, (![bag : ('type/num/num' > 'type/num/num'), n : 'type/num/num']: (('const/bag/BAG_GEN_PROD' bag n) = (('const/bag/ITBAG' 'type/num/num' 'type/num/num') 'const/arithmetic/*' bag n)))).
tt('thm/bag/BAG_GEN_SUM_EMPTY_', ax, (![n : 'type/num/num']: (('const/bag/BAG_GEN_SUM' ('const/bag/EMPTY_BAG' 'type/num/num') n) = n))).
tt('thm/bag/BAG_GEN_PROD_EMPTY_', ax, (![n : 'type/num/num']: (('const/bag/BAG_GEN_PROD' ('const/bag/EMPTY_BAG' 'type/num/num') n) = n))).
tt('thm/bag/BAG_GEN_SUM_TAILREC_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => (![x : 'type/num/num', a : 'type/num/num']: (('const/bag/BAG_GEN_SUM' (('const/bag/BAG_INSERT' 'type/num/num') x b) a) = ('const/bag/BAG_GEN_SUM' b ('const/arithmetic/+' x a))))))).
tt('thm/bag/BAG_GEN_SUM_REC_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => (![x : 'type/num/num', a : 'type/num/num']: (('const/bag/BAG_GEN_SUM' (('const/bag/BAG_INSERT' 'type/num/num') x b) a) = ('const/arithmetic/+' x ('const/bag/BAG_GEN_SUM' b a))))))).
tt('thm/bag/BAG_GEN_PROD_TAILREC_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => (![x : 'type/num/num', a : 'type/num/num']: (('const/bag/BAG_GEN_PROD' (('const/bag/BAG_INSERT' 'type/num/num') x b) a) = ('const/bag/BAG_GEN_PROD' b ('const/arithmetic/*' x a))))))).
tt('thm/bag/BAG_GEN_PROD_REC_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => (![x : 'type/num/num', a : 'type/num/num']: (('const/bag/BAG_GEN_PROD' (('const/bag/BAG_INSERT' 'type/num/num') x b) a) = ('const/arithmetic/*' x ('const/bag/BAG_GEN_PROD' b a))))))).
tt('thm/bag/BAG_GEN_PROD_EQ_1_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => (![e : 'type/num/num']: ((('const/bag/BAG_GEN_PROD' b e) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) => (e = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/bag/BAG_GEN_PROD_ALL_ONES_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => ((('const/bag/BAG_GEN_PROD' b ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) => (![x : 'type/num/num']: ((('const/bag/BAG_IN' 'type/num/num') x b) => (x = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/bag/BAG_GEN_PROD_POSITIVE_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b) => ((![x : 'type/num/num']: ((('const/bag/BAG_IN' 'type/num/num') x b) => ('const/prim_rec/<' 'const/num/0' x))) => ('const/prim_rec/<' 'const/num/0' ('const/bag/BAG_GEN_PROD' b ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/bag/BAG_EVERY_', def, ![A : $t]: (![P : (A > $o), b : (A > 'type/num/num')]: ((('const/bag/BAG_EVERY' A) P b) = (![e : A]: ((('const/bag/BAG_IN' A) e b) => (P e)))))).
tt('thm/bag/BAG_EVERY_THM_0', ax, ![A : $t]: (![P : (A > $o)]: (('const/bag/BAG_EVERY' A) P ('const/bag/EMPTY_BAG' A)))).
tt('thm/bag/BAG_EVERY_THM_e1', ax, ![B : $t]: (![P : (B > $o), e : B, b : (B > 'type/num/num')]: ((('const/bag/BAG_EVERY' B) P (('const/bag/BAG_INSERT' B) e b)) = ((P e) & (('const/bag/BAG_EVERY' B) P b))))).
tt('thm/bag/BAG_EVERY_UNION_', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num'), P : (A > $o)]: ((('const/bag/BAG_EVERY' A) P (('const/bag/BAG_UNION' A) b1 b2)) = ((('const/bag/BAG_EVERY' A) P b1) & (('const/bag/BAG_EVERY' A) P b2))))).
tt('thm/bag/BAG_EVERY_MERGE_', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num'), P : (A > $o)]: ((('const/bag/BAG_EVERY' A) P (('const/bag/BAG_MERGE' A) b1 b2)) = ((('const/bag/BAG_EVERY' A) P b1) & (('const/bag/BAG_EVERY' A) P b2))))).
tt('thm/bag/BAG_EVERY_SET_', ax, ![A : $t]: (![b : (A > 'type/num/num'), P : (A > $o)]: ((('const/bag/BAG_EVERY' A) P b) = (('const/pred_set/SUBSET' A) (('const/bag/SET_OF_BAG' A) b) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (P x)))))))).
tt('thm/bag/BAG_FILTER_EQ_EMPTY_', ax, ![A : $t]: (![b : (A > 'type/num/num'), P : (A > $o)]: (((('const/bag/BAG_FILTER' A) P b) = ('const/bag/EMPTY_BAG' A)) = (('const/bag/BAG_EVERY' A) (('const/combin/o' A $o $o) $not P) b)))).
tt('thm/bag/SET_OF_BAG_IMAGE_', ax, ![B : $t, A : $t]: (![f : (B > A), b : (B > 'type/num/num')]: ((('const/bag/SET_OF_BAG' A) (('const/bag/BAG_IMAGE' A B) f b)) = (('const/pred_set/IMAGE' B A) f (('const/bag/SET_OF_BAG' B) b))))).
tt('thm/bag/BAG_IMAGE_FINITE_RESTRICTED_I_', ax, ![A : $t]: (![f : (A > A), b : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b) & (('const/bag/BAG_EVERY' A) (^[e : A]: ((f e) = e)) b)) => ((('const/bag/BAG_IMAGE' A A) f b) = b)))).
tt('thm/bag/BAG_ALL_DISTINCT_', def, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) b) = (![e : A]: ('const/arithmetic/<=' (b e) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/bag/BAG_ALL_DISTINCT_THM_0', ax, ![A : $t]: (('const/bag/BAG_ALL_DISTINCT' A) ('const/bag/EMPTY_BAG' A))).
tt('thm/bag/BAG_ALL_DISTINCT_THM_e1', ax, ![B : $t]: (![e : B, b : (B > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' B) (('const/bag/BAG_INSERT' B) e b)) = ((~ (('const/bag/BAG_IN' B) e b)) & (('const/bag/BAG_ALL_DISTINCT' B) b))))).
tt('thm/bag/BAG_ALL_DISTINCT_BAG_MERGE_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) (('const/bag/BAG_MERGE' A) b1 b2)) = ((('const/bag/BAG_ALL_DISTINCT' A) b1) & (('const/bag/BAG_ALL_DISTINCT' A) b2))))).
tt('thm/bag/BAG_ALL_DISTINCT_BAG_UNION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) (('const/bag/BAG_UNION' A) b1 b2)) = ((('const/bag/BAG_ALL_DISTINCT' A) b1) & ((('const/bag/BAG_ALL_DISTINCT' A) b2) & (('const/bag/BAG_DISJOINT' A) b1 b2)))))).
tt('thm/bag/BAG_ALL_DISTINCT_DIFF_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) b1) => (('const/bag/BAG_ALL_DISTINCT' A) (('const/bag/BAG_DIFF' A) b1 b2))))).
tt('thm/bag/BAG_ALL_DISTINCT_DELETE_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) b) = (![e : A]: ((('const/bag/BAG_IN' A) e b) => (~ (('const/bag/BAG_IN' A) e (('const/bag/BAG_DIFF' A) b (('const/bag/BAG_INSERT' A) e ('const/bag/EMPTY_BAG' A)))))))))).
tt('thm/bag/BAG_ALL_DISTINCT_SET_', ax, ![A : $t]: (![b : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) b) = ((('const/bag/BAG_OF_SET' A) (('const/bag/SET_OF_BAG' A) b)) = b)))).
tt('thm/bag/BAG_ALL_DISTINCT_BAG_OF_SET_', ax, ![A : $t]: (![s : (A > $o)]: (('const/bag/BAG_ALL_DISTINCT' A) (('const/bag/BAG_OF_SET' A) s)))).
tt('thm/bag/BAG_IN_BAG_DIFF_ALL_DISTINCT_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num'), e : A]: ((('const/bag/BAG_ALL_DISTINCT' A) b1) => ((('const/bag/BAG_IN' A) e (('const/bag/BAG_DIFF' A) b1 b2)) = ((('const/bag/BAG_IN' A) e b1) & (~ (('const/bag/BAG_IN' A) e b2))))))).
tt('thm/bag/SUB_BAG_ALL_DISTINCT_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/BAG_ALL_DISTINCT' A) b1) => ((('const/bag/SUB_BAG' A) b1 b2) = (![x : A]: ((('const/bag/BAG_IN' A) x b1) => (('const/bag/BAG_IN' A) x b2))))))).
tt('thm/bag/BAG_ALL_DISTINCT_BAG_INN_', ax, ![A : $t]: (![b : (A > 'type/num/num'), n : 'type/num/num', e : A]: ((('const/bag/BAG_ALL_DISTINCT' A) b) => ((('const/bag/BAG_INN' A) e n b) = ((n = 'const/num/0') | ((n = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (('const/bag/BAG_IN' A) e b))))))).
tt('thm/bag/BAG_ALL_DISTINCT_EXTENSION_', ax, ![A : $t]: (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: (((('const/bag/BAG_ALL_DISTINCT' A) b1) & (('const/bag/BAG_ALL_DISTINCT' A) b2)) => ((b1 = b2) = (![x : A]: ((('const/bag/BAG_IN' A) x b1) = (('const/bag/BAG_IN' A) x b2))))))).
tt('thm/bag/NOT_BAG_IN_', ax, ![A : $t]: (![b : (A > 'type/num/num'), x : A]: (((b x) = 'const/num/0') = (~ (('const/bag/BAG_IN' A) x b))))).
tt('thm/bag/BAG_UNION_EQ_LEFT_', ax, ![A : $t]: (![b : (A > 'type/num/num'), c : (A > 'type/num/num'), d : (A > 'type/num/num')]: (((('const/bag/BAG_UNION' A) b c) = (('const/bag/BAG_UNION' A) b d)) => (c = d)))).
tt('thm/bag/BAG_IN_DIVIDES_', ax, (![b : ('type/num/num' > 'type/num/num'), x : 'type/num/num', a : 'type/num/num']: (((('const/bag/FINITE_BAG' 'type/num/num') b) & (('const/bag/BAG_IN' 'type/num/num') x b)) => ('const/divides/divides' x ('const/bag/BAG_GEN_PROD' b a))))).
tt('thm/bag/BAG_GEN_PROD_UNION_LEM_', ax, (![b1 : ('type/num/num' > 'type/num/num')]: ((('const/bag/FINITE_BAG' 'type/num/num') b1) => (![b2 : ('type/num/num' > 'type/num/num'), a : 'type/num/num', b : 'type/num/num']: ((('const/bag/FINITE_BAG' 'type/num/num') b2) => (('const/bag/BAG_GEN_PROD' (('const/bag/BAG_UNION' 'type/num/num') b1 b2) ('const/arithmetic/*' a b)) = ('const/arithmetic/*' ('const/bag/BAG_GEN_PROD' b1 a) ('const/bag/BAG_GEN_PROD' b2 b)))))))).
tt('thm/bag/BAG_GEN_PROD_UNION_', ax, (![b1 : ('type/num/num' > 'type/num/num'), b2 : ('type/num/num' > 'type/num/num')]: (((('const/bag/FINITE_BAG' 'type/num/num') b1) & (('const/bag/FINITE_BAG' 'type/num/num') b2)) => (('const/bag/BAG_GEN_PROD' (('const/bag/BAG_UNION' 'type/num/num') b1 b2) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ('const/arithmetic/*' ('const/bag/BAG_GEN_PROD' b1 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/bag/BAG_GEN_PROD' b2 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/bag/BIG_BAG_UNION_def_', def, ![A : $t]: (![sob : ((A > 'type/num/num') > $o)]: ((('const/bag/BIG_BAG_UNION' A) sob) = (^[x : A]: (('const/pred_set/SUM_IMAGE' (A > 'type/num/num')) (^[b : (A > 'type/num/num')]: (b x)) sob))))).
tt('thm/bag/BIG_BAG_UNION_EMPTY_', ax, ![A : $t]: ((('const/bag/BIG_BAG_UNION' A) ('const/pred_set/EMPTY' (A > 'type/num/num'))) = ('const/bag/EMPTY_BAG' A))).
tt('thm/bag/BIG_BAG_UNION_INSERT_', ax, ![A : $t]: (![sob : ((A > 'type/num/num') > $o), b : (A > 'type/num/num')]: ((('const/pred_set/FINITE' (A > 'type/num/num')) sob) => ((('const/bag/BIG_BAG_UNION' A) (('const/pred_set/INSERT' (A > 'type/num/num')) b sob)) = (('const/bag/BAG_UNION' A) b (('const/bag/BIG_BAG_UNION' A) (('const/pred_set/DELETE' (A > 'type/num/num')) sob b))))))).
tt('thm/bag/BIG_BAG_UNION_DELETE_', ax, ![A : $t]: (![sob : ((A > 'type/num/num') > $o), b : (A > 'type/num/num')]: ((('const/pred_set/FINITE' (A > 'type/num/num')) sob) => ((('const/bag/BIG_BAG_UNION' A) (('const/pred_set/DELETE' (A > 'type/num/num')) sob b)) = (('const/bool/COND' (A > 'type/num/num')) (('const/bool/IN' (A > 'type/num/num')) b sob) (('const/bag/BAG_DIFF' A) (('const/bag/BIG_BAG_UNION' A) sob) b) (('const/bag/BIG_BAG_UNION' A) sob)))))).
tt('thm/bag/BIG_BAG_UNION_ITSET_BAG_UNION_', ax, ![A : $t]: (![sob : ((A > 'type/num/num') > $o)]: ((('const/pred_set/FINITE' (A > 'type/num/num')) sob) => ((('const/bag/BIG_BAG_UNION' A) sob) = (('const/pred_set/ITSET' (A > 'type/num/num') (A > 'type/num/num')) ('const/bag/BAG_UNION' A) sob ('const/bag/EMPTY_BAG' A)))))).
tt('thm/bag/FINITE_BIG_BAG_UNION_', ax, ![A : $t]: (![sob : ((A > 'type/num/num') > $o)]: (((('const/pred_set/FINITE' (A > 'type/num/num')) sob) & (![b : (A > 'type/num/num')]: ((('const/bool/IN' (A > 'type/num/num')) b sob) => (('const/bag/FINITE_BAG' A) b)))) => (('const/bag/FINITE_BAG' A) (('const/bag/BIG_BAG_UNION' A) sob))))).
tt('thm/bag/BAG_IN_BIG_BAG_UNION_', ax, ![A : $t]: (![e : A, P : ((A > 'type/num/num') > $o)]: ((('const/pred_set/FINITE' (A > 'type/num/num')) P) => ((('const/bag/BAG_IN' A) e (('const/bag/BIG_BAG_UNION' A) P)) = (?[b : (A > 'type/num/num')]: ((('const/bag/BAG_IN' A) e b) & (('const/bool/IN' (A > 'type/num/num')) b P))))))).
tt('thm/bag/BIG_BAG_UNION_EQ_EMPTY_BAG_', ax, ![A : $t]: (![sob : ((A > 'type/num/num') > $o)]: ((('const/pred_set/FINITE' (A > 'type/num/num')) sob) => (((('const/bag/BIG_BAG_UNION' A) sob) = ('const/bag/EMPTY_BAG' A)) = (![b : (A > 'type/num/num')]: ((('const/bool/IN' (A > 'type/num/num')) b sob) => (b = ('const/bag/EMPTY_BAG' A)))))))).
tt('thm/bag/BIG_BAG_UNION_UNION_', ax, ![A : $t]: (![s2 : ((A > 'type/num/num') > $o), s1 : ((A > 'type/num/num') > $o)]: (((('const/pred_set/FINITE' (A > 'type/num/num')) s1) & (('const/pred_set/FINITE' (A > 'type/num/num')) s2)) => ((('const/bag/BIG_BAG_UNION' A) (('const/pred_set/UNION' (A > 'type/num/num')) s1 s2)) = (('const/bag/BAG_DIFF' A) (('const/bag/BAG_UNION' A) (('const/bag/BIG_BAG_UNION' A) s1) (('const/bag/BIG_BAG_UNION' A) s2)) (('const/bag/BIG_BAG_UNION' A) (('const/pred_set/INTER' (A > 'type/num/num')) s1 s2))))))).
tt('thm/bag/BIG_BAG_UNION_EQ_ELEMENT_', ax, ![A : $t]: (![sob : ((A > 'type/num/num') > $o), b : (A > 'type/num/num')]: (((('const/pred_set/FINITE' (A > 'type/num/num')) sob) & (('const/bool/IN' (A > 'type/num/num')) b sob)) => (((('const/bag/BIG_BAG_UNION' A) sob) = b) = (!['b\'' : (A > 'type/num/num')]: ((('const/bool/IN' (A > 'type/num/num')) 'b\'' sob) => (('b\'' = b) | ('b\'' = ('const/bag/EMPTY_BAG' A))))))))).
tt('thm/bag/mlt1_def_', def, ![A : $t]: (![r : (A > (A > $o)), b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/bag/mlt1' A) r b1 b2) = ((('const/bag/FINITE_BAG' A) b1) & ((('const/bag/FINITE_BAG' A) b2) & (?[e : A, rep : (A > 'type/num/num'), res : (A > 'type/num/num')]: ((b1 = (('const/bag/BAG_UNION' A) rep res)) & ((b2 = (('const/bag/BAG_UNION' A) res (('const/bag/BAG_INSERT' A) e ('const/bag/EMPTY_BAG' A)))) & (!['e\'' : A]: ((('const/bag/BAG_IN' A) 'e\'' rep) => (r 'e\'' e))))))))))).
tt('thm/bag/BAG_NOT_LESS_EMPTY_', ax, ![A : $t]: (![r : (A > (A > $o)), b : (A > 'type/num/num')]: (~ (('const/bag/mlt1' A) r b ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/NOT_mlt_EMPTY_', ax, ![A : $t]: (![b : (A > 'type/num/num'), R : (A > (A > $o))]: (~ (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b ('const/bag/EMPTY_BAG' A))))).
tt('thm/bag/BAG_LESS_ADD_', ax, ![A : $t]: (![r : (A > (A > $o)), a : A, N : (A > 'type/num/num'), M0 : (A > 'type/num/num')]: ((('const/bag/mlt1' A) r N (('const/bag/BAG_UNION' A) M0 (('const/bag/BAG_INSERT' A) a ('const/bag/EMPTY_BAG' A)))) => ((?[M : (A > 'type/num/num')]: ((('const/bag/mlt1' A) r M M0) & (N = (('const/bag/BAG_UNION' A) M (('const/bag/BAG_INSERT' A) a ('const/bag/EMPTY_BAG' A)))))) | (?[KK : (A > 'type/num/num')]: ((![b : A]: ((('const/bag/BAG_IN' A) b KK) => (r b a))) & (N = (('const/bag/BAG_UNION' A) M0 KK)))))))).
tt('thm/bag/mlt1_all_accessible_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/relation/WF' A) R) => (![M : (A > 'type/num/num')]: (('const/relation/WFP' (A > 'type/num/num')) (('const/bag/mlt1' A) R) M))))).
tt('thm/bag/WF_mlt1_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/relation/WF' A) R) => (('const/relation/WF' (A > 'type/num/num')) (('const/bag/mlt1' A) R))))).
tt('thm/bag/TC_mlt1_FINITE_BAG_', ax, ![A : $t]: (![R : (A > (A > $o)), b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b1 b2) => ((('const/bag/FINITE_BAG' A) b1) & (('const/bag/FINITE_BAG' A) b2))))).
tt('thm/bag/TC_mlt1_UNION2_I_', ax, ![A : $t]: (![R : (A > (A > $o)), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b2) & ((('const/bag/FINITE_BAG' A) b1) & (~ (b2 = ('const/bag/EMPTY_BAG' A))))) => (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b1 (('const/bag/BAG_UNION' A) b1 b2))))).
tt('thm/bag/TC_mlt1_UNION1_I_', ax, ![A : $t]: (![R : (A > (A > $o)), b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b2) & ((('const/bag/FINITE_BAG' A) b1) & (~ (b1 = ('const/bag/EMPTY_BAG' A))))) => (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b2 (('const/bag/BAG_UNION' A) b1 b2))))).
tt('thm/bag/mlt_NOT_REFL_', ax, ![A : $t]: (![a : (A > 'type/num/num'), R : (A > (A > $o))]: ((('const/relation/WF' A) R) => (~ (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a a))))).
tt('thm/bag/mlt_INSERT_CANCEL_I_', ax, ![A : $t]: (![e : A, R : (A > (A > $o)), a : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a b) => (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) (('const/bag/BAG_INSERT' A) e a) (('const/bag/BAG_INSERT' A) e b))))).
tt('thm/bag/mlt1_INSERT_CANCEL_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num'), a : (A > 'type/num/num'), R : (A > (A > $o))]: ((('const/relation/WF' A) R) => ((('const/bag/mlt1' A) R (('const/bag/BAG_INSERT' A) e a) (('const/bag/BAG_INSERT' A) e b)) = (('const/bag/mlt1' A) R a b))))).
tt('thm/bag/dominates_def_', def, ![B : $t, A : $t]: (![R : (A > (B > $o)), s1 : (A > $o), s2 : (B > $o)]: ((('const/bag/dominates' A B) R s1 s2) = (![x : A]: ((('const/bool/IN' A) x s1) => (?[y : B]: ((('const/bool/IN' B) y s2) & (R x y)))))))).
tt('thm/bag/dominates_EMPTY_', ax, ![B : $t, A : $t]: (![b : (B > $o), R : (A > (B > $o))]: (('const/bag/dominates' A B) R ('const/pred_set/EMPTY' A) b))).
tt('thm/bag/dominates_SUBSET_', ax, ![A : $t]: (![Y : (A > $o), X : (A > $o), R : (A > (A > $o))]: (((('const/relation/transitive' A) R) & ((('const/pred_set/FINITE' A) Y) & ((('const/bag/dominates' A A) R Y X) & ((('const/pred_set/SUBSET' A) X Y) & (~ (X = ('const/pred_set/EMPTY' A))))))) => (?[x : A]: ((('const/bool/IN' A) x X) & (R x x)))))).
tt('thm/bag/mlt_dominates_thm1_', ax, ![A : $t]: (![R : (A > (A > $o))]: ((('const/relation/transitive' A) R) => (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b1 b2) = ((('const/bag/FINITE_BAG' A) b1) & ((('const/bag/FINITE_BAG' A) b2) & (?[x : (A > 'type/num/num'), y : (A > 'type/num/num')]: ((~ (x = ('const/bag/EMPTY_BAG' A))) & ((('const/bag/SUB_BAG' A) x b2) & ((b1 = (('const/bag/BAG_UNION' A) (('const/bag/BAG_DIFF' A) b2 x) y)) & (('const/bag/dominates' A A) R (('const/bag/SET_OF_BAG' A) y) (('const/bag/SET_OF_BAG' A) x))))))))))))).
tt('thm/bag/dominates_DIFF_', ax, ![A : $t]: (![y : (A > $o), x : (A > $o), i : (A > $o), R : (A > (A > $o))]: (((('const/relation/WF' A) R) & ((('const/relation/transitive' A) R) & ((('const/bag/dominates' A A) R x y) & ((('const/pred_set/FINITE' A) i) & ((('const/pred_set/SUBSET' A) i x) & (('const/pred_set/SUBSET' A) i y)))))) => (('const/bag/dominates' A A) R (('const/pred_set/DIFF' A) x i) (('const/pred_set/DIFF' A) y i))))).
tt('thm/bag/BAG_INSERT_SUB_BAG_E_', ax, ![A : $t]: (![e : A, c : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) (('const/bag/BAG_INSERT' A) e b) c) => ((('const/bag/BAG_IN' A) e c) & (('const/bag/SUB_BAG' A) b c))))).
tt('thm/bag/bdominates_BAG_DIFF_', ax, ![A : $t]: (![y : (A > 'type/num/num'), x : (A > 'type/num/num'), i : (A > 'type/num/num'), R : (A > (A > $o))]: (((('const/relation/WF' A) R) & ((('const/relation/transitive' A) R) & ((('const/bag/dominates' A A) R (('const/bag/SET_OF_BAG' A) x) (('const/bag/SET_OF_BAG' A) y)) & ((('const/bag/FINITE_BAG' A) i) & ((('const/bag/SUB_BAG' A) i x) & (('const/bag/SUB_BAG' A) i y)))))) => (('const/bag/dominates' A A) R (('const/bag/SET_OF_BAG' A) (('const/bag/BAG_DIFF' A) x i)) (('const/bag/SET_OF_BAG' A) (('const/bag/BAG_DIFF' A) y i)))))).
tt('thm/bag/BAG_INTER_SUB_BAG_0', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) (('const/bag/BAG_INTER' A) b1 b2) b1))).
tt('thm/bag/BAG_INTER_SUB_BAG_e1', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) (('const/bag/BAG_INTER' A) b1 b2) b2))).
tt('thm/bag/BAG_INTER_FINITE_', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num')]: (((('const/bag/FINITE_BAG' A) b1) | (('const/bag/FINITE_BAG' A) b2)) => (('const/bag/FINITE_BAG' A) (('const/bag/BAG_INTER' A) b1 b2))))).
tt('thm/bag/mlt_dominates_thm2_', ax, ![A : $t]: (![R : (A > (A > $o))]: (((('const/relation/WF' A) R) & (('const/relation/transitive' A) R)) => (![b1 : (A > 'type/num/num'), b2 : (A > 'type/num/num')]: ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b1 b2) = ((('const/bag/FINITE_BAG' A) b1) & ((('const/bag/FINITE_BAG' A) b2) & (?[x : (A > 'type/num/num'), y : (A > 'type/num/num')]: ((~ (x = ('const/bag/EMPTY_BAG' A))) & ((('const/bag/SUB_BAG' A) x b2) & ((('const/bag/BAG_DISJOINT' A) x y) & ((b1 = (('const/bag/BAG_UNION' A) (('const/bag/BAG_DIFF' A) b2 x) y)) & (('const/bag/dominates' A A) R (('const/bag/SET_OF_BAG' A) y) (('const/bag/SET_OF_BAG' A) x)))))))))))))).
tt('thm/bag/BAG_DIFF_INSERT_SUB_BAG_', ax, ![A : $t]: (![e : A, c : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) c b) => ((('const/bag/BAG_DIFF' A) (('const/bag/BAG_INSERT' A) e b) c) = (('const/bag/BAG_INSERT' A) e (('const/bag/BAG_DIFF' A) b c)))))).
tt('thm/bag/mlt_INSERT_CANCEL_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num'), a : (A > 'type/num/num'), R : (A > (A > $o))]: (((('const/relation/transitive' A) R) & (('const/relation/WF' A) R)) => ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) (('const/bag/BAG_INSERT' A) e a) (('const/bag/BAG_INSERT' A) e b)) = (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a b))))).
tt('thm/bag/mlt_UNION_RCANCEL_I_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num'), a : (A > 'type/num/num'), R : (A > (A > $o))]: (((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a b) & (('const/bag/FINITE_BAG' A) c)) => (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) (('const/bag/BAG_UNION' A) a c) (('const/bag/BAG_UNION' A) b c))))).
tt('thm/bag/mlt_UNION_RCANCEL_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num'), a : (A > 'type/num/num'), R : (A > (A > $o))]: (((('const/relation/WF' A) R) & (('const/relation/transitive' A) R)) => ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) (('const/bag/BAG_UNION' A) a c) (('const/bag/BAG_UNION' A) b c)) = ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a b) & (('const/bag/FINITE_BAG' A) c)))))).
tt('thm/bag/mlt_UNION_LCANCEL_I_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num'), a : (A > 'type/num/num'), R : (A > (A > $o))]: (((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a b) & (('const/bag/FINITE_BAG' A) c)) => (('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) (('const/bag/BAG_UNION' A) c a) (('const/bag/BAG_UNION' A) c b))))).
tt('thm/bag/mlt_UNION_LCANCEL_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num'), a : (A > 'type/num/num'), R : (A > (A > $o))]: (((('const/relation/WF' A) R) & (('const/relation/transitive' A) R)) => ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) (('const/bag/BAG_UNION' A) c a) (('const/bag/BAG_UNION' A) c b)) = ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) a b) & (('const/bag/FINITE_BAG' A) c)))))).
tt('thm/bag/mlt_UNION_CANCEL_EQN_', ax, ![A : $t]: (![b2 : (A > 'type/num/num'), b1 : (A > 'type/num/num'), R : (A > (A > $o))]: ((('const/relation/WF' A) R) => (((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b1 (('const/bag/BAG_UNION' A) b1 b2)) = ((('const/bag/FINITE_BAG' A) b1) & ((('const/bag/FINITE_BAG' A) b2) & (~ (b2 = ('const/bag/EMPTY_BAG' A)))))) & ((('const/relation/TC' (A > 'type/num/num')) (('const/bag/mlt1' A) R) b1 (('const/bag/BAG_UNION' A) b2 b1)) = ((('const/bag/FINITE_BAG' A) b1) & ((('const/bag/FINITE_BAG' A) b2) & (~ (b2 = ('const/bag/EMPTY_BAG' A)))))))))).
tt('thm/bag/mlt_UNION_EMPTY_EQN_', ax, $true).
tt('thm/bag/SUB_BAG_SING_', ax, ![A : $t]: (![e : A, b : (A > 'type/num/num')]: ((('const/bag/SUB_BAG' A) b (('const/bag/BAG_INSERT' A) e ('const/bag/EMPTY_BAG' A))) = ((b = ('const/bag/EMPTY_BAG' A)) | (b = (('const/bag/BAG_INSERT' A) e ('const/bag/EMPTY_BAG' A))))))).
tt('thm/bag/SUB_BAG_DIFF_simple_', ax, ![A : $t]: (![c : (A > 'type/num/num'), b : (A > 'type/num/num')]: (('const/bag/SUB_BAG' A) (('const/bag/BAG_DIFF' A) b c) b))).
tt('thm/bag/mltLT_SING0_', ax, (![b : ('type/num/num' > 'type/num/num')]: ((('const/relation/TC' ('type/num/num' > 'type/num/num')) (('const/bag/mlt1' 'type/num/num') 'const/prim_rec/<') (('const/bag/BAG_INSERT' 'type/num/num') 'const/num/0' ('const/bag/EMPTY_BAG' 'type/num/num')) b) = ((('const/bag/FINITE_BAG' 'type/num/num') b) & ((~ (b = (('const/bag/BAG_INSERT' 'type/num/num') 'const/num/0' ('const/bag/EMPTY_BAG' 'type/num/num')))) & (~ (b = ('const/bag/EMPTY_BAG' 'type/num/num')))))))).
tt('thm/bag/bag_size_def_', def, ![A : $t]: (![eltsize : (A > 'type/num/num'), b : (A > 'type/num/num')]: ((('const/bag/bag_size' A) eltsize b) = (('const/bag/ITBAG' A 'type/num/num') (^[e : A, acc : 'type/num/num']: ('const/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (eltsize e)) acc)) b 'const/num/0')))).
tt('thm/bag/BAG_SIZE_EMPTY_', ax, ![A : $t]: (![eltsize : (A > 'type/num/num')]: ((('const/bag/bag_size' A) eltsize ('const/bag/EMPTY_BAG' A)) = 'const/num/0'))).
tt('thm/bag/BAG_SIZE_INSERT_', ax, ![A : $t]: (![eltsize : (A > 'type/num/num'), e : A, b : (A > 'type/num/num')]: ((('const/bag/FINITE_BAG' A) b) => ((('const/bag/bag_size' A) eltsize (('const/bag/BAG_INSERT' A) e b)) = ('const/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (eltsize e)) (('const/bag/bag_size' A) eltsize b)))))).
