include('Axioms/ordinal+2.ax').
fof(mem_c_2Ewords_2EBIT__SET,axiom,( mem(c_2Ewords_2EBIT__SET,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))) )).
fof(mem_c_2Ewords_2EINT__MAX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2EINT__MAX(A_27a),arr(ty_2Ebool_2Eitself(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2EINT__MIN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2EINT__MIN(A_27a),arr(ty_2Ebool_2Eitself(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2EUINT__MAX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2EUINT__MAX(A_27a),arr(ty_2Ebool_2Eitself(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2Eadd__with__carry,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eadd__with__carry(A_27a),arr(ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27a),ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27a),bool)),ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27a),ty_2Epair_2Eprod(bool,bool)))) ) )).
fof(mem_c_2Ewords_2Ebit__count,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ebit__count(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2Ebit__count__upto,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ebit__count__upto(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ewords_2Ebit__field__insert,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Ebit__field__insert(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27b),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))))) ) ) )).
fof(mem_c_2Ewords_2Econcat__word__list,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Econcat__word__list(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Efcp_2Ecart(bool,A_27a)),ty_2Efcp_2Ecart(bool,A_27b))) ) ) )).
fof(mem_c_2Ewords_2Edimword,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Edimword(A_27a),arr(ty_2Ebool_2Eitself(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2El2w,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2El2w(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2En2w,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2En2w(A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2En2w__itself,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2En2w__itself(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Ebool_2Eitself(A_27a)),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Enzcv,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Enzcv(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)))))) ) )).
fof(mem_c_2Ewords_2Ereduce__and,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ereduce__and(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) ) )).
fof(mem_c_2Ewords_2Ereduce__nand,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ereduce__nand(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) ) )).
fof(mem_c_2Ewords_2Ereduce__nor,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ereduce__nor(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) ) )).
fof(mem_c_2Ewords_2Ereduce__or,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ereduce__or(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) ) )).
fof(mem_c_2Ewords_2Ereduce__xnor,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ereduce__xnor(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) ) )).
fof(mem_c_2Ewords_2Ereduce__xor,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ereduce__xor(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone))) ) )).
fof(mem_c_2Ewords_2Es2w,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Es2w(A_27a),arr(ty_2Enum_2Enum,arr(arr(ty_2Estring_2Echar,ty_2Enum_2Enum),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Efcp_2Ecart(bool,A_27a))))) ) )).
fof(mem_c_2Ewords_2Esaturate__add,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Esaturate__add(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Esaturate__mul,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Esaturate__mul(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Esaturate__n2w,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Esaturate__n2w(A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Esaturate__sub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Esaturate__sub(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Esaturate__w2w,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Esaturate__w2w(A_27a,A_27b),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27b))) ) ) )).
fof(mem_c_2Ewords_2Esw2sw,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Esw2sw(A_27a,A_27b),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27b))) ) ) )).
fof(mem_c_2Ewords_2Ew2l,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ew2l(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Ewords_2Ew2n,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ew2n(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2Ew2s,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Ew2s(A_27a),arr(ty_2Enum_2Enum,arr(arr(ty_2Enum_2Enum,ty_2Estring_2Echar),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Estring_2Echar))))) ) )).
fof(mem_c_2Ewords_2Ew2w,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Ew2w(A_27a,A_27b),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27b))) ) ) )).
fof(mem_c_2Ewords_2Eword__1comp,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__1comp(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__2comp,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__2comp(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__H,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__H(A_27a),ty_2Efcp_2Ecart(bool,A_27a)) ) )).
fof(mem_c_2Ewords_2Eword__L,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__L(A_27a),ty_2Efcp_2Ecart(bool,A_27a)) ) )).
fof(mem_c_2Ewords_2Eword__L2,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__L2(A_27a),ty_2Efcp_2Ecart(bool,A_27a)) ) )).
fof(mem_c_2Ewords_2Eword__T,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__T(A_27a),ty_2Efcp_2Ecart(bool,A_27a)) ) )).
fof(mem_c_2Ewords_2Eword__abs,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__abs(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__add,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__add(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__and,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__and(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__asr,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__asr(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__asr__bv,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__asr__bv(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__bit,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__bit(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__bits,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__bits(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))))) ) )).
fof(mem_c_2Ewords_2Eword__compare,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__compare(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)))) ) )).
fof(mem_c_2Ewords_2Eword__concat,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27c),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27b),ty_2Efcp_2Ecart(bool,A_27c)))) ) ) ) )).
fof(mem_c_2Ewords_2Eword__div,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__div(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__extract,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Eword__extract(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27b))))) ) ) )).
fof(mem_c_2Ewords_2Eword__from__bin__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__bin__list(A_27a),arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__bin__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__bin__string(A_27a),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__dec__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__dec__list(A_27a),arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__dec__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__dec__string(A_27a),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__hex__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__hex__list(A_27a),arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__hex__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__hex__string(A_27a),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__oct__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__oct__list(A_27a),arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__from__oct__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__from__oct__string(A_27a),arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__ge,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__ge(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__gt,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__gt(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__hi,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__hi(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__hs,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__hs(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__join,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Eword__join(A_27a,A_27b),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27b),ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Ewords_2Eword__le,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__le(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__len,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__len(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Ewords_2Eword__lo,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lo(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__log2,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__log2(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__ls,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__ls(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__lsb,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lsb(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool)) ) )).
fof(mem_c_2Ewords_2Eword__lsl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lsl(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__lsl__bv,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lsl__bv(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__lsr,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lsr(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__lsr__bv,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lsr__bv(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__lt,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__lt(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool))) ) )).
fof(mem_c_2Ewords_2Eword__max,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__max(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__min,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__min(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__mod,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__mod(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__modify,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__modify(A_27a),arr(arr(ty_2Enum_2Enum,arr(bool,bool)),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__msb,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__msb(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),bool)) ) )).
fof(mem_c_2Ewords_2Eword__mul,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__mul(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__nand,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__nand(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__nor,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__nor(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__or,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__or(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__quot,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__quot(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__reduce,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__reduce(A_27a),arr(arr(bool,arr(bool,bool)),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)))) ) )).
fof(mem_c_2Ewords_2Eword__rem,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__rem(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__replicate,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewords_2Eword__replicate(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27b)))) ) ) )).
fof(mem_c_2Ewords_2Eword__reverse,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__reverse(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ewords_2Eword__rol,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__rol(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__rol__bv,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__rol__bv(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__ror,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__ror(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__ror__bv,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__ror__bv(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__rrx,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__rrx(A_27a),arr(ty_2Epair_2Eprod(bool,ty_2Efcp_2Ecart(bool,A_27a)),ty_2Epair_2Eprod(bool,ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__sign__extend,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__sign__extend(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__signed__bits,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__signed__bits(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))))) ) )).
fof(mem_c_2Ewords_2Eword__slice,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__slice(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a))))) ) )).
fof(mem_c_2Ewords_2Eword__smax,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__smax(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__smin,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__smin(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__sub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__sub(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__to__bin__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__bin__list(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ewords_2Eword__to__bin__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__bin__string(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Estring_2Echar))) ) )).
fof(mem_c_2Ewords_2Eword__to__dec__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__dec__list(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ewords_2Eword__to__dec__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__dec__string(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Estring_2Echar))) ) )).
fof(mem_c_2Ewords_2Eword__to__hex__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__hex__list(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ewords_2Eword__to__hex__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__hex__string(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Estring_2Echar))) ) )).
fof(mem_c_2Ewords_2Eword__to__oct__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__oct__list(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum))) ) )).
fof(mem_c_2Ewords_2Eword__to__oct__string,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__to__oct__string(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Estring_2Echar))) ) )).
fof(mem_c_2Ewords_2Eword__xnor,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__xnor(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(mem_c_2Ewords_2Eword__xor,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewords_2Eword__xor(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a)))) ) )).
fof(ax_thm_2Ewords_2Edimword__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) ) )).
fof(ax_thm_2Ewords_2EINT__MIN__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) )).
fof(ax_thm_2Ewords_2EUINT__MAX__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) )).
fof(ax_thm_2Ewords_2EINT__MAX__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) )).
fof(ax_thm_2Ewords_2Ew2n__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Ew2n(A_27a),V0w) = ap(ap(c_2Esum__num_2ESUM,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),f2160(A_27a,V0w)) ) ) ) )).
fof(ax_thm_2Ewords_2En2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2En2w(A_27a),V0n) = ap(c_2Efcp_2EFCP(bool,A_27a),f249(V0n)) ) ) ) )).
fof(ax_thm_2Ewords_2Ew2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Ew2w(A_27a,A_27b),V0w) = ap(c_2Ewords_2En2w(A_27b),ap(c_2Ewords_2Ew2n(A_27a),V0w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Esw2sw__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Esw2sw(A_27a,A_27b),V0w) = ap(c_2Ewords_2En2w(A_27b),ap(ap(ap(c_2Ebit_2ESIGN__EXTEND,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),ap(c_2Ewords_2Ew2n(A_27a),V0w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Ew2l__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Ew2l(A_27a),V0b),V1w) = ap(ap(c_2Enumposrep_2En2l,V0b),ap(c_2Ewords_2Ew2n(A_27a),V1w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2El2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ewords_2El2w(A_27a),V0b),V1l) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Enumposrep_2El2n,V0b),V1l)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Ew2s__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,ty_2Estring_2Echar)) => ! [V2w] : ( mem(V2w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(ap(c_2Ewords_2Ew2s(A_27a),V0b),V1f),V2w) = ap(ap(ap(c_2EASCIInumbers_2En2s,V0b),V1f),ap(c_2Ewords_2Ew2n(A_27a),V2w)) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Es2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1f] : ( mem(V1f,arr(ty_2Estring_2Echar,ty_2Enum_2Enum)) => ! [V2s] : ( mem(V2s,ty_2Elist_2Elist(ty_2Estring_2Echar)) => ( ap(ap(ap(c_2Ewords_2Es2w(A_27a),V0b),V1f),V2s) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(c_2EASCIInumbers_2Es2n,V0b),V1f),V2s)) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__bin__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__bin__list(A_27a) = ap(c_2Ewords_2El2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__oct__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__oct__list(A_27a) = ap(c_2Ewords_2El2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__dec__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__dec__list(A_27a) = ap(c_2Ewords_2El2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__hex__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__hex__list(A_27a) = ap(c_2Ewords_2El2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__bin__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__bin__list(A_27a) = ap(c_2Ewords_2Ew2l(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__oct__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__oct__list(A_27a) = ap(c_2Ewords_2Ew2l(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__dec__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__dec__list(A_27a) = ap(c_2Ewords_2Ew2l(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__hex__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__hex__list(A_27a) = ap(c_2Ewords_2Ew2l(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__bin__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__bin__string(A_27a) = ap(ap(c_2Ewords_2Es2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),c_2EASCIInumbers_2EUNHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__oct__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__oct__string(A_27a) = ap(ap(c_2Ewords_2Es2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2EASCIInumbers_2EUNHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__dec__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__dec__string(A_27a) = ap(ap(c_2Ewords_2Es2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2EASCIInumbers_2EUNHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__from__hex__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__from__hex__string(A_27a) = ap(ap(c_2Ewords_2Es2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),c_2EASCIInumbers_2EUNHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__bin__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__bin__string(A_27a) = ap(ap(c_2Ewords_2Ew2s(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),c_2EASCIInumbers_2EHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__oct__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__oct__string(A_27a) = ap(ap(c_2Ewords_2Ew2s(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2EASCIInumbers_2EHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__dec__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__dec__string(A_27a) = ap(ap(c_2Ewords_2Ew2s(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2EASCIInumbers_2EHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__to__hex__string__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__to__hex__string(A_27a) = ap(ap(c_2Ewords_2Ew2s(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),c_2EASCIInumbers_2EHEX) ) ) )).
fof(ax_thm_2Ewords_2Eword__T__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__T(A_27a) = ap(c_2Ewords_2En2w(A_27a),ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) ) )).
fof(ax_thm_2Ewords_2Eword__L__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__L(A_27a) = ap(c_2Ewords_2En2w(A_27a),ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) ) )).
fof(ax_thm_2Ewords_2Eword__H__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__H(A_27a) = ap(c_2Ewords_2En2w(A_27a),ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) ) )).
fof(ax_thm_2Ewords_2Eword__1comp__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__1comp(A_27a),V0w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2161(A_27a,V0w)) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__and__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__and(A_27a),V0v),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2162(A_27a,V0v,V1w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__or__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__or(A_27a),V0v),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2163(A_27a,V0v,V1w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__xor__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__xor(A_27a),V0v),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2164(A_27a,V1w,V0v)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__nand__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__nand(A_27a),V0v),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2165(A_27a,V1w,V0v)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__nor__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__nor(A_27a),V0v),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2166(A_27a,V1w,V0v)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__xnor__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__xnor(A_27a),V0v),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2167(A_27a,V0v,V1w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__reduce__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(bool,arr(bool,bool))) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__reduce(A_27a),V0f),V1w) = ap(c_2Efcp_2EFCP(bool,ty_2Eone_2Eone),ap(c_2Ecombin_2EK(bool,ty_2Enum_2Enum),ap(ap(c_2Ebool_2ELET(ty_2Elist_2Elist(bool),bool),f2168(V0f)),ap(ap(c_2Elist_2EGENLIST(bool),f2169(A_27a,V1w)),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__compare__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__compare(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),ap(ap(c_2Emin_2E_3D(ty_2Efcp_2Ecart(bool,A_27a)),V0a),V1b)),ap(c_2Ewords_2En2w(ty_2Eone_2Eone),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Ewords_2En2w(ty_2Eone_2Eone),c_2Enum_2E0)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Ereduce__and__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Ereduce__and(A_27a) = ap(c_2Ewords_2Eword__reduce(A_27a),c_2Ebool_2E_2F_5C) ) ) )).
fof(ax_thm_2Ewords_2Ereduce__or__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Ereduce__or(A_27a) = ap(c_2Ewords_2Eword__reduce(A_27a),c_2Ebool_2E_5C_2F) ) ) )).
fof(ax_thm_2Ewords_2Ereduce__xor__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Ereduce__xor(A_27a) = ap(c_2Ewords_2Eword__reduce(A_27a),f2171) ) ) )).
fof(ax_thm_2Ewords_2Ereduce__nand__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Ereduce__nand(A_27a) = ap(c_2Ewords_2Eword__reduce(A_27a),f2173) ) ) )).
fof(ax_thm_2Ewords_2Ereduce__nor__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Ereduce__nor(A_27a) = ap(c_2Ewords_2Eword__reduce(A_27a),f2175) ) ) )).
fof(ax_thm_2Ewords_2Ereduce__xnor__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Ereduce__xnor(A_27a) = ap(c_2Ewords_2Eword__reduce(A_27a),c_2Emin_2E_3D(bool)) ) ) )).
fof(ax_thm_2Ewords_2Eword__lsb__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(c_2Ewords_2Eword__lsb(A_27a),V0w)) <=> p(ap(ap(c_2Efcp_2Efcp__index(bool,A_27a),V0w),c_2Enum_2E0)) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__msb__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(c_2Ewords_2Eword__msb(A_27a),V0w)) <=> p(ap(ap(c_2Efcp_2Efcp__index(bool,A_27a),V0w),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__slice__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__slice(A_27a),V0h),V1l) = f2177(A_27a,V1l,V0h) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__bits__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__bits(A_27a),V0h),V1l) = f2179(A_27a,V1l,V0h) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__signed__bits__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__signed__bits(A_27a),V0h),V1l) = f2181(A_27a,V1l,V0h) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__extract__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__extract(A_27a,A_27b),V0h),V1l) = ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27b),ty_2Efcp_2Ecart(bool,A_27a)),c_2Ewords_2Ew2w(A_27a,A_27b)),ap(ap(c_2Ewords_2Eword__bits(A_27a),V0h),V1l)) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__bit__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__bit(A_27a),V0b),V1w)) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) & p(ap(ap(c_2Efcp_2Efcp__index(bool,A_27a),V1w),V0b)) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__reverse__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__reverse(A_27a),V0w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2182(A_27a,V0w)) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__modify__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(bool,bool))) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__modify(A_27a),V0f),V1w) = ap(c_2Efcp_2EFCP(bool,A_27a),f2183(A_27a,V0f,V1w)) ) ) ) ) )).
fof(conj_thm_2Ewords_2EBIT__SET__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) => ( ( ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ( ( ( ~~ ( V2n = c_2Enum_2E0 ) ) & p(ap(c_2Earithmetic_2EODD,V2n)) ) => p(ap(ap(V0P,ap(c_2Enum_2ESUC,V1i)),ap(ap(c_2Earithmetic_2EDIV,V2n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) & ( ( ( ~~ ( V2n = c_2Enum_2E0 ) ) & ( ~~ p(ap(c_2Earithmetic_2EODD,V2n)) ) ) => p(ap(ap(V0P,ap(c_2Enum_2ESUC,V1i)),ap(ap(c_2Earithmetic_2EDIV,V2n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) => p(ap(ap(V0P,V1i),V2n)) ) ) ) ) => ! [V3v] : ( mem(V3v,ty_2Enum_2Enum) => ! [V4v1] : ( mem(V4v1,ty_2Enum_2Enum) => p(ap(ap(V0P,V3v),V4v1)) ) ) ) ))).
fof(conj_thm_2Ewords_2EBIT__SET__def,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2EBIT__SET,V1i),V0n) = ap(ap(ap(c_2Ebool_2ECOND(arr(ty_2Enum_2Enum,bool)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V0n),c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)),ap(ap(ap(c_2Ebool_2ECOND(arr(ty_2Enum_2Enum,bool)),ap(c_2Earithmetic_2EODD,V0n)),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),V1i),ap(ap(c_2Ewords_2EBIT__SET,ap(c_2Enum_2ESUC,V1i)),ap(ap(c_2Earithmetic_2EDIV,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(ap(c_2Ewords_2EBIT__SET,ap(c_2Enum_2ESUC,V1i)),ap(ap(c_2Earithmetic_2EDIV,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ) ))).
fof(ax_thm_2Ewords_2Ebit__field__insert__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,ty_2Efcp_2Ecart(bool,A_27b)) => ( ap(ap(ap(c_2Ewords_2Ebit__field__insert(A_27a,A_27b),V0h),V1l),V2a) = ap(c_2Ewords_2Eword__modify(A_27a),f2184(A_27b,V0h,V1l,V2a)) ) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__sign__extend__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__sign__extend(A_27a),V0n),V1w) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(c_2Ebit_2ESIGN__EXTEND,V0n),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Ew2n(A_27a),V1w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__len__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__len(A_27a),V0w) = ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) ) ) ) )).
fof(ax_thm_2Ewords_2Ebit__count__upto__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Ebit__count__upto(A_27a),V0n),V1w) = ap(ap(c_2Esum__num_2ESUM,V0n),f2185(A_27a,V1w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Ebit__count__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Ebit__count(A_27a),V0w) = ap(ap(c_2Ewords_2Ebit__count__upto(A_27a),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0w) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__2comp__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__2comp(A_27a),V0w) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Ew2n(A_27a),V0w))) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__add__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__add(A_27a),V0v),V1w) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Ewords_2Ew2n(A_27a),V0v)),ap(c_2Ewords_2Ew2n(A_27a),V1w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__mul__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__mul(A_27a),V0v),V1w) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Ewords_2Ew2n(A_27a),V0v)),ap(c_2Ewords_2Ew2n(A_27a),V1w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__log2__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__log2(A_27a),V0w) = ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebit_2ELOG2,ap(c_2Ewords_2Ew2n(A_27a),V0w))) ) ) ) )).
fof(ax_thm_2Ewords_2Eadd__with__carry__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1y] : ( mem(V1y,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V2carry__in] : ( mem(V2carry__in,bool) => ( ap(c_2Ewords_2Eadd__with__carry(A_27a),ap(ap(c_2Epair_2E_2C(ty_2Efcp_2Ecart(bool,A_27a),ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27a),bool)),V0x),ap(ap(c_2Epair_2E_2C(ty_2Efcp_2Ecart(bool,A_27a),bool),V1y),V2carry__in))) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Efcp_2Ecart(bool,A_27a),ty_2Epair_2Eprod(bool,bool))),f2189(A_27a,V0x,V1y)),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Ewords_2Ew2n(A_27a),V0x)),ap(c_2Ewords_2Ew2n(A_27a),V1y))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),V2carry__in),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),c_2Enum_2E0))) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__sub__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__sub(A_27a),V0v),V1w) = ap(ap(c_2Ewords_2Eword__add(A_27a),V0v),ap(c_2Ewords_2Eword__2comp(A_27a),V1w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__div__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__div(A_27a),V0v),V1w) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(c_2Ewords_2Ew2n(A_27a),V0v)),ap(c_2Ewords_2Ew2n(A_27a),V1w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__mod__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__mod(A_27a),V0v),V1w) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2EMOD,ap(c_2Ewords_2Ew2n(A_27a),V0v)),ap(c_2Ewords_2Ew2n(A_27a),V1w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__quot__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__quot(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__msb(A_27a),V0a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__msb(A_27a),V1b)),ap(ap(c_2Ewords_2Eword__div(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),V0a)),ap(c_2Ewords_2Eword__2comp(A_27a),V1b))),ap(c_2Ewords_2Eword__2comp(A_27a),ap(ap(c_2Ewords_2Eword__div(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),V0a)),V1b)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__msb(A_27a),V1b)),ap(c_2Ewords_2Eword__2comp(A_27a),ap(ap(c_2Ewords_2Eword__div(A_27a),V0a),ap(c_2Ewords_2Eword__2comp(A_27a),V1b)))),ap(ap(c_2Ewords_2Eword__div(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__rem__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__rem(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__msb(A_27a),V0a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__msb(A_27a),V1b)),ap(c_2Ewords_2Eword__2comp(A_27a),ap(ap(c_2Ewords_2Eword__mod(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),V0a)),ap(c_2Ewords_2Eword__2comp(A_27a),V1b)))),ap(c_2Ewords_2Eword__2comp(A_27a),ap(ap(c_2Ewords_2Eword__mod(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),V0a)),V1b)))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__msb(A_27a),V1b)),ap(ap(c_2Ewords_2Eword__mod(A_27a),V0a),ap(c_2Ewords_2Eword__2comp(A_27a),V1b))),ap(ap(c_2Ewords_2Eword__mod(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__L2__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewords_2Eword__L2(A_27a) = ap(ap(c_2Ewords_2Eword__mul(A_27a),c_2Ewords_2Eword__L(A_27a)),c_2Ewords_2Eword__L(A_27a)) ) ) )).
fof(ax_thm_2Ewords_2Enzcv__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)))),f2191(A_27a,V0a,V1b)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Ewords_2Ew2n(A_27a),V0a)),ap(c_2Ewords_2Ew2n(A_27a),ap(c_2Ewords_2Eword__2comp(A_27a),V1b)))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__lt__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__lt(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),f2193)),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__gt__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__gt(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),f2196)),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__le__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__le(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),f2199)),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__ge__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__ge(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),f2201)),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__ls__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__ls(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),k(bool,ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,bool),bool),f2203)))),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__hi__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__hi(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),k(bool,ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,bool),bool),f2205)))),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__lo__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__lo(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),k(bool,ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,bool),bool),k(bool,ap(c_2Epair_2EUNCURRY(bool,bool,bool),f2206)))))),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__hs__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__hs(A_27a),V0a),V1b)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool))),bool),ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,ty_2Epair_2Eprod(bool,bool)),bool),k(bool,ap(c_2Epair_2EUNCURRY(bool,ty_2Epair_2Eprod(bool,bool),bool),k(bool,ap(c_2Epair_2EUNCURRY(bool,bool,bool),f2207)))))),ap(ap(c_2Ewords_2Enzcv(A_27a),V0a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__min__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__min(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(ap(c_2Ewords_2Eword__lo(A_27a),V0a),V1b)),V0a),V1b) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__max__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__max(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(ap(c_2Ewords_2Eword__lo(A_27a),V0a),V1b)),V1b),V0a) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__smin__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__smin(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(ap(c_2Ewords_2Eword__lt(A_27a),V0a),V1b)),V0a),V1b) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__smax__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__smax(A_27a),V0a),V1b) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(ap(c_2Ewords_2Eword__lt(A_27a),V0a),V1b)),V1b),V0a) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__abs__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__abs(A_27a),V0w) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(ap(c_2Ewords_2Eword__lt(A_27a),V0w),ap(c_2Ewords_2En2w(A_27a),c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(A_27a),V0w)),V0w) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__lsl__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__lsl(A_27a),V0w),V1n) = ap(c_2Efcp_2EFCP(bool,A_27a),f2208(A_27a,V1n,V0w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__lsr__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__lsr(A_27a),V0w),V1n) = ap(c_2Efcp_2EFCP(bool,A_27a),f2209(A_27a,V0w,V1n)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__asr__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__asr(A_27a),V0w),V1n) = ap(c_2Efcp_2EFCP(bool,A_27a),f2210(A_27a,V1n,V0w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__ror__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__ror(A_27a),V0w),V1n) = ap(c_2Efcp_2EFCP(bool,A_27a),f2211(A_27a,V1n,V0w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__rol__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__rol(A_27a),V0w),V1n) = ap(ap(c_2Ewords_2Eword__ror(A_27a),V0w),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(ap(c_2Earithmetic_2EMOD,V1n),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__rrx__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0c] : ( mem(V0c,bool) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Eword__rrx(A_27a),ap(ap(c_2Epair_2E_2C(bool,ty_2Efcp_2Ecart(bool,A_27a)),V0c),V1w)) = ap(ap(c_2Epair_2E_2C(bool,ty_2Efcp_2Ecart(bool,A_27a)),ap(c_2Ewords_2Eword__lsb(A_27a),V1w)),ap(c_2Efcp_2EFCP(bool,A_27a),f2212(A_27a,V0c,V1w))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__lsl__bv__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__lsl__bv(A_27a),V0w),V1n) = ap(ap(c_2Ewords_2Eword__lsl(A_27a),V0w),ap(c_2Ewords_2Ew2n(A_27a),V1n)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__lsr__bv__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__lsr__bv(A_27a),V0w),V1n) = ap(ap(c_2Ewords_2Eword__lsr(A_27a),V0w),ap(c_2Ewords_2Ew2n(A_27a),V1n)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__asr__bv__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__asr__bv(A_27a),V0w),V1n) = ap(ap(c_2Ewords_2Eword__asr(A_27a),V0w),ap(c_2Ewords_2Ew2n(A_27a),V1n)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__ror__bv__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__ror__bv(A_27a),V0w),V1n) = ap(ap(c_2Ewords_2Eword__ror(A_27a),V0w),ap(c_2Ewords_2Ew2n(A_27a),V1n)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__rol__bv__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__rol__bv(A_27a),V0w),V1n) = ap(ap(c_2Ewords_2Eword__rol(A_27a),V0w),ap(c_2Ewords_2Ew2n(A_27a),V1n)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__join__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27b)) => ( ap(ap(c_2Ewords_2Eword__join(A_27a,A_27b),V0v),V1w) = ap(ap(c_2Ebool_2ELET(ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b)),ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b))),ap(ap(c_2Ebool_2ELET(ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b)),arr(ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b)),ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b)))),f2214(A_27b,A_27a)),ap(c_2Ewords_2Ew2w(A_27a,ty_2Esum_2Esum(A_27a,A_27b)),V0v))),ap(c_2Ewords_2Ew2w(A_27b,ty_2Esum_2Esum(A_27a,A_27b)),V1w)) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__concat__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27b)) => ( ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27c),V0v),V1w) = ap(c_2Ewords_2Ew2w(ty_2Esum_2Esum(A_27a,A_27b),A_27c),ap(ap(c_2Ewords_2Eword__join(A_27a,A_27b),V0v),V1w)) ) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Eword__replicate__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Eword__replicate(A_27a,A_27b),V0n),V1w) = ap(c_2Efcp_2EFCP(bool,A_27b),f2215(A_27a,V0n,V1w)) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Econcat__word__list__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ap(c_2Ewords_2Econcat__word__list(A_27a,A_27b),c_2Elist_2ENIL(ty_2Efcp_2Ecart(bool,A_27a))) = ap(c_2Ewords_2En2w(A_27b),c_2Enum_2E0) ) & ! [V0h] : ( mem(V0h,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(ty_2Efcp_2Ecart(bool,A_27a))) => ( ap(c_2Ewords_2Econcat__word__list(A_27a,A_27b),ap(ap(c_2Elist_2ECONS(ty_2Efcp_2Ecart(bool,A_27a)),V0h),V1t)) = ap(ap(c_2Ewords_2Eword__or(A_27b),ap(c_2Ewords_2Ew2w(A_27a,A_27b),V0h)),ap(ap(c_2Ewords_2Eword__lsl(A_27b),ap(c_2Ewords_2Econcat__word__list(A_27a,A_27b),V1t)),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))) ) ) ) ) ) ) )).
fof(ax_thm_2Ewords_2Esaturate__n2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2Esaturate__n2w(A_27a),V0n) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27a)),ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0n)),c_2Ewords_2Eword__T(A_27a)),ap(c_2Ewords_2En2w(A_27a),V0n)) ) ) ) )).
fof(ax_thm_2Ewords_2Esaturate__w2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2Esaturate__w2w(A_27a,A_27b),V0w) = ap(c_2Ewords_2Esaturate__n2w(A_27b),ap(c_2Ewords_2Ew2n(A_27a),V0w)) ) ) ) ) )).
fof(ax_thm_2Ewords_2Esaturate__add__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Esaturate__add(A_27a),V0a),V1b) = ap(c_2Ewords_2Esaturate__n2w(A_27a),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Ewords_2Ew2n(A_27a),V0a)),ap(c_2Ewords_2Ew2n(A_27a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Esaturate__sub__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Esaturate__sub(A_27a),V0a),V1b) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2Ew2n(A_27a),V0a)),ap(c_2Ewords_2Ew2n(A_27a),V1b))) ) ) ) ) )).
fof(ax_thm_2Ewords_2Esaturate__mul__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1b] : ( mem(V1b,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(ap(c_2Ewords_2Esaturate__mul(A_27a),V0a),V1b) = ap(c_2Ewords_2Esaturate__n2w(A_27a),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Ewords_2Ew2n(A_27a),V0a)),ap(c_2Ewords_2Ew2n(A_27a),V1b))) ) ) ) ) )).
fof(conj_thm_2Ewords_2EZERO__LT__dimword,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EDIMINDEX__GT__0,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2Edimword__IS__TWICE__INT__MIN,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))) )))).
fof(conj_thm_2Ewords_2Edimword__sub__int__min,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))) = ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a)) )))).
fof(conj_thm_2Ewords_2EONE__LT__dimword,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EEXISTS__HB,lemma,( ! [A_27a]: ( ne(A_27a) => ? [V0m] : ( mem(V0m,ty_2Enum_2Enum) & ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Enum_2ESUC,V0m) ) )))).
fof(conj_thm_2Ewords_2EMOD__DIMINDEX,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))) = ap(ap(ap(c_2Ebit_2EBITS,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),c_2Enum_2E0),V0n) ) )))).
fof(conj_thm_2Ewords_2EBITS__ZEROL__DIMINDEX,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) => ( ap(ap(ap(c_2Ebit_2EBITS,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),c_2Enum_2E0),V0n) = V0n ) ) )))).
fof(conj_thm_2Ewords_2EMOD__2EXP__DIMINDEX,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))) = ap(ap(c_2Ebit_2EMOD__2EXP,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0n) ) )))).
fof(conj_thm_2Ewords_2EINT__MIN__SUM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ap(c_2Ewords_2EINT__MIN(ty_2Esum_2Esum(A_27a,A_27b)),c_2Ebool_2Ethe__value(ty_2Esum_2Esum(A_27a,A_27b))) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2E_2F_5C,ap(c_2Epred__set_2EFINITE(A_27a),c_2Epred__set_2EUNIV(A_27a))),ap(c_2Epred__set_2EFINITE(A_27b),c_2Epred__set_2EUNIV(A_27b)))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MIN(A_27b),c_2Ebool_2Ethe__value(A_27b)))),ap(c_2Ewords_2EINT__MIN(ty_2Esum_2Esum(A_27a,A_27b)),c_2Ebool_2Ethe__value(ty_2Esum_2Esum(A_27a,A_27b)))) ))))).
fof(conj_thm_2Ewords_2EZERO__LT__INT__MIN,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EZERO__LT__INT__MAX,lemma,( ! [A_27a]: ( ne(A_27a) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a)))) )))).
fof(conj_thm_2Ewords_2EZERO__LE__INT__MAX,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Earithmetic_2E_3C_3D,c_2Enum_2E0),ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EZERO__LT__UINT__MAX,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EINT__MIN__LT__DIMWORD,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EINT__MAX__LT__DIMWORD,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2Edimindex__lt__dimword,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))))).
fof(conj_thm_2Ewords_2EBOUND__ORDER,lemma,( ! [A_27a]: ( ne(A_27a) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a)))) & ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a)))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) ) )))).
fof(conj_thm_2Ewords_2Edimindex__dimword__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) <=> ( ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Ewords_2Edimword(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) ))))).
fof(conj_thm_2Ewords_2Edimindex__dimword__le__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Edimword(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__dimword__lt__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2Edimword(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__int__min__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) <=> ( ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Ewords_2EINT__MIN(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) ))))).
fof(conj_thm_2Ewords_2Edimindex__int__min__le__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MIN(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__int__min__lt__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MIN(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__int__max__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) <=> ( ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Ewords_2EINT__MAX(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) ))))).
fof(conj_thm_2Ewords_2Edimindex__int__max__le__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MAX(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__int__max__lt__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EINT__MAX(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__uint__max__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) <=> ( ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Ewords_2EUINT__MAX(A_27b),c_2Ebool_2Ethe__value(A_27b)) ) ))))).
fof(conj_thm_2Ewords_2Edimindex__uint__max__le__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EUINT__MAX(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Edimindex__uint__max__lt__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2EUINT__MAX(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ewords_2EUINT__MAX(A_27b),c_2Ebool_2Ethe__value(A_27b)))) ))))).
fof(conj_thm_2Ewords_2Ew2n__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2Ew2n(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)) = ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) )))).
fof(conj_thm_2Ewords_2En2w__w2n,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ewords_2En2w(A_27a),ap(c_2Ewords_2Ew2n(A_27a),V0w)) = V0w ) )))).
fof(conj_thm_2Ewords_2Eword__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( V0w = ap(c_2Ewords_2En2w(A_27a),V1n) ) ) )))).
fof(conj_thm_2Ewords_2En2w__mod,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) = ap(c_2Ewords_2En2w(A_27a),V0n) ) )))).
fof(conj_thm_2Ewords_2En2w__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(c_2Ewords_2En2w(A_27a),V0m) = ap(c_2Ewords_2En2w(A_27a),V1n) ) <=> ( ap(ap(c_2Earithmetic_2EMOD,V0m),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))) = ap(ap(c_2Earithmetic_2EMOD,V1n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) ) ) )))).
fof(conj_thm_2Ewords_2Eranged__word__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( ( V0w = ap(c_2Ewords_2En2w(A_27a),V1n) ) & p(ap(ap(c_2Eprim__rec_2E_3C,V1n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) ) ) )))).
fof(conj_thm_2Ewords_2Edimindex__1__cases,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Efcp_2Ecart(bool,A_27a)) => ( ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) => ( ( V0a = ap(c_2Ewords_2En2w(A_27a),c_2Enum_2E0) ) | ( V0a = ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) )))).
fof(conj_thm_2Ewords_2Emod__dimindex,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) )))).
fof(conj_thm_2Ewords_2EWORD__INDUCT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Efcp_2Ecart(bool,A_27a),bool)) => ( ( p(ap(V0P,ap(c_2Ewords_2En2w(A_27a),c_2Enum_2E0))) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,V1n)),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) => ( p(ap(V0P,ap(c_2Ewords_2En2w(A_27a),V1n))) => p(ap(V0P,ap(c_2Ewords_2En2w(A_27a),ap(c_2Enum_2ESUC,V1n)))) ) ) ) ) => ! [V2x] : ( mem(V2x,ty_2Efcp_2Ecart(bool,A_27a)) => p(ap(V0P,V2x)) ) ) )))).
fof(conj_thm_2Ewords_2Ew2n__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ( ap(c_2Ewords_2Ew2n(A_27a),V0v) = ap(c_2Ewords_2Ew2n(A_27a),V1w) ) <=> ( V0v = V1w ) ) ) )))).
fof(conj_thm_2Ewords_2Ew2n__lt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ewords_2Ew2n(A_27a),V0w)),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) )))).
fof(conj_thm_2Ewords_2Eword__0__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ewords_2Ew2n(A_27a),ap(c_2Ewords_2En2w(A_27a),c_2Enum_2E0)) = c_2Enum_2E0 )))).
fof(conj_thm_2Ewords_2Eword__1__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ewords_2Ew2n(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) )))).
fof(conj_thm_2Ewords_2Ew2n__eq__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ( ap(c_2Ewords_2Ew2n(A_27a),V0w) = c_2Enum_2E0 ) <=> ( V0w = ap(c_2Ewords_2En2w(A_27a),c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Ewords_2En2w__dimword,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ewords_2En2w(A_27a),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))) = ap(c_2Ewords_2En2w(A_27a),c_2Enum_2E0) )))).
fof(conj_thm_2Ewords_2Eword__2comp__dimindex__1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ( ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) => ( ap(c_2Ewords_2Eword__2comp(A_27a),V0w) = V0w ) ) )))).
fof(conj_thm_2Ewords_2Eword__add__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__add(A_27a),ap(c_2Ewords_2En2w(A_27a),V0m)),ap(c_2Ewords_2En2w(A_27a),V1n)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__mul__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__mul(A_27a),ap(c_2Ewords_2En2w(A_27a),V0m)),ap(c_2Ewords_2En2w(A_27a),V1n)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__log2__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2Eword__log2(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)) = ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebit_2ELOG2,ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))) ) )))).
fof(conj_thm_2Ewords_2Eword__1comp__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2Eword__1comp(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))) ) )))).
fof(conj_thm_2Ewords_2Eword__2comp__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewords_2Eword__2comp(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))) ) )))).
fof(conj_thm_2Ewords_2Eword__lsb,lemma,( ! [A_27a]: ( ne(A_27a) => ( c_2Ewords_2Eword__lsb(A_27a) = ap(c_2Ewords_2Eword__bit(A_27a),c_2Enum_2E0) )))).
fof(conj_thm_2Ewords_2Eword__msb,lemma,( ! [A_27a]: ( ne(A_27a) => ( c_2Ewords_2Eword__msb(A_27a) = ap(c_2Ewords_2Eword__bit(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) )))).
fof(conj_thm_2Ewords_2Eword__lsb__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Ewords_2Eword__lsb(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n))) <=> p(ap(c_2Earithmetic_2EODD,V0n)) ) )))).
fof(conj_thm_2Ewords_2Eword__msb__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Ewords_2Eword__msb(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n))) <=> p(ap(ap(c_2Ebit_2EBIT,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0n)) ) )))).
fof(conj_thm_2Ewords_2Eword__msb__n2w__numeric,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Ewords_2Eword__msb(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Ewords_2EINT__MIN(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(ap(c_2Earithmetic_2EMOD,V0n),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a))))) ) )))).
fof(conj_thm_2Ewords_2Eword__and__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__and(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)),ap(c_2Ewords_2En2w(A_27a),V1m)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),c_2Ebool_2E_2F_5C),V0n),V1m)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__or__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__or(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)),ap(c_2Ewords_2En2w(A_27a),V1m)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),c_2Ebool_2E_5C_2F),V0n),V1m)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__xor__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__xor(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)),ap(c_2Ewords_2En2w(A_27a),V1m)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),f2217),V0n),V1m)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__nand__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__nand(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)),ap(c_2Ewords_2En2w(A_27a),V1m)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),f2219),V0n),V1m)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__nor__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__nor(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)),ap(c_2Ewords_2En2w(A_27a),V1m)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),f2221),V0n),V1m)) ) ) )))).
fof(conj_thm_2Ewords_2Eword__xnor__n2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__xnor(A_27a),ap(c_2Ewords_2En2w(A_27a),V0n)),ap(c_2Ewords_2En2w(A_27a),V1m)) = ap(c_2Ewords_2En2w(A_27a),ap(ap(ap(ap(c_2Ebit_2EBITWISE,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),c_2Emin_2E_3D(bool)),V0n),V1m)) ) ) )))).
fof(conj_thm_2Ewords_2El2w__w2l,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V0b)) => ( ap(ap(c_2Ewords_2El2w(A_27a),V0b),ap(ap(c_2Ewords_2Ew2l(A_27a),V0b),V1w)) = V1w ) ) ) )))).
fof(conj_thm_2Ewords_2Ew2l__l2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ewords_2Ew2l(A_27a),V0b),ap(ap(c_2Ewords_2El2w(A_27a),V0b),V1l)) = ap(ap(c_2Enumposrep_2En2l,V0b),ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Enumposrep_2El2n,V0b),V1l)),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) ) ) )))).
fof(conj_thm_2Ewords_2Es2w__w2s,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0c2n] : ( mem(V0c2n,arr(ty_2Estring_2Echar,ty_2Enum_2Enum)) => ! [V1n2c] : ( mem(V1n2c,arr(ty_2Enum_2Enum,ty_2Estring_2Echar)) => ! [V2b] : ( mem(V2b,ty_2Enum_2Enum) => ! [V3w] : ( mem(V3w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V2b)) & ! [V4x] : ( mem(V4x,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V4x),V2b)) => ( ap(V0c2n,ap(V1n2c,V4x)) = V4x ) ) ) ) => ( ap(ap(ap(c_2Ewords_2Es2w(A_27a),V2b),V0c2n),ap(ap(ap(c_2Ewords_2Ew2s(A_27a),V2b),V1n2c),V3w)) = V3w ) ) ) ) ) )))).
fof(conj_thm_2Ewords_2Ew2s__s2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1c2n] : ( mem(V1c2n,arr(ty_2Estring_2Echar,ty_2Enum_2Enum)) => ! [V2n2c] : ( mem(V2n2c,arr(ty_2Enum_2Enum,ty_2Estring_2Echar)) => ! [V3s] : ( mem(V3s,ty_2Elist_2Elist(ty_2Estring_2Echar)) => ( ap(ap(ap(c_2Ewords_2Ew2s(A_27a),V0b),V2n2c),ap(ap(ap(c_2Ewords_2Es2w(A_27a),V0b),V1c2n),V3s)) = ap(ap(ap(c_2EASCIInumbers_2En2s,V0b),V2n2c),ap(ap(c_2Earithmetic_2EMOD,ap(ap(ap(c_2EASCIInumbers_2Es2n,V0b),V1c2n),V3s)),ap(c_2Ewords_2Edimword(A_27a),c_2Ebool_2Ethe__value(A_27a)))) ) ) ) ) )))).
fof(conj_thm_2Ewords_2ENUMERAL__LESS__THM,lemma,(( ( ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n)))) <=> ( ( V0m = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) | p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ) ) ) & ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n)))) <=> ( ( V2m = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n)) ) | p(ap(ap(c_2Eprim__rec_2E_3C,V2m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n)))) ) ) ) ) ))).
fof(conj_thm_2Ewords_2Eword__bin__list,conjecture,( ! [A_27a]: ( ne(A_27a) => ( ap(ap(c_2Ecombin_2Eo(ty_2Efcp_2Ecart(bool,A_27a),ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(ty_2Enum_2Enum)),c_2Ewords_2Eword__from__bin__list(A_27a)),c_2Ewords_2Eword__to__bin__list(A_27a)) = c_2Ecombin_2EI(ty_2Efcp_2Ecart(bool,A_27a)) )))).
