include('Axioms/readerMonad+2.ax').
fof(mem_c_2Ebag_2EBAG__ALL__DISTINCT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__ALL__DISTINCT(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),bool)) ) )).
fof(mem_c_2Ebag_2EBAG__CARD,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__CARD(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ebag_2EBAG__CARD__RELn,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__CARD__RELn(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))) ) )).
fof(mem_c_2Ebag_2EBAG__CHOICE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__CHOICE(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),A_27a)) ) )).
fof(mem_c_2Ebag_2EBAG__DELETE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__DELETE(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,arr(arr(A_27a,ty_2Enum_2Enum),bool)))) ) )).
fof(mem_c_2Ebag_2EBAG__DIFF,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__DIFF(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ebag_2EBAG__DISJOINT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__DISJOINT(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),bool))) ) )).
fof(mem_c_2Ebag_2EBAG__EVERY,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__EVERY(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,ty_2Enum_2Enum),bool))) ) )).
fof(mem_c_2Ebag_2EBAG__FILTER,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__FILTER(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ebag_2EBAG__GEN__PROD,axiom,( mem(c_2Ebag_2EBAG__GEN__PROD,arr(arr(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Ebag_2EBAG__GEN__SUM,axiom,( mem(c_2Ebag_2EBAG__GEN__SUM,arr(arr(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Ebag_2EBAG__IMAGE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ebag_2EBAG__IMAGE(A_27a,A_27b),arr(arr(A_27b,A_27a),arr(arr(A_27b,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) ) )).
fof(mem_c_2Ebag_2EBAG__IN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__IN(A_27a),arr(A_27a,arr(arr(A_27a,ty_2Enum_2Enum),bool))) ) )).
fof(mem_c_2Ebag_2EBAG__INN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__INN(A_27a),arr(A_27a,arr(ty_2Enum_2Enum,arr(arr(A_27a,ty_2Enum_2Enum),bool)))) ) )).
fof(mem_c_2Ebag_2EBAG__INSERT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__INSERT(A_27a),arr(A_27a,arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ebag_2EBAG__INTER,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__INTER(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ebag_2EBAG__MERGE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__MERGE(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ebag_2EBAG__OF__SET,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__OF__SET(A_27a),arr(arr(A_27a,bool),arr(A_27a,ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ebag_2EBAG__REST,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__REST(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ebag_2EBAG__UNION,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBAG__UNION(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ebag_2EBIG__BAG__UNION,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EBIG__BAG__UNION(A_27a),arr(arr(arr(A_27a,ty_2Enum_2Enum),bool),arr(A_27a,ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ebag_2EEL__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EEL__BAG(A_27a),arr(A_27a,arr(A_27a,ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ebag_2EEMPTY__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EEMPTY__BAG(A_27a),arr(A_27a,ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ebag_2EFINITE__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EFINITE__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),bool)) ) )).
fof(mem_c_2Ebag_2EITBAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ebag_2EITBAG(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,A_27b)),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27b,A_27b)))) ) ) )).
fof(mem_c_2Ebag_2EPSUB__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2EPSUB__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),bool))) ) )).
fof(mem_c_2Ebag_2ESET__OF__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2ESET__OF__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(A_27a,bool))) ) )).
fof(mem_c_2Ebag_2ESING__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2ESING__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),bool)) ) )).
fof(mem_c_2Ebag_2ESUB__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2ESUB__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),bool))) ) )).
fof(mem_c_2Ebag_2Ebag__size,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2Ebag__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ebag_2Edominates,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ebag_2Edominates(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,bool)),arr(arr(A_27a,bool),arr(arr(A_27b,bool),bool)))) ) ) )).
fof(mem_c_2Ebag_2Emlt1,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebag_2Emlt1(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,ty_2Enum_2Enum),bool)))) ) )).
fof(ax_thm_2Ebag_2EEMPTY__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ebag_2EEMPTY__BAG(A_27a) = ap(c_2Ecombin_2EK(ty_2Enum_2Enum,A_27a),c_2Enum_2E0) ) ) )).
fof(conj_thm_2Ebag_2EEMPTY__BAG__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ( c_2Ebag_2EEMPTY__BAG(A_27a) = k(A_27a,c_2Enum_2E0) )))).
fof(ax_thm_2Ebag_2EBAG__INN,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V0e),V1n),V2b)) <=> p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(V2b,V0e)),V1n)) ) ) ) ) ) )).
fof(ax_thm_2Ebag_2ESUB__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) <=> ! [V2x] : ( mem(V2x,A_27a) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2x),V3n),V0b1)) => p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2x),V3n),V1b2)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Ebag_2EPSUB__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V1b2)) <=> ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) & ( ~~ ( V0b1 = V1b2 ) ) ) ) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__IN,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b)) <=> p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V0e),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V1b)) ) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__UNION,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b),V1c) = f960(A_27a,V0b,V1c) ) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__DIFF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b1),V1b2) = f961(A_27a,V0b1,V1b2) ) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__INSERT,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V1b) = f962(A_27a,V0e,V1b) ) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__cases,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ( V0b = c_2Ebag_2EEMPTY__BAG(A_27a) ) | ? [V1b0] : ( mem(V1b0,arr(A_27a,ty_2Enum_2Enum)) & ? [V2e] : ( mem(V2e,A_27a) & ( V0b = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e),V1b0) ) ) ) ) )))).
fof(ax_thm_2Ebag_2EBAG__INTER,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__INTER(A_27a),V0b1),V1b2) = f963(A_27a,V0b1,V1b2) ) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__MERGE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__MERGE(A_27a),V0b1),V1b2) = f964(A_27a,V1b2,V0b1) ) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__MERGE__IDEM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__MERGE(A_27a),V0b),V0b) = V0b ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),c_2Enum_2E0),V0b)) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__LESS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ( ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V2n),V0b)) & p(ap(ap(c_2Eprim__rec_2E_3C,V3m),V2n)) ) => p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V3m),V0b)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e1] : ( mem(V1e1,A_27a) => ! [V2e2] : ( mem(V2e2,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V1e1),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e2),V0b))) <=> ( ( V1e1 = V2e2 ) | p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V1e1),V0b)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e1] : ( mem(V2e1,A_27a) => ! [V3e2] : ( mem(V3e2,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e1),V0n),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V3e2),V1b))) <=> ( ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e1),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V1b)) & ( V2e1 = V3e2 ) ) | p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e1),V0n),V1b)) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__BAG__INSERT__STRONG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2e1] : ( mem(V2e1,A_27a) => ! [V3e2] : ( mem(V3e2,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e1),V1n),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V3e2),V0b))) <=> ( ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e1),ap(ap(c_2Earithmetic_2E_2D,V1n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0b)) & ( V2e1 = V3e2 ) ) | ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e1),V1n),V0b)) & ( ~~ ( V2e1 = V3e2 ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__EQ__LCANCEL1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ( ( V0b = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b),V1c) ) <=> ( V1c = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__EQ__RCANCEL1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ( ( V0b = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1c),V0b) ) <=> ( V1c = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2))) <=> ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),V0b1)) | p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),V1b2)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2b1] : ( mem(V2b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V3b2] : ( mem(V3b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V0n),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V2b1),V3b2))) <=> ? [V4m1] : ( mem(V4m1,ty_2Enum_2Enum) & ? [V5m2] : ( mem(V5m2,ty_2Enum_2Enum) & ( ( V0n = ap(ap(c_2Earithmetic_2E_2B,V4m1),V5m2) ) & ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V4m1),V2b1)) & p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V5m2),V3b2)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__BAG__MERGE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2b1] : ( mem(V2b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V3b2] : ( mem(V3b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V0n),ap(ap(c_2Ebag_2EBAG__MERGE(A_27a),V2b1),V3b2))) <=> ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V0n),V2b1)) | p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V1e),V0n),V3b2)) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__BAG__MERGE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),ap(ap(c_2Ebag_2EBAG__MERGE(A_27a),V1b1),V2b2))) <=> ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b1)) | p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V2b2)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__EXTENSION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( V0b1 = V1b2 ) <=> ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3e] : ( mem(V3e,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V3e),V2n),V0b1)) <=> p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V3e),V2n),V1b2)) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V1b1)),V2b2) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b1),V2b2)) ) & ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b1),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V2b2)) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b1),V2b2)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ~~ ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V1b) = V1b ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__NOT__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ~~ ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V1b) = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__ONE__ONE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2x),V0b1) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2x),V1b2) ) <=> ( V0b1 = V1b2 ) ) ) ) )))).
fof(conj_thm_2Ebag_2EC__BAG__INSERT__ONE__ONE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V2b) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1y),V2b) ) <=> ( V0x = V1y ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__commutes,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e1] : ( mem(V1e1,A_27a) => ! [V2e2] : ( mem(V2e2,A_27a) => ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e1),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e2),V0b)) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e2),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e1),V0b)) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DECOMPOSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b)) => ? [V2b_27] : ( mem(V2b_27,arr(A_27a,ty_2Enum_2Enum)) & ( V1b = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V2b_27) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__LEFT__CANCEL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b),V1b1) = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b),V2b2) ) <=> ( V1b1 = V2b2 ) ) ) ) )))).
fof(conj_thm_2Ebag_2ECOMM__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2) = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V0b1) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__RIGHT__CANCEL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b1),V0b) = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V2b2),V0b) ) <=> ( V1b1 = V2b2 ) ) ) ) )))).
fof(conj_thm_2Ebag_2EASSOC__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V2b3)) = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),V2b3) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ( ( ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b),c_2Ebag_2EEMPTY__BAG(A_27a)) = V0b ) ) ) & ( ( ! [V1b] : ( mem(V1b,arr(A_27b,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__UNION(A_27b),c_2Ebag_2EEMPTY__BAG(A_27b)),V1b) = V1b ) ) ) & ! [V2b1] : ( mem(V2b1,arr(A_27c,ty_2Enum_2Enum)) => ! [V3b2] : ( mem(V3b2,arr(A_27c,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__UNION(A_27c),V2b1),V3b2) = c_2Ebag_2EEMPTY__BAG(A_27c) ) <=> ( ( V2b1 = c_2Ebag_2EEMPTY__BAG(A_27c) ) & ( V3b2 = c_2Ebag_2EEMPTY__BAG(A_27c) ) ) ) ) ) ) )))))).
fof(ax_thm_2Ebag_2EBAG__DELETE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V1e),V2b)) <=> ( V0b0 = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e),V2b) ) ) ) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__DELETE__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ~~ p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)),V0e),V1b)) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__commutes,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V3e1] : ( mem(V3e1,A_27a) => ! [V4e2] : ( mem(V4e2,A_27a) => ( ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V3e1),V1b1)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V1b1),V4e2),V2b2)) ) => ? [V5b_27] : ( mem(V5b_27,arr(A_27a,ty_2Enum_2Enum)) & ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V4e2),V5b_27)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V5b_27),V3e1),V2b2)) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e1] : ( mem(V1e1,A_27a) => ! [V2e2] : ( mem(V2e2,A_27a) => ! [V3b1] : ( mem(V3b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V4b2] : ( mem(V4b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V1e1),V3b1)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V2e2),V4b2)) ) => ( ( V1e1 = V2e2 ) <=> ( V3b1 = V4b2 ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__BAG__DELETE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2e] : ( mem(V2e,A_27a) => ( ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e),V1n),V0b)) & p(ap(ap(c_2Earithmetic_2E_3E,V1n),c_2Enum_2E0)) ) => ? [V3b_27] : ( mem(V3b_27,arr(A_27a,ty_2Enum_2Enum)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b),V2e),V3b_27)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__BAG__DELETE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V1e),V0b)) => ? [V2b_27] : ( mem(V2b_27,arr(A_27a,ty_2Enum_2Enum)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b),V1e),V2b_27)) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2b1] : ( mem(V2b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V3b2] : ( mem(V3b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V2b1)),V1y),V3b2)) => ( ( ( V0x = V1y ) & ( V2b1 = V3b2 ) ) | ( ( ? [V4b3] : ( mem(V4b3,arr(A_27a,ty_2Enum_2Enum)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V2b1),V1y),V4b3)) ) ) & ( ~~ ( V0x = V1y ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__BAG__IN__up,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V2e),V1b)) => ! [V3e_27] : ( mem(V3e_27,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V3e_27),V1b)) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V3e_27),V0b0)) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__BAG__IN__down,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e1] : ( mem(V2e1,A_27a) => ! [V3e2] : ( mem(V3e2,A_27a) => ( ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V2e1),V1b)) & ( ( ~~ ( V2e1 = V3e2 ) ) & p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V3e2),V0b0)) ) ) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V3e2),V1b)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__BAG__IN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V2e),V1b)) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),V0b0)) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__concrete,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V2e),V1b)) <=> ( p(ap(ap(c_2Earithmetic_2E_3E,ap(V0b0,V2e)),c_2Enum_2E0)) & ( V1b = f965(A_27a,V2e,V0b0) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__DIFF__eliminate,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b),V1c)),V1c) = V0b ) & ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1c),V0b)),V1c) = V0b ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__EQUAL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,A_27a) => ! [V1M] : ( mem(V1M,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b] : ( mem(V2b,A_27a) => ! [V3N] : ( mem(V3N,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0a),V1M) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2b),V3N) ) <=> ( ( ( V1M = V3N ) & ( V0a = V2b ) ) | ? [V4k] : ( mem(V4k,arr(A_27a,ty_2Enum_2Enum)) & ( ( V1M = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2b),V4k) ) & ( V3N = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0a),V4k) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__TWICE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e1] : ( mem(V1e1,A_27a) => ! [V2e2] : ( mem(V2e2,A_27a) => ! [V3b1] : ( mem(V3b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V4b2] : ( mem(V4b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V1e1),V3b1)) & ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V2e2),V4b2)) & ( ~~ ( V3b1 = V4b2 ) ) ) ) => ? [V5b] : ( mem(V5b,arr(A_27a,ty_2Enum_2Enum)) & ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V3b1),V2e2),V5b)) & p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V4b2),V1e1),V5b)) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Ebag_2ESING__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2ESING__BAG(A_27a),V0b)) <=> ? [V1x] : ( mem(V1x,A_27a) & ( V0b = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1x),c_2Ebag_2EEMPTY__BAG(A_27a)) ) ) ) ) ) )).
fof(conj_thm_2Ebag_2ESING__BAG__THM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => p(ap(c_2Ebag_2ESING__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),c_2Ebag_2EEMPTY__BAG(A_27a)))) )))).
fof(ax_thm_2Ebag_2EEL__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ( ap(c_2Ebag_2EEL__BAG(A_27a),V0e) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),c_2Ebag_2EEMPTY__BAG(A_27a)) ) ) ) )).
fof(conj_thm_2Ebag_2EEL__BAG__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( ( ap(c_2Ebag_2EEL__BAG(A_27a),V0x) = ap(c_2Ebag_2EEL__BAG(A_27a),V1y) ) => ( V0x = V1y ) ) ) )))).
fof(conj_thm_2Ebag_2EEL__BAG__INSERT__squeeze,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ! [V2y] : ( mem(V2y,A_27a) => ( ( ap(c_2Ebag_2EEL__BAG(A_27a),V0x) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2y),V1b) ) => ( ( V0x = V2y ) & ( V1b = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESING__EL__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => p(ap(c_2Ebag_2ESING__BAG(A_27a),ap(c_2Ebag_2EEL__BAG(A_27a),V0e))) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e),V0b) = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(c_2Ebag_2EEL__BAG(A_27a),V1e)),V0b) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INSERT__EQ__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V3b] : ( mem(V3b,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V3b) = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b1),V2b2) ) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b1)) | p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V2b2)) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__SING,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b),V1e),c_2Ebag_2EEMPTY__BAG(A_27a))) => p(ap(c_2Ebag_2ESING__BAG(A_27a),V0b)) ) ) )))).
fof(conj_thm_2Ebag_2ENOT__IN__EMPTY__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0x),c_2Ebag_2EEMPTY__BAG(A_27a))) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__EMPTY__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V0e),V1n),c_2Ebag_2EEMPTY__BAG(A_27a))) <=> ( V1n = c_2Enum_2E0 ) ) ) )))).
fof(conj_thm_2Ebag_2EMEMBER__NOT__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ( ? [V1x] : ( mem(V1x,A_27a) & p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V1x),V0b)) ) ) <=> ( ~~ ( V0b = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__LEQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) <=> ! [V2x] : ( mem(V2x,A_27a) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(V0b1,V2x)),ap(V1b2,V2x))) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)),V0b)) ) ) & ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b),c_2Ebag_2EEMPTY__BAG(A_27a))) <=> ( V1b = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__REFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b),V0b)) )))).
fof(conj_thm_2Ebag_2EPSUB__BAG__IRREFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ~~ p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b),V0b)) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__ANTISYM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) & p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V0b1)) ) => ( V0b1 = V1b2 ) ) ) )))).
fof(conj_thm_2Ebag_2EPSUB__BAG__ANTISYM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ~~ ( p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V1b2)) & p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V1b2),V0b1)) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) & p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V2b3)) ) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V2b3)) ) ) ) )))).
fof(conj_thm_2Ebag_2EPSUB__BAG__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V1b2)) & p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V1b2),V2b3)) ) => p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V2b3)) ) ) ) )))).
fof(conj_thm_2Ebag_2EPSUB__BAG__SUB__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V1b2)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) ) ) )))).
fof(conj_thm_2Ebag_2EPSUB__BAG__NOT__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V1b2)) => ( ~~ ( V0b1 = V1b2 ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DIFF__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b),V0b) = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) & ( ( ! [V1b] : ( mem(V1b,arr(A_27b,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27b),V1b),c_2Ebag_2EEMPTY__BAG(A_27b)) = V1b ) ) ) & ( ( ! [V2b] : ( mem(V2b,arr(A_27c,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27c),c_2Ebag_2EEMPTY__BAG(A_27c)),V2b) = c_2Ebag_2EEMPTY__BAG(A_27c) ) ) ) & ! [V3b1] : ( mem(V3b1,arr(A_27d,ty_2Enum_2Enum)) => ! [V4b2] : ( mem(V4b2,arr(A_27d,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27d),V3b1),V4b2)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27d),V3b1),V4b2) = c_2Ebag_2EEMPTY__BAG(A_27d) ) ) ) ) ) ) ))))))).
fof(conj_thm_2Ebag_2EBAG__DIFF__EMPTY__simple,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ( ( ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b),V0b) = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) & ( ( ! [V1b] : ( mem(V1b,arr(A_27b,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27b),V1b),c_2Ebag_2EEMPTY__BAG(A_27b)) = V1b ) ) ) & ! [V2b] : ( mem(V2b,arr(A_27c,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27c),c_2Ebag_2EEMPTY__BAG(A_27c)),V2b) = c_2Ebag_2EEMPTY__BAG(A_27c) ) ) ) )))))).
fof(conj_thm_2Ebag_2EBAG__DIFF__EQ__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b),V1c) = c_2Ebag_2EEMPTY__BAG(A_27a) ) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b),V1c)) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DIFF__INSERT__same,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V1b1)),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V2b2)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b1),V2b2) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DIFF__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0x),V1b1)) ) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V2b2)),V1b1) = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V2b2),V1b1)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ENOT__IN__BAG__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0x),V1b1)) ) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b1),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V2b2)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b1),V2b2) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__DIFF__I,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b1)) & ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V2b2)) ) ) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b1),V2b2))) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__DIFF__E,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b1),V2b2))) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b1)) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__UNION__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0X] : ( mem(V0X,arr(A_27a,ty_2Enum_2Enum)) => ! [V1Y] : ( mem(V1Y,arr(A_27a,ty_2Enum_2Enum)) => ! [V2Z] : ( mem(V2Z,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V2Z),V1Y)) => ( ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0X),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1Y),V2Z)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0X),V1Y)),V2Z) ) & ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1Y),V2Z)),V0X) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0X),V1Y)),V2Z) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DIFF__2L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0X] : ( mem(V0X,arr(A_27a,ty_2Enum_2Enum)) => ! [V1Y] : ( mem(V1Y,arr(A_27a,ty_2Enum_2Enum)) => ! [V2Z] : ( mem(V2Z,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0X),V1Y)),V2Z) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0X),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1Y),V2Z)) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DIFF__2R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0A] : ( mem(V0A,arr(A_27a,ty_2Enum_2Enum)) => ! [V1B] : ( mem(V1B,arr(A_27a,ty_2Enum_2Enum)) => ! [V2C] : ( mem(V2C,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V2C),V1B)) => ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0A),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1B),V2C)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0A),V2C)),V1B) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__BAG__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0X] : ( mem(V0X,arr(A_27a,ty_2Enum_2Enum)) => ! [V1Y] : ( mem(V1Y,arr(A_27a,ty_2Enum_2Enum)) => ! [V2Y_27] : ( mem(V2Y_27,arr(A_27a,ty_2Enum_2Enum)) => ! [V3Z] : ( mem(V3Z,arr(A_27a,ty_2Enum_2Enum)) => ! [V4W] : ( mem(V4W,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0X),V1Y)),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V3Z),V4W))) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0X),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1Y),V2Y_27))),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V3Z),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V4W),V2Y_27)))) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DIFF__UNION__eliminate,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V2b3)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b2),V2b3) ) & ( ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V2b3),V0b1)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b2),V2b3) ) & ( ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V0b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V2b3)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b2),V2b3) ) & ( ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V0b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V2b3),V0b1)) = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b2),V2b3) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__UNION__eliminate,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V2b3))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V2b3)) ) & ( ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V2b3),V0b1))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V2b3)) ) & ( ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V0b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V2b3))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V2b3)) ) & ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V0b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V2b3),V0b1))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V2b3)) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2Emove__BAG__UNION__over__eq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0X] : ( mem(V0X,arr(A_27a,ty_2Enum_2Enum)) => ! [V1Y] : ( mem(V1Y,arr(A_27a,ty_2Enum_2Enum)) => ! [V2Z] : ( mem(V2Z,arr(A_27a,ty_2Enum_2Enum)) => ( ( ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0X),V1Y) = V2Z ) => ( V0X = ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V2Z),V1Y) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V2b))) ) ) ) ) ) & ( ( ! [V3b1] : ( mem(V3b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V4b2] : ( mem(V4b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V3b1),V4b2)) => ! [V5b] : ( mem(V5b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V3b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V5b),V4b2))) ) ) ) ) ) & ( ( ! [V6b1] : ( mem(V6b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V7b2] : ( mem(V7b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V8b3] : ( mem(V8b3,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V6b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V7b2),V8b3))) => ! [V9b] : ( mem(V9b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V6b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V7b2),V9b)),V8b3))) ) ) ) ) ) ) & ( ( ! [V10b1] : ( mem(V10b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V11b2] : ( mem(V11b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V12b3] : ( mem(V12b3,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V10b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V11b2),V12b3))) => ! [V13b] : ( mem(V13b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V10b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V13b),V11b2)),V12b3))) ) ) ) ) ) ) & ( ( ! [V14b1] : ( mem(V14b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V15b2] : ( mem(V15b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V16b3] : ( mem(V16b3,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V14b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V16b3),V15b2))) => ! [V17b] : ( mem(V17b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V14b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V16b3),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V15b2),V17b)))) ) ) ) ) ) ) & ( ( ! [V18b1] : ( mem(V18b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V19b2] : ( mem(V19b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V20b3] : ( mem(V20b3,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V18b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V20b3),V19b2))) => ! [V21b] : ( mem(V21b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V18b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V20b3),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V21b),V19b2)))) ) ) ) ) ) ) & ( ( ! [V22b1] : ( mem(V22b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V23b2] : ( mem(V23b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V24b3] : ( mem(V24b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V25b4] : ( mem(V25b4,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V22b1),V24b3)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V23b2),V25b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V22b1),V23b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V24b3),V25b4))) ) ) ) ) ) ) ) & ( ( ! [V26b1] : ( mem(V26b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V27b2] : ( mem(V27b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V28b3] : ( mem(V28b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V29b4] : ( mem(V29b4,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V26b1),V29b4)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V27b2),V28b3)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V26b1),V27b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V28b3),V29b4))) ) ) ) ) ) ) ) & ( ( ! [V30b1] : ( mem(V30b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V31b2] : ( mem(V31b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V32b3] : ( mem(V32b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V33b4] : ( mem(V33b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V34b5] : ( mem(V34b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V30b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V32b3),V34b5))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V31b2),V33b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V30b1),V31b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V32b3),V33b4)),V34b5))) ) ) ) ) ) ) ) ) & ( ( ! [V35b1] : ( mem(V35b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V36b2] : ( mem(V36b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V37b3] : ( mem(V37b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V38b4] : ( mem(V38b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V39b5] : ( mem(V39b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V35b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V38b4),V39b5))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V36b2),V37b3)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V35b1),V36b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V37b3),V38b4)),V39b5))) ) ) ) ) ) ) ) ) & ( ( ! [V40b1] : ( mem(V40b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V41b2] : ( mem(V41b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V42b3] : ( mem(V42b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V43b4] : ( mem(V43b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V44b5] : ( mem(V44b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V41b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V42b3),V44b5))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V40b1),V43b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V40b1),V41b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V42b3),V43b4)),V44b5))) ) ) ) ) ) ) ) ) & ( ( ! [V45b1] : ( mem(V45b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V46b2] : ( mem(V46b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V47b3] : ( mem(V47b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V48b4] : ( mem(V48b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V49b5] : ( mem(V49b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V46b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V48b4),V49b5))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V45b1),V47b3)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V45b1),V46b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V47b3),V48b4)),V49b5))) ) ) ) ) ) ) ) ) & ( ( ! [V50b1] : ( mem(V50b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V51b2] : ( mem(V51b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V52b3] : ( mem(V52b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V53b4] : ( mem(V53b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V54b5] : ( mem(V54b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V50b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V54b5),V52b3))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V51b2),V53b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V51b2),V50b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V54b5),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V52b3),V53b4)))) ) ) ) ) ) ) ) ) & ( ( ! [V55b1] : ( mem(V55b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V56b2] : ( mem(V56b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V57b3] : ( mem(V57b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V58b4] : ( mem(V58b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V59b5] : ( mem(V59b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V55b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V59b5),V58b4))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V56b2),V57b3)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V56b2),V55b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V59b5),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V57b3),V58b4)))) ) ) ) ) ) ) ) ) & ( ( ! [V60b1] : ( mem(V60b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V61b2] : ( mem(V61b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V62b3] : ( mem(V62b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V63b4] : ( mem(V63b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V64b5] : ( mem(V64b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V61b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V64b5),V62b3))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V60b1),V63b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V61b2),V60b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V64b5),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V62b3),V63b4)))) ) ) ) ) ) ) ) ) & ( ( ! [V65b1] : ( mem(V65b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V66b2] : ( mem(V66b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V67b3] : ( mem(V67b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V68b4] : ( mem(V68b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V69b5] : ( mem(V69b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V66b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V69b5),V68b4))) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V65b1),V67b3)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V66b2),V65b1)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V69b5),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V67b3),V68b4)))) ) ) ) ) ) ) ) ) & ( ( ! [V70b1] : ( mem(V70b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V71b2] : ( mem(V71b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V72b3] : ( mem(V72b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V73b4] : ( mem(V73b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V74b5] : ( mem(V74b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V70b1),V71b2)),V73b4)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V72b3),V74b5)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V70b1),V72b3)),V71b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V73b4),V74b5))) ) ) ) ) ) ) ) ) & ( ( ! [V75b1] : ( mem(V75b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V76b2] : ( mem(V76b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V77b3] : ( mem(V77b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V78b4] : ( mem(V78b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V79b5] : ( mem(V79b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V75b1),V76b2)),V79b5)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V77b3),V78b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V75b1),V77b3)),V76b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V78b4),V79b5))) ) ) ) ) ) ) ) ) & ( ( ! [V80b1] : ( mem(V80b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V81b2] : ( mem(V81b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V82b3] : ( mem(V82b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V83b4] : ( mem(V83b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V84b5] : ( mem(V84b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V82b3),V81b2)),V83b4)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V80b1),V84b5)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V80b1),V82b3)),V81b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V83b4),V84b5))) ) ) ) ) ) ) ) ) & ( ( ! [V85b1] : ( mem(V85b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V86b2] : ( mem(V86b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V87b3] : ( mem(V87b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V88b4] : ( mem(V88b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V89b5] : ( mem(V89b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V87b3),V86b2)),V89b5)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V85b1),V88b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V85b1),V87b3)),V86b2)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V88b4),V89b5))) ) ) ) ) ) ) ) ) & ( ( ! [V90b1] : ( mem(V90b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V91b2] : ( mem(V91b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V92b3] : ( mem(V92b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V93b4] : ( mem(V93b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V94b5] : ( mem(V94b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V91b2),V90b1)),V93b4)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V92b3),V94b5)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V91b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V90b1),V92b3))),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V94b5),V93b4))) ) ) ) ) ) ) ) ) & ( ( ! [V95b1] : ( mem(V95b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V96b2] : ( mem(V96b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V97b3] : ( mem(V97b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V98b4] : ( mem(V98b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V99b5] : ( mem(V99b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V96b2),V95b1)),V99b5)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V97b3),V98b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V96b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V95b1),V97b3))),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V99b5),V98b4))) ) ) ) ) ) ) ) ) & ( ( ! [V100b1] : ( mem(V100b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V101b2] : ( mem(V101b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V102b3] : ( mem(V102b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V103b4] : ( mem(V103b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V104b5] : ( mem(V104b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V101b2),V102b3)),V103b4)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V100b1),V104b5)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V101b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V100b1),V102b3))),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V104b5),V103b4))) ) ) ) ) ) ) ) ) & ! [V105b1] : ( mem(V105b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V106b2] : ( mem(V106b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V107b3] : ( mem(V107b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V108b4] : ( mem(V108b4,arr(A_27a,ty_2Enum_2Enum)) => ! [V109b5] : ( mem(V109b5,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V106b2),V107b3)),V109b5)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V105b1),V108b4)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V106b2),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V105b1),V107b3))),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V109b5),V108b4))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__EL__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(c_2Ebag_2EEL__BAG(A_27a),V0e)),V1b)) <=> p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V1b)) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V1b1)),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V2b2))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b1),V2b2)) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__INSERT__I,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b),V1c)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e),V1c))) ) ) ) )))).
fof(conj_thm_2Ebag_2ENOT__IN__SUB__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e] : ( mem(V2e,A_27a) => ( ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),V0b1)) ) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e),V1b2))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__BAG__IN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b1] : ( mem(V1b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b2] : ( mem(V2b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0x),V1b1)),V2b2)) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0x),V2b2)) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__EXISTS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) <=> ? [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) & ( V1b2 = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V2b) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__UNION__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V2b3)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V2b3),V0b1))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),V2b3)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__UNION__down,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),V2b3)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V2b3)) & p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V2b3)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b1),V2b3)),V1b2)) ) ) ) ) ) & ! [V3b1] : ( mem(V3b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V4b2] : ( mem(V4b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V5b3] : ( mem(V5b3,arr(A_27a,ty_2Enum_2Enum)) => ! [V6b4] : ( mem(V6b4,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V4b2),V3b1)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V6b4),V5b3)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V3b1),V4b2)),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V5b3),V6b4))) <=> p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V3b1),V6b4)),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V4b2),V5b3))) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__PSUB__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) <=> ( p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V0b1),V1b2)) | ( V0b1 = V1b2 ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DELETE__PSUB__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b0] : ( mem(V0b0,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__DELETE(A_27a),V0b0),V1e),V2b)) => p(ap(ap(c_2Ebag_2EPSUB__BAG(A_27a),V2b),V0b0)) ) ) ) )))).
fof(ax_thm_2Ebag_2ESET__OF__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b) = f966(A_27a,V0b) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__OF__SET,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ap(c_2Ebag_2EBAG__OF__SET(A_27a),V0P) = f967(A_27a,V0P) ) ) ) )).
fof(conj_thm_2Ebag_2ESET__OF__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ebag_2EBAG__OF__SET(A_27a),c_2Epred__set_2EEMPTY(A_27a)) = c_2Ebag_2EEMPTY__BAG(A_27a) )))).
fof(conj_thm_2Ebag_2EBAG__IN__BAG__OF__SET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V1p),ap(c_2Ebag_2EBAG__OF__SET(A_27a),V0P))) <=> p(ap(ap(c_2Ebool_2EIN(A_27a),V1p),V0P)) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__OF__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)) = c_2Epred__set_2EEMPTY(A_27a) )))).
fof(conj_thm_2Ebag_2ESET__BAG__I,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(c_2Ebag_2EBAG__OF__SET(A_27a),V0s)) = V0s ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__SET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b1)),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b2))) ) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b1)),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b2)) ) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__MERGE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__MERGE(A_27a),V0b1),V1b2)) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b1)),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b2)) ) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V1b)) = ap(ap(c_2Epred__set_2EINSERT(A_27a),V0e),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b)) ) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__EL__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(c_2Ebag_2EEL__BAG(A_27a),V0e)) = ap(ap(c_2Epred__set_2EINSERT(A_27a),V0e),c_2Epred__set_2EEMPTY(A_27a)) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__DIFF__SUBSET__down,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b1)),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b2))),ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b1),V1b2)))) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__DIFF__SUBSET__up,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b1),V1b2))),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b1))) ) )))).
fof(conj_thm_2Ebag_2EIN__SET__OF__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b))) <=> p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0x),V1b)) ) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__EQ__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( ( ( c_2Epred__set_2EEMPTY(A_27a) = ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b) ) <=> ( V0b = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) & ( ( ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b) = c_2Epred__set_2EEMPTY(A_27a) ) <=> ( V0b = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(ax_thm_2Ebag_2EBAG__DISJOINT,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),V1b2)) <=> p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b1)),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V1b2))) ) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__DISJOINT__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b),c_2Ebag_2EEMPTY__BAG(A_27a))) & p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)),V0b)) ) )))).
fof(conj_thm_2Ebag_2EBAG__DISJOINT__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0B1] : ( mem(V0B1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1B2] : ( mem(V1B2,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0B1),V1B2)),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1B2),V0B1))) ) )))).
fof(conj_thm_2Ebag_2EBAG__DISJOINT__BAG__IN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),V1b2)) <=> ! [V2e] : ( mem(V2e,A_27a) => ( ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),V0b1)) ) | ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e),V1b2)) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__DISJOINT__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2e1] : ( mem(V2e1,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e1),V0b1)),V1b2)) <=> ( ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V2e1),V1b2)) ) & p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),V1b2)) ) ) ) ) ) ) & ! [V3b1] : ( mem(V3b1,arr(A_27b,ty_2Enum_2Enum)) => ! [V4b2] : ( mem(V4b2,arr(A_27b,ty_2Enum_2Enum)) => ! [V5e2] : ( mem(V5e2,A_27b) => ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27b),V3b1),ap(ap(c_2Ebag_2EBAG__INSERT(A_27b),V5e2),V4b2))) <=> ( ( ~~ p(ap(ap(c_2Ebag_2EBAG__IN(A_27b),V5e2),V3b1)) ) & p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27b),V3b1),V4b2)) ) ) ) ) ) ))))).
fof(conj_thm_2Ebag_2EBAG__DISJOINT__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ! [V2b3] : ( mem(V2b3,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V1b2),V2b3))) <=> ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),V1b2)) & p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),V2b3)) ) ) & ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)),V2b3)) <=> ( p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V0b1),V2b3)) & p(ap(ap(c_2Ebag_2EBAG__DISJOINT(A_27a),V1b2),V2b3)) ) ) ) ) ) )))).
fof(ax_thm_2Ebag_2EFINITE__BAG,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) <=> ! [V1P] : ( mem(V1P,arr(arr(A_27a,ty_2Enum_2Enum),bool)) => ( ( p(ap(V1P,c_2Ebag_2EEMPTY__BAG(A_27a))) & ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(V1P,V2b)) => ! [V3e] : ( mem(V3e,A_27a) => p(ap(V1P,ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V3e),V2b))) ) ) ) ) => p(ap(V1P,V0b)) ) ) ) ) ) )).
fof(conj_thm_2Ebag_2EFINITE__EMPTY__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Ebag_2EFINITE__BAG(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)))))).
fof(conj_thm_2Ebag_2EFINITE__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => ! [V1e] : ( mem(V1e,A_27a) => p(ap(c_2Ebag_2EFINITE__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e),V0b))) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__BAG__INDUCT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(arr(A_27a,ty_2Enum_2Enum),bool)) => ( ( p(ap(V0P,c_2Ebag_2EEMPTY__BAG(A_27a))) & ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(V0P,V1b)) => ! [V2e] : ( mem(V2e,A_27a) => p(ap(V0P,ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e),V1b))) ) ) ) ) => ! [V3b] : ( mem(V3b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V3b)) => p(ap(V0P,V3b)) ) ) ) )))).
fof(conj_thm_2Ebag_2ESTRONG__FINITE__BAG__INDUCT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(arr(A_27a,ty_2Enum_2Enum),bool)) => ( ( p(ap(V0P,c_2Ebag_2EEMPTY__BAG(A_27a))) & ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b)) & p(ap(V0P,V1b)) ) => ! [V2e] : ( mem(V2e,A_27a) => p(ap(V0P,ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V2e),V1b))) ) ) ) ) => ! [V3b] : ( mem(V3b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V3b)) => p(ap(V0P,V3b)) ) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__BAG__THM,lemma,( ! [A_27a]: ( ne(A_27a) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a))) & ! [V0e] : ( mem(V0e,A_27a) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V0e),V1b))) <=> p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b)) ) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__BAG__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b1)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => p(ap(c_2Ebag_2EFINITE__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b1),V1b2))) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__BAG__DIFF__dual,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b1)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b2),V0b1))) => p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b2)) ) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__BAG__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2))) <=> ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b1)) & p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b2)) ) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__SUB__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b1)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1b2),V0b1)) => p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b2)) ) ) ) )))).
fof(ax_thm_2Ebag_2EBAG__CARD__RELn,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebag_2EBAG__CARD__RELn(A_27a),V0b),V1n)) <=> ! [V2P] : ( mem(V2P,arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))) => ( ( p(ap(ap(V2P,c_2Ebag_2EEMPTY__BAG(A_27a)),c_2Enum_2E0)) & ! [V3b] : ( mem(V3b,arr(A_27a,ty_2Enum_2Enum)) => ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( p(ap(ap(V2P,V3b),V4n)) => ! [V5e] : ( mem(V5e,A_27a) => p(ap(ap(V2P,ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V5e),V3b)),ap(c_2Enum_2ESUC,V4n))) ) ) ) ) ) => p(ap(ap(V2P,V0b),V1n)) ) ) ) ) ) ) )).
fof(ax_thm_2Ebag_2EBAG__CARD,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => p(ap(ap(c_2Ebag_2EBAG__CARD__RELn(A_27a),V0b),ap(c_2Ebag_2EBAG__CARD(A_27a),V0b))) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__CARD__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ebag_2EBAG__CARD(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)) = c_2Enum_2E0 )))).
fof(conj_thm_2Ebag_2EBCARD__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => ( ( ap(c_2Ebag_2EBAG__CARD(A_27a),V0b) = c_2Enum_2E0 ) <=> ( V0b = c_2Ebag_2EEMPTY__BAG(A_27a) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__CARD__THM,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ap(c_2Ebag_2EBAG__CARD(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)) = c_2Enum_2E0 ) & ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => ! [V1e] : ( mem(V1e,A_27a) => ( ap(c_2Ebag_2EBAG__CARD(A_27a),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e),V0b)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Ebag_2EBAG__CARD(A_27a),V0b)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__CARD__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b1)) & p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b2)) ) => ( ap(c_2Ebag_2EBAG__CARD(A_27a),ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),V1b2)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Ebag_2EBAG__CARD(A_27a),V0b1)),ap(c_2Ebag_2EBAG__CARD(A_27a),V1b2)) ) ) ) )))).
fof(conj_thm_2Ebag_2EBCARD__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(c_2Ebag_2EBAG__CARD(A_27a),V0b) = ap(c_2Enum_2ESUC,V1n) ) <=> ? [V2b0] : ( mem(V2b0,arr(A_27a,ty_2Enum_2Enum)) & ? [V3e] : ( mem(V3e,A_27a) & ( ( V0b = ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V3e),V2b0) ) & ( ap(c_2Ebag_2EBAG__CARD(A_27a),V2b0) = V1n ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__CARD__BAG__INN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V2e),V1n),V0b)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),ap(c_2Ebag_2EBAG__CARD(A_27a),V0b))) ) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__DIFF__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) => ( V1b2 = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V0b1),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V1b2),V0b1)) ) ) ) )))).
fof(conj_thm_2Ebag_2ESUB__BAG__CARD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b1] : ( mem(V0b1,arr(A_27a,ty_2Enum_2Enum)) => ! [V1b2] : ( mem(V1b2,arr(A_27a,ty_2Enum_2Enum)) => ( ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b2)) & p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V0b1),V1b2)) ) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ebag_2EBAG__CARD(A_27a),V0b1)),ap(c_2Ebag_2EBAG__CARD(A_27a),V1b2))) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__CARD__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) => ! [V1c] : ( mem(V1c,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),V1c),V0b)) => ( ap(c_2Ebag_2EBAG__CARD(A_27a),ap(ap(c_2Ebag_2EBAG__DIFF(A_27a),V0b),V1c)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ebag_2EBAG__CARD(A_27a),V0b)),ap(c_2Ebag_2EBAG__CARD(A_27a),V1c)) ) ) ) ) )))).
fof(ax_thm_2Ebag_2EBAG__FILTER__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),V1b) = f968(A_27a,V1b,V0P) ) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__FILTER__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),c_2Ebag_2EEMPTY__BAG(A_27a)) = c_2Ebag_2EEMPTY__BAG(A_27a) ) )))).
fof(conj_thm_2Ebag_2EBAG__FILTER__BAG__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e),V2b)) = ap(ap(ap(c_2Ebool_2ECOND(arr(A_27a,ty_2Enum_2Enum)),ap(V0P,V1e)),ap(ap(c_2Ebag_2EBAG__INSERT(A_27a),V1e),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),V2b))),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),V2b)) ) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__BAG__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V1b)) => p(ap(c_2Ebag_2EFINITE__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),V1b))) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__INN__BAG__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2P] : ( mem(V2P,arr(A_27a,bool)) => ! [V3b] : ( mem(V3b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V0e),V1n),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V2P),V3b))) <=> ( ( V1n = c_2Enum_2E0 ) | ( p(ap(V2P,V0e)) & p(ap(ap(ap(c_2Ebag_2EBAG__INN(A_27a),V0e),V1n),V3b)) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__IN__BAG__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V1P),V2b))) <=> ( p(ap(V1P,V0e)) & p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V0e),V2b)) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__FILTER__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1Q] : ( mem(V1Q,arr(A_27a,bool)) => ! [V2b] : ( mem(V2b,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V1Q),V2b)) = ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),f969(A_27a,V0P,V1Q)),V2b) ) ) ) )))).
fof(conj_thm_2Ebag_2EBAG__FILTER__SUB__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1b] : ( mem(V1b,arr(A_27a,ty_2Enum_2Enum)) => p(ap(ap(c_2Ebag_2ESUB__BAG(A_27a),ap(ap(c_2Ebag_2EBAG__FILTER(A_27a),V0P),V1b)),V1b)) ) )))).
fof(conj_thm_2Ebag_2ESET__OF__BAG__EQ__INSERT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( ( ap(ap(c_2Epred__set_2EINSERT(A_27a),V1e),V2s) = ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b) ) <=> ? [V3b0] : ( mem(V3b0,arr(A_27a,ty_2Enum_2Enum)) & ? [V4eb] : ( mem(V4eb,arr(A_27a,ty_2Enum_2Enum)) & ( ( V0b = ap(ap(c_2Ebag_2EBAG__UNION(A_27a),V4eb),V3b0) ) & ( ( V2s = ap(c_2Ebag_2ESET__OF__BAG(A_27a),V3b0) ) & ( ( ! [V5e_27] : ( mem(V5e_27,A_27a) => ( p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V5e_27),V4eb)) => ( V5e_27 = V1e ) ) ) ) & ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V1e),V2s)) ) => p(ap(ap(c_2Ebag_2EBAG__IN(A_27a),V1e),V4eb)) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ebag_2EFINITE__SET__OF__BAG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,arr(A_27a,ty_2Enum_2Enum)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Ebag_2ESET__OF__BAG(A_27a),V0b))) <=> p(ap(c_2Ebag_2EFINITE__BAG(A_27a),V0b)) ) )))).
fof(ax_thm_2Ebag_2EBAG__IMAGE__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27a)) => ! [V1b] : ( mem(V1b,arr(A_27b,ty_2Enum_2Enum)) => ( ap(ap(c_2Ebag_2EBAG__IMAGE(A_27a,A_27b),V0f),V1b) = f972(A_27a,A_27b,V1b,V0f) ) ) ) ) ) )).
fof(conj_thm_2Ebag_2EBAG__IMAGE__EMPTY,conjecture,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ( ap(ap(c_2Ebag_2EBAG__IMAGE(A_27b,A_27a),V0f),c_2Ebag_2EEMPTY__BAG(A_27a)) = c_2Ebag_2EEMPTY__BAG(A_27b) ) ))))).
