include('Axioms/comparison+2.ax').
fof(mem_c_2Ebitstring_2Eadd,axiom,( mem(c_2Ebitstring_2Eadd,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Eband,axiom,( mem(c_2Ebitstring_2Eband,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Ebitify,axiom,( mem(c_2Ebitstring_2Ebitify,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(ty_2Enum_2Enum)))) )).
fof(mem_c_2Ebitstring_2Ebitwise,axiom,( mem(c_2Ebitstring_2Ebitwise,arr(arr(bool,arr(bool,bool)),arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool))))) )).
fof(mem_c_2Ebitstring_2Ebnand,axiom,( mem(c_2Ebitstring_2Ebnand,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Ebnor,axiom,( mem(c_2Ebitstring_2Ebnor,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Ebnot,axiom,( mem(c_2Ebitstring_2Ebnot,arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool))) )).
fof(mem_c_2Ebitstring_2Eboolify,axiom,( mem(c_2Ebitstring_2Eboolify,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Ebor,axiom,( mem(c_2Ebitstring_2Ebor,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Ebxnor,axiom,( mem(c_2Ebitstring_2Ebxnor,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Ebxor,axiom,( mem(c_2Ebitstring_2Ebxor,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Eextend,axiom,( mem(c_2Ebitstring_2Eextend,arr(bool,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool))))) )).
fof(mem_c_2Ebitstring_2Efield,axiom,( mem(c_2Ebitstring_2Efield,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool))))) )).
fof(mem_c_2Ebitstring_2Efield__insert,axiom,( mem(c_2Ebitstring_2Efield__insert,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))))) )).
fof(mem_c_2Ebitstring_2Efixwidth,axiom,( mem(c_2Ebitstring_2Efixwidth,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Emodify,axiom,( mem(c_2Ebitstring_2Emodify,arr(arr(ty_2Enum_2Enum,arr(bool,bool)),arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2En2v,axiom,( mem(c_2Ebitstring_2En2v,arr(ty_2Enum_2Enum,ty_2Elist_2Elist(bool))) )).
fof(mem_c_2Ebitstring_2Ereplicate,axiom,( mem(c_2Ebitstring_2Ereplicate,arr(ty_2Elist_2Elist(bool),arr(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Erev__count__list,axiom,( mem(c_2Ebitstring_2Erev__count__list,arr(ty_2Enum_2Enum,ty_2Elist_2Elist(ty_2Enum_2Enum))) )).
fof(mem_c_2Ebitstring_2Erotate,axiom,( mem(c_2Ebitstring_2Erotate,arr(ty_2Elist_2Elist(bool),arr(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Es2v,axiom,( mem(c_2Ebitstring_2Es2v,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(bool))) )).
fof(mem_c_2Ebitstring_2Eshiftl,axiom,( mem(c_2Ebitstring_2Eshiftl,arr(ty_2Elist_2Elist(bool),arr(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Eshiftr,axiom,( mem(c_2Ebitstring_2Eshiftr,arr(ty_2Elist_2Elist(bool),arr(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)))) )).
fof(mem_c_2Ebitstring_2Esign__extend,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebitstring_2Esign__extend(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Ebitstring_2Etestbit,axiom,( mem(c_2Ebitstring_2Etestbit,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),bool))) )).
fof(mem_c_2Ebitstring_2Ev2n,axiom,( mem(c_2Ebitstring_2Ev2n,arr(ty_2Elist_2Elist(bool),ty_2Enum_2Enum)) )).
fof(mem_c_2Ebitstring_2Ev2s,axiom,( mem(c_2Ebitstring_2Ev2s,arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(ty_2Estring_2Echar))) )).
fof(mem_c_2Ebitstring_2Ev2w,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebitstring_2Ev2w(A_27a),arr(ty_2Elist_2Elist(bool),ty_2Efcp_2Ecart(bool,A_27a))) ) )).
fof(mem_c_2Ebitstring_2Ew2v,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ebitstring_2Ew2v(A_27a),arr(ty_2Efcp_2Ecart(bool,A_27a),ty_2Elist_2Elist(bool))) ) )).
fof(mem_c_2Ebitstring_2Ezero__extend,axiom,( mem(c_2Ebitstring_2Ezero__extend,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(bool),ty_2Elist_2Elist(bool)))) )).
fof(ax_thm_2Ebitstring_2Eextend__def,axiom, ( ( ! [V0v0] : ( mem(V0v0,bool) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Eextend,V0v0),c_2Enum_2E0),V1l) = V1l ) ) ) ) & ! [V2c] : ( mem(V2c,bool) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Eextend,V2c),ap(c_2Enum_2ESUC,V3n)),V4l) = ap(ap(ap(c_2Ebitstring_2Eextend,V2c),V3n),ap(ap(c_2Elist_2ECONS(bool),V2c),V4l)) ) ) ) ) )).
fof(conj_thm_2Ebitstring_2Eextend__def__compute,lemma,(( ( ! [V0v0] : ( mem(V0v0,bool) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Eextend,V0v0),c_2Enum_2E0),V1l) = V1l ) ) ) ) & ( ( ! [V2c] : ( mem(V2c,bool) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Eextend,V2c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),V4l) = ap(ap(ap(c_2Ebitstring_2Eextend,V2c),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Elist_2ECONS(bool),V2c),V4l)) ) ) ) ) ) & ! [V5c] : ( mem(V5c,bool) => ! [V6n] : ( mem(V6n,ty_2Enum_2Enum) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Eextend,V5c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V6n))),V7l) = ap(ap(ap(c_2Ebitstring_2Eextend,V5c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V6n))),ap(ap(c_2Elist_2ECONS(bool),V5c),V7l)) ) ) ) ) ) ))).
fof(ax_thm_2Ebitstring_2Eboolify__def,axiom, ( ( ! [V0a] : ( mem(V0a,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Eboolify,V0a),c_2Elist_2ENIL(ty_2Enum_2Enum)) = V0a ) ) ) & ! [V1a] : ( mem(V1a,ty_2Elist_2Elist(bool)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ebitstring_2Eboolify,V1a),ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),V2n),V3l)) = ap(ap(c_2Ebitstring_2Eboolify,ap(ap(c_2Elist_2ECONS(bool),ap(c_2Ebool_2E_7E,ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V2n),c_2Enum_2E0))),V1a)),V3l) ) ) ) ) )).
fof(conj_thm_2Ebitstring_2Ebitify__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),arr(ty_2Elist_2Elist(bool),bool))) => ( ( ( ! [V1a] : ( mem(V1a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => p(ap(ap(V0P,V1a),c_2Elist_2ENIL(bool))) ) ) & ( ( ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(bool)) => ( p(ap(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),c_2Enum_2E0),V2a)),V3l)) => p(ap(ap(V0P,V2a),ap(ap(c_2Elist_2ECONS(bool),c_2Ebool_2EF),V3l))) ) ) ) ) & ! [V4a] : ( mem(V4a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ! [V5l] : ( mem(V5l,ty_2Elist_2Elist(bool)) => ( p(ap(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V4a)),V5l)) => p(ap(ap(V0P,V4a),ap(ap(c_2Elist_2ECONS(bool),c_2Ebool_2ET),V5l))) ) ) ) ) ) => ! [V6v] : ( mem(V6v,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ! [V7v1] : ( mem(V7v1,ty_2Elist_2Elist(bool)) => p(ap(ap(V0P,V6v),V7v1)) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Ebitify__def,lemma,(( ( ! [V0a] : ( mem(V0a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ebitstring_2Ebitify,V0a),c_2Elist_2ENIL(bool)) = V0a ) ) ) & ( ( ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(bool)) => ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ebitstring_2Ebitify,V2a),ap(ap(c_2Elist_2ECONS(bool),c_2Ebool_2EF),V1l)) = ap(ap(c_2Ebitstring_2Ebitify,ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),c_2Enum_2E0),V2a)),V1l) ) ) ) ) & ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(bool)) => ! [V4a] : ( mem(V4a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ebitstring_2Ebitify,V4a),ap(ap(c_2Elist_2ECONS(bool),c_2Ebool_2ET),V3l)) = ap(ap(c_2Ebitstring_2Ebitify,ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V4a)),V3l) ) ) ) ) ))).
fof(ax_thm_2Ebitstring_2En2v__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ebitstring_2En2v,V0n) = ap(ap(c_2Ebitstring_2Eboolify,c_2Elist_2ENIL(bool)),ap(c_2Enumposrep_2Enum__to__bin__list,V0n)) ) )).
fof(ax_thm_2Ebitstring_2Ev2n__def,axiom, ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(bool)) => ( ap(c_2Ebitstring_2Ev2n,V0l) = ap(c_2Enumposrep_2Enum__from__bin__list,ap(ap(c_2Ebitstring_2Ebitify,c_2Elist_2ENIL(ty_2Enum_2Enum)),V0l)) ) )).
fof(ax_thm_2Ebitstring_2Es2v__def,axiom, ( c_2Ebitstring_2Es2v = ap(c_2Elist_2EMAP(ty_2Estring_2Echar,bool),f2288) )).
fof(ax_thm_2Ebitstring_2Ev2s__def,axiom, ( c_2Ebitstring_2Ev2s = ap(c_2Elist_2EMAP(bool,ty_2Estring_2Echar),f2289) )).
fof(ax_thm_2Ebitstring_2Ezero__extend__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Ezero__extend,V0n),V1v) = ap(ap(ap(c_2Elist_2EPAD__LEFT(bool),c_2Ebool_2EF),V0n),V1v) ) ) )).
fof(ax_thm_2Ebitstring_2Esign__extend__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Ebitstring_2Esign__extend(A_27a),V0n),V1v) = ap(ap(ap(c_2Elist_2EPAD__LEFT(A_27a),ap(c_2Elist_2EHD(A_27a),V1v)),V0n),V1v) ) ) ) ) )).
fof(ax_thm_2Ebitstring_2Efixwidth__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1v) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)),f2290(V0n,V1v)),ap(c_2Elist_2ELENGTH(bool),V1v)) ) ) )).
fof(ax_thm_2Ebitstring_2Eshiftl__def,axiom, ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ebitstring_2Eshiftl,V0v),V1m) = ap(ap(ap(c_2Elist_2EPAD__RIGHT(bool),c_2Ebool_2EF),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(bool),V0v)),V1m)),V0v) ) ) )).
fof(ax_thm_2Ebitstring_2Eshiftr__def,axiom, ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ebitstring_2Eshiftr,V0v),V1m) = ap(ap(c_2Elist_2ETAKE(bool),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(bool),V0v)),V1m)),V0v) ) ) )).
fof(ax_thm_2Ebitstring_2Efield__def,axiom, ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Efield,V0h),V1l),V2v) = ap(ap(c_2Ebitstring_2Efixwidth,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0h)),V1l)),ap(ap(c_2Ebitstring_2Eshiftr,V2v),V1l)) ) ) ) )).
fof(ax_thm_2Ebitstring_2Erotate__def,axiom, ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Ebitstring_2Erotate,V0v),V1m) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)),f2292(V0v,V1m)),ap(c_2Elist_2ELENGTH(bool),V0v)) ) ) )).
fof(ax_thm_2Ebitstring_2Etestbit__def,axiom, ! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Ebitstring_2Etestbit,V0b),V1v)) <=> ( ap(ap(ap(c_2Ebitstring_2Efield,V0b),V0b),V1v) = ap(ap(c_2Elist_2ECONS(bool),c_2Ebool_2ET),c_2Elist_2ENIL(bool)) ) ) ) )).
fof(ax_thm_2Ebitstring_2Ew2v__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ebitstring_2Ew2v(A_27a),V0w) = ap(ap(c_2Elist_2EGENLIST(bool),f2182(A_27a,V0w)),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))) ) ) ) )).
fof(ax_thm_2Ebitstring_2Ev2w__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ebitstring_2Ev2w(A_27a),V0v) = ap(c_2Efcp_2EFCP(bool,A_27a),f2293(V0v)) ) ) ) )).
fof(ax_thm_2Ebitstring_2Erev__count__list__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ebitstring_2Erev__count__list,V0n) = ap(ap(c_2Elist_2EGENLIST(ty_2Enum_2Enum),f2294(V0n)),V0n) ) )).
fof(ax_thm_2Ebitstring_2Emodify__def,axiom, ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(bool,bool))) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Emodify,V0f),V1v) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(ty_2Enum_2Enum,bool),bool),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,bool,bool),V0f)),ap(c_2Elist_2EZIP(ty_2Enum_2Enum,bool),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Elist_2Elist(bool)),ap(c_2Ebitstring_2Erev__count__list,ap(c_2Elist_2ELENGTH(bool),V1v))),V1v))) ) ) )).
fof(ax_thm_2Ebitstring_2Efield__insert__def,axiom, ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2s] : ( mem(V2s,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Efield__insert,V0h),V1l),V2s) = ap(c_2Ebitstring_2Emodify,f2295(V0h,V1l,V2s)) ) ) ) )).
fof(ax_thm_2Ebitstring_2Eadd__def,axiom, ! [V0a] : ( mem(V0a,ty_2Elist_2Elist(bool)) => ! [V1b] : ( mem(V1b,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Eadd,V0a),V1b) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)),f2296(V0a,V1b)),ap(ap(c_2Earithmetic_2EMAX,ap(c_2Elist_2ELENGTH(bool),V0a)),ap(c_2Elist_2ELENGTH(bool),V1b))) ) ) )).
fof(ax_thm_2Ebitstring_2Ebitwise__def,axiom, ! [V0f] : ( mem(V0f,arr(bool,arr(bool,bool))) => ! [V1v1] : ( mem(V1v1,ty_2Elist_2Elist(bool)) => ! [V2v2] : ( mem(V2v2,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Ebitwise,V0f),V1v1),V2v2) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)),f2297(V1v1,V2v2,V0f)),ap(ap(c_2Earithmetic_2EMAX,ap(c_2Elist_2ELENGTH(bool),V1v1)),ap(c_2Elist_2ELENGTH(bool),V2v2))) ) ) ) )).
fof(ax_thm_2Ebitstring_2Ebnot__def,axiom, ( c_2Ebitstring_2Ebnot = ap(c_2Elist_2EMAP(bool,bool),c_2Ebool_2E_7E) )).
fof(ax_thm_2Ebitstring_2Ebor__def,axiom, ( c_2Ebitstring_2Ebor = ap(c_2Ebitstring_2Ebitwise,c_2Ebool_2E_5C_2F) )).
fof(ax_thm_2Ebitstring_2Eband__def,axiom, ( c_2Ebitstring_2Eband = ap(c_2Ebitstring_2Ebitwise,c_2Ebool_2E_2F_5C) )).
fof(ax_thm_2Ebitstring_2Ebxor__def,axiom, ( c_2Ebitstring_2Ebxor = ap(c_2Ebitstring_2Ebitwise,f2171) )).
fof(ax_thm_2Ebitstring_2Ebnor__def,axiom, ( c_2Ebitstring_2Ebnor = ap(c_2Ebitstring_2Ebitwise,f2299) )).
fof(ax_thm_2Ebitstring_2Ebxnor__def,axiom, ( c_2Ebitstring_2Ebxnor = ap(c_2Ebitstring_2Ebitwise,c_2Emin_2E_3D(bool)) )).
fof(ax_thm_2Ebitstring_2Ebnand__def,axiom, ( c_2Ebitstring_2Ebnand = ap(c_2Ebitstring_2Ebitwise,f2301) )).
fof(ax_thm_2Ebitstring_2Ereplicate__def,axiom, ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ebitstring_2Ereplicate,V0v),V1n) = ap(c_2Elist_2EFLAT(bool),ap(ap(c_2Elist_2EGENLIST(ty_2Elist_2Elist(bool)),ap(c_2Ecombin_2EK(ty_2Elist_2Elist(bool),ty_2Enum_2Enum),V0v)),V1n)) ) ) )).
fof(conj_thm_2Ebitstring_2Eextend__cons,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1c] : ( mem(V1c,bool) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Eextend,V1c),ap(c_2Enum_2ESUC,V0n)),V2l) = ap(ap(c_2Elist_2ECONS(bool),V1c),ap(ap(ap(c_2Ebitstring_2Eextend,V1c),V0n),V2l)) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Epad__left__extend,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(bool)) => ! [V2c] : ( mem(V2c,bool) => ( ap(ap(ap(c_2Elist_2EPAD__LEFT(bool),V2c),V0n),V1l) = ap(ap(ap(c_2Ebitstring_2Eextend,V2c),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(bool),V1l))),V1l) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eextend,lemma,(( ( ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Ezero__extend,V0n),V1v) = ap(ap(ap(c_2Ebitstring_2Eextend,c_2Ebool_2EF),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(bool),V1v))),V1v) ) ) ) ) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3v] : ( mem(V3v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Esign__extend(bool),V2n),V3v) = ap(ap(ap(c_2Ebitstring_2Eextend,ap(c_2Elist_2EHD(bool),V3v)),ap(ap(c_2Earithmetic_2E_2D,V2n),ap(c_2Elist_2ELENGTH(bool),V3v))),V3v) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Efixwidth,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1v) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Elist_2Elist(bool)),f2302(V0n,V1v)),ap(c_2Elist_2ELENGTH(bool),V1v)) ) ) ))).
fof(conj_thm_2Ebitstring_2Efixwidth__id,lemma,(! [V0w] : ( mem(V0w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Elist_2ELENGTH(bool),V0w)),V0w) = V0w ) ))).
fof(conj_thm_2Ebitstring_2Efixwidth__id__imp,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ( V0n = ap(c_2Elist_2ELENGTH(bool),V1w) ) => ( ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1w) = V1w ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eboolify__reverse__map,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ! [V1a] : ( mem(V1a,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Eboolify,V1a),V0v) = ap(ap(c_2Elist_2EAPPEND(bool),ap(c_2Elist_2EREVERSE(bool),ap(ap(c_2Elist_2EMAP(ty_2Enum_2Enum,bool),f2303),V0v))),V1a) ) ) ))).
fof(conj_thm_2Ebitstring_2Ebitify__reverse__map,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1a] : ( mem(V1a,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Ebitstring_2Ebitify,V1a),V0v) = ap(ap(c_2Elist_2EAPPEND(ty_2Enum_2Enum),ap(c_2Elist_2EREVERSE(ty_2Enum_2Enum),ap(ap(c_2Elist_2EMAP(bool,ty_2Enum_2Enum),f2304),V0v))),V1a) ) ) ))).
fof(conj_thm_2Ebitstring_2Eevery__bit__bitify,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => p(ap(ap(c_2Elist_2EEVERY(ty_2Enum_2Enum),ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ebitstring_2Ebitify,c_2Elist_2ENIL(ty_2Enum_2Enum)),V0v))) ))).
fof(conj_thm_2Ebitstring_2Elength__pad__left,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(ap(c_2Elist_2EPAD__LEFT(A_27a),V0x),V1n),V2a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V2a)),V1n)),V1n),ap(c_2Elist_2ELENGTH(A_27a),V2a)) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Elength__pad__right,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(ap(c_2Elist_2EPAD__RIGHT(A_27a),V0x),V1n),V2a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V2a)),V1n)),V1n),ap(c_2Elist_2ELENGTH(A_27a),V2a)) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Elength__zero__extend,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(bool),V1v)),V0n)) => ( ap(c_2Elist_2ELENGTH(bool),ap(ap(c_2Ebitstring_2Ezero__extend,V0n),V1v)) = V0n ) ) ) ))).
fof(conj_thm_2Ebitstring_2Elength__sign__extend,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V1v)),V0n)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Ebitstring_2Esign__extend(A_27a),V0n),V1v)) = V0n ) ) ) )))).
fof(conj_thm_2Ebitstring_2Elength__fixwidth,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(c_2Elist_2ELENGTH(bool),ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1v)) = V0n ) ) ))).
fof(conj_thm_2Ebitstring_2Elength__field,lemma,(! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( ap(c_2Elist_2ELENGTH(bool),ap(ap(ap(c_2Ebitstring_2Efield,V0h),V1l),V2v)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0h)),V1l) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Elength__bitify,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(c_2Elist_2ELENGTH(ty_2Enum_2Enum),ap(ap(c_2Ebitstring_2Ebitify,V1l),V0v)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(ty_2Enum_2Enum),V1l)),ap(c_2Elist_2ELENGTH(bool),V0v)) ) ) ))).
fof(conj_thm_2Ebitstring_2Elength__bitify__null,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1l] : ( mem(V1l,A_27a) => ( ap(c_2Elist_2ELENGTH(ty_2Enum_2Enum),ap(ap(c_2Ebitstring_2Ebitify,c_2Elist_2ENIL(ty_2Enum_2Enum)),V0v)) = ap(c_2Elist_2ELENGTH(bool),V0v) ) ) )))).
fof(conj_thm_2Ebitstring_2Elength__shiftr,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Elist_2ELENGTH(bool),ap(ap(c_2Ebitstring_2Eshiftr,V0v),V1n)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(bool),V0v)),V1n) ) ) ))).
fof(conj_thm_2Ebitstring_2Elength__rev__count__list,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Elist_2ELENGTH(ty_2Enum_2Enum),ap(c_2Ebitstring_2Erev__count__list,V0n)) = V0n ) ))).
fof(conj_thm_2Ebitstring_2Elength__w2v,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Elist_2ELENGTH(bool),ap(c_2Ebitstring_2Ew2v(A_27a),V0w)) = ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)) ) )))).
fof(conj_thm_2Ebitstring_2Elength__rotate,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Elist_2ELENGTH(bool),ap(ap(c_2Ebitstring_2Erotate,V0v),V1n)) = ap(c_2Elist_2ELENGTH(bool),V0v) ) ) ))).
fof(conj_thm_2Ebitstring_2Eel__rev__count__list,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1i),V0n)) => ( ap(ap(c_2Elist_2EEL(ty_2Enum_2Enum),V1i),ap(c_2Ebitstring_2Erev__count__list,V0n)) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V1i) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eel__zero__extend,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Elist_2EEL(bool),V1i),ap(ap(c_2Ebitstring_2Ezero__extend,V0n),V2v))) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(bool),V2v))),V1i)) & p(ap(ap(c_2Elist_2EEL(bool),ap(ap(c_2Earithmetic_2E_2D,V1i),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(bool),V2v)))),V2v)) ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eel__sign__extend,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EEL(A_27a),V1i),ap(ap(c_2Ebitstring_2Esign__extend(A_27a),V0n),V2v)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Eprim__rec_2E_3C,V1i),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V2v)))),ap(ap(c_2Elist_2EEL(A_27a),c_2Enum_2E0),V2v)),ap(ap(c_2Elist_2EEL(A_27a),ap(ap(c_2Earithmetic_2E_2D,V1i),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V2v)))),V2v)) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Eel__fixwidth,lemma,(! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2w] : ( mem(V2w,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0i),V1n)) => ( p(ap(ap(c_2Elist_2EEL(bool),V0i),ap(ap(c_2Ebitstring_2Efixwidth,V1n),V2w))) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(bool),V2w)),V1n)),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,V1n),ap(c_2Elist_2ELENGTH(bool),V2w))),V0i)),ap(ap(c_2Elist_2EEL(bool),ap(ap(c_2Earithmetic_2E_2D,V0i),ap(ap(c_2Earithmetic_2E_2D,V1n),ap(c_2Elist_2ELENGTH(bool),V2w)))),V2w))),ap(ap(c_2Elist_2EEL(bool),ap(ap(c_2Earithmetic_2E_2B,V0i),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(bool),V2w)),V1n))),V2w))) ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eel__field,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1h] : ( mem(V1h,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Enum_2Enum) => ! [V3i] : ( mem(V3i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3i),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V1h)),V2l))) => ( p(ap(ap(c_2Elist_2EEL(bool),V3i),ap(ap(ap(c_2Ebitstring_2Efield,V1h),V2l),V0v))) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V1h)),ap(ap(c_2Earithmetic_2E_2B,V3i),ap(c_2Elist_2ELENGTH(bool),V0v)))) & p(ap(ap(c_2Elist_2EEL(bool),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V3i),ap(c_2Elist_2ELENGTH(bool),V0v))),ap(c_2Enum_2ESUC,V1h))),V0v)) ) ) ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eel__w2v,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1n),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))) => ( p(ap(ap(c_2Elist_2EEL(bool),V1n),ap(c_2Ebitstring_2Ew2v(A_27a),V0w))) <=> p(ap(ap(c_2Efcp_2Efcp__index(bool,A_27a),V0w),ap(ap(c_2Earithmetic_2E_2D,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)))),V1n))) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Eel__shiftr,lemma,(! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3d] : ( mem(V3d,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V2n),V3d)) & ( p(ap(ap(c_2Eprim__rec_2E_3C,V0i),ap(ap(c_2Earithmetic_2E_2D,V3d),V2n))) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V3d)) ) ) => ( p(ap(ap(c_2Elist_2EEL(bool),V0i),ap(ap(c_2Ebitstring_2Eshiftr,ap(ap(c_2Ebitstring_2Efixwidth,V3d),V1v)),V2n))) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V3d),ap(ap(c_2Earithmetic_2E_2B,V0i),ap(c_2Elist_2ELENGTH(bool),V1v)))) & p(ap(ap(c_2Elist_2EEL(bool),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V0i),ap(c_2Elist_2ELENGTH(bool),V1v))),V3d)),V1v)) ) ) ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eshiftr__0,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Eshiftr,V0v),c_2Enum_2E0) = V0v ) ))).
fof(conj_thm_2Ebitstring_2Efield__fixwidth,lemma,(! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ebitstring_2Efield,V0h),c_2Enum_2E0),V1v) = ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Enum_2ESUC,V0h)),V1v) ) ) ))).
fof(conj_thm_2Ebitstring_2Etestbit,lemma,(! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Ebitstring_2Etestbit,V0b),V1v)) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,bool),f2305(V1v,V0b)),ap(c_2Elist_2ELENGTH(bool),V1v))) ) ) ))).
fof(conj_thm_2Ebitstring_2Etestbit__geq__len,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(bool),V0v)),V1i)) => ( ~~ p(ap(ap(c_2Ebitstring_2Etestbit,V1i),V0v)) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Etestbit__el,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1i),ap(c_2Elist_2ELENGTH(bool),V0v))) => ( p(ap(ap(c_2Ebitstring_2Etestbit,V1i),V0v)) <=> p(ap(ap(c_2Elist_2EEL(bool),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(bool),V0v)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V1i)),V0v)) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Ebit__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Ewords_2Eword__bit(A_27a),V0n),ap(c_2Ebitstring_2Ev2w(A_27a),V1v))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))) & p(ap(ap(c_2Ebitstring_2Etestbit,V0n),V1v)) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__index__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0index_20too_20large] : ( mem(V0index_20too_20large,bool) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Efcp_2Efcp__index(bool,A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)),V2i)) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2Eprim__rec_2E_3C,V2i),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))),ap(ap(c_2Ebitstring_2Etestbit,V2i),V1v)),ap(ap(ap(ap(c_2Ecombin_2EFAIL(arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Enum_2Enum,bool)),bool),c_2Efcp_2Efcp__index(bool,A_27a)),V0index_20too_20large),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)),V2i))) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Etestbit__w2v,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1w] : ( mem(V1w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ebitstring_2Etestbit,V0n),ap(c_2Ebitstring_2Ew2v(A_27a),V1w))) <=> p(ap(ap(c_2Ewords_2Eword__bit(A_27a),V0n),V1w)) ) ) )))).
fof(conj_thm_2Ebitstring_2Ew2v__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ebitstring_2Ew2v(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v) ) )))).
fof(conj_thm_2Ebitstring_2Ev2w__w2v,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ( ap(c_2Ebitstring_2Ev2w(A_27a),ap(c_2Ebitstring_2Ew2v(A_27a),V0w)) = V0w ) )))).
fof(conj_thm_2Ebitstring_2Ev2w__fixwidth,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v)) = ap(c_2Ebitstring_2Ev2w(A_27a),V0v) ) )))).
fof(conj_thm_2Ebitstring_2Efixwidth__fixwidth,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ebitstring_2Efixwidth,V0n),ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1v)) = ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1v) ) ) ))).
fof(conj_thm_2Ebitstring_2Ebitstring__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ? [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) & ( V0w = ap(c_2Ebitstring_2Ev2w(A_27a),V1v) ) ) )))).
fof(conj_thm_2Ebitstring_2Eranged__bitstring__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Efcp_2Ecart(bool,A_27a)) => ? [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) & ( ( V0w = ap(c_2Ebitstring_2Ev2w(A_27a),V1v) ) & p(ap(c_2Emarker_2EAbbrev,ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),ap(c_2Elist_2ELENGTH(bool),V1v)),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))))) ) ) )))).
fof(conj_thm_2Ebitstring_2Efixwidth__eq,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ! [V2w] : ( mem(V2w,ty_2Elist_2Elist(bool)) => ( ( ap(ap(c_2Ebitstring_2Efixwidth,V0n),V1v) = ap(ap(c_2Ebitstring_2Efixwidth,V0n),V2w) ) <=> ! [V3i] : ( mem(V3i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3i),V0n)) => ( p(ap(ap(c_2Ebitstring_2Etestbit,V3i),V1v)) <=> p(ap(ap(c_2Ebitstring_2Etestbit,V3i),V2w)) ) ) ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Ev2w__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ( ap(c_2Ebitstring_2Ev2w(A_27a),V0v) = ap(c_2Ebitstring_2Ev2w(A_27a),V1w) ) <=> ( ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v) = ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1w) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Efield__concat__right,lemma,(! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1a] : ( mem(V1a,ty_2Elist_2Elist(bool)) => ! [V2b] : ( mem(V2b,ty_2Elist_2Elist(bool)) => ( ( ap(c_2Elist_2ELENGTH(bool),V2b) = ap(c_2Enum_2ESUC,V0h) ) => ( ap(ap(ap(c_2Ebitstring_2Efield,V0h),c_2Enum_2E0),ap(ap(c_2Elist_2EAPPEND(bool),V1a),V2b)) = V2b ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Efield__concat__left,lemma,(! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(bool)) => ! [V3b] : ( mem(V3b,ty_2Elist_2Elist(bool)) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1l),V0h)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(bool),V3b)),V1l)) ) => ( ap(ap(ap(c_2Ebitstring_2Efield,V0h),V1l),ap(ap(c_2Elist_2EAPPEND(bool),V2a),V3b)) = ap(ap(ap(c_2Ebitstring_2Efield,ap(ap(c_2Earithmetic_2E_2D,V0h),ap(c_2Elist_2ELENGTH(bool),V3b))),ap(ap(c_2Earithmetic_2E_2D,V1l),ap(c_2Elist_2ELENGTH(bool),V3b))),V2a) ) ) ) ) ) ))).
fof(conj_thm_2Ebitstring_2Efield__id__imp,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ( ap(c_2Enum_2ESUC,V0n) = ap(c_2Elist_2ELENGTH(bool),V1v) ) => ( ap(ap(ap(c_2Ebitstring_2Efield,V0n),c_2Enum_2E0),V1v) = V1v ) ) ) ))).
fof(conj_thm_2Ebitstring_2Eshiftl__replicate__F,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ebitstring_2Eshiftl,V0v),V1n) = ap(ap(c_2Elist_2EAPPEND(bool),V0v),ap(ap(c_2Ebitstring_2Ereplicate,ap(ap(c_2Elist_2ECONS(bool),c_2Ebool_2EF),c_2Elist_2ENIL(bool))),V1n)) ) ) ))).
fof(conj_thm_2Ebitstring_2Eword__lsb__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( p(ap(c_2Ewords_2Eword__lsb(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v))) <=> ( ( ~~ ( V0v = c_2Elist_2ENIL(bool) ) ) & p(ap(c_2Elist_2ELAST(bool),V0v)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__msb__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( p(ap(c_2Ewords_2Eword__msb(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v))) <=> p(ap(ap(c_2Ebitstring_2Etestbit,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)))),V0v)) ) )))).
fof(conj_thm_2Ebitstring_2Ew2w__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Ew2w(A_27a,A_27b),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(c_2Ebitstring_2Ev2w(A_27b),ap(ap(c_2Ebitstring_2Efixwidth,ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(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_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))),V0v)) ) ))))).
fof(conj_thm_2Ebitstring_2Esw2sw__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Esw2sw(A_27a,A_27b),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27b)),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)))),ap(c_2Ebitstring_2Ev2w(A_27b),ap(ap(c_2Ebitstring_2Esign__extend(bool),ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v)))),ap(c_2Ebitstring_2Ev2w(A_27b),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),V0v))) ) ))))).
fof(conj_thm_2Ebitstring_2En2w__v2n,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V0v)) = ap(c_2Ebitstring_2Ev2w(A_27a),V0v) ) )))).
fof(conj_thm_2Ebitstring_2Ev2n__n2v,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ebitstring_2Ev2n,ap(c_2Ebitstring_2En2v,V0n)) = V0n ) ))).
fof(conj_thm_2Ebitstring_2Ev2w__n2v,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ebitstring_2Ev2w(A_27a),ap(c_2Ebitstring_2En2v,V0n)) = ap(c_2Ewords_2En2w(A_27a),V0n) ) )))).
fof(conj_thm_2Ebitstring_2Ew2n__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Ew2n(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(ap(c_2Ebit_2EMOD__2EXP,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),ap(c_2Ebitstring_2Ev2n,V0v)) ) )))).
fof(conj_thm_2Ebitstring_2Ev2n__lt,lemma,(! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Ebitstring_2Ev2n,V0v)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ap(c_2Elist_2ELENGTH(bool),V0v)))) ))).
fof(conj_thm_2Ebitstring_2Eword__and__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__and(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)),ap(c_2Ebitstring_2Ev2w(A_27a),V1w)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Eband,V0v),V1w)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__or__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__or(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)),ap(c_2Ebitstring_2Ev2w(A_27a),V1w)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Ebor,V0v),V1w)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__xor__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__xor(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)),ap(c_2Ebitstring_2Ev2w(A_27a),V1w)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Ebxor,V0v),V1w)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__nand__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__nand(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)),ap(c_2Ebitstring_2Ev2w(A_27a),V1w)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Ebnand,ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v)),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1w))) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__nor__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__nor(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)),ap(c_2Ebitstring_2Ev2w(A_27a),V1w)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Ebnor,ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v)),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1w))) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__xnor__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1w] : ( mem(V1w,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__xnor(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)),ap(c_2Ebitstring_2Ev2w(A_27a),V1w)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Ebxnor,ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v)),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1w))) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__1comp__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Eword__1comp(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(c_2Ebitstring_2Ebnot,ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v))) ) )))).
fof(conj_thm_2Ebitstring_2Eword__lsl__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__lsl(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)),V0n) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Eshiftl,V1v),V0n)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__lsr__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__lsr(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)),V0n) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Eshiftr,ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1v)),V0n)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__modify__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,arr(bool,bool))) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__modify(A_27a),V0f),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Emodify,V0f),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1v))) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__bits__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ewords_2Eword__bits(A_27a),V0h),V1l),ap(c_2Ebitstring_2Ev2w(A_27a),V2v)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(ap(c_2Ebitstring_2Efield,V0h),V1l),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V2v))) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__extract__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ewords_2Eword__extract(A_27a,A_27b),V0h),V1l),ap(c_2Ebitstring_2Ev2w(A_27a),V2v)) = ap(c_2Ewords_2Ew2w(A_27a,A_27b),ap(ap(ap(c_2Ewords_2Eword__bits(A_27a),V0h),V1l),ap(c_2Ebitstring_2Ev2w(A_27a),V2v))) ) ) ) ))))).
fof(conj_thm_2Ebitstring_2Eword__slice__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( ap(ap(ap(c_2Ewords_2Eword__slice(A_27a),V0h),V1l),ap(c_2Ebitstring_2Ev2w(A_27a),V2v)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Eshiftl,ap(ap(ap(c_2Ebitstring_2Efield,V0h),V1l),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V2v))),V1l)) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__asr__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__asr(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)),V0n) = ap(ap(c_2Ebool_2ELET(ty_2Elist_2Elist(bool),ty_2Efcp_2Ecart(bool,A_27a)),f2306(A_27a,V0n)),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1v)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__ror__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__ror(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)),V0n) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(ap(c_2Ebitstring_2Erotate,ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1v)),V0n)) ) ) )))).
fof(conj_thm_2Ebitstring_2Eword__reverse__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Eword__reverse(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(c_2Ebitstring_2Ev2w(A_27a),ap(c_2Elist_2EREVERSE(bool),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V0v))) ) )))).
fof(conj_thm_2Ebitstring_2Eword__join__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v1] : ( mem(V0v1,ty_2Elist_2Elist(bool)) => ! [V1v2] : ( mem(V1v2,ty_2Elist_2Elist(bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),c_2Epred__set_2EUNIV(A_27a))) & p(ap(c_2Epred__set_2EFINITE(A_27b),c_2Epred__set_2EUNIV(A_27b))) ) => ( ap(ap(c_2Ewords_2Eword__join(A_27a,A_27b),ap(c_2Ebitstring_2Ev2w(A_27a),V0v1)),ap(c_2Ebitstring_2Ev2w(A_27b),V1v2)) = ap(c_2Ebitstring_2Ev2w(ty_2Esum_2Esum(A_27a,A_27b)),ap(ap(c_2Elist_2EAPPEND(bool),V0v1),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),V1v2))) ) ) ) ))))).
fof(conj_thm_2Ebitstring_2Eword__concat__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0v1] : ( mem(V0v1,ty_2Elist_2Elist(bool)) => ! [V1v2] : ( mem(V1v2,ty_2Elist_2Elist(bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),c_2Epred__set_2EUNIV(A_27a))) & p(ap(c_2Epred__set_2EFINITE(A_27b),c_2Epred__set_2EUNIV(A_27b))) ) => ( ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27c),ap(c_2Ebitstring_2Ev2w(A_27a),V0v1)),ap(c_2Ebitstring_2Ev2w(A_27b),V1v2)) = ap(c_2Ebitstring_2Ev2w(A_27c),ap(ap(c_2Ebitstring_2Efixwidth,ap(ap(c_2Earithmetic_2EMIN,ap(c_2Efcp_2Edimindex(A_27c),c_2Ebool_2Ethe__value(A_27c))),ap(ap(c_2Earithmetic_2E_2B,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(ap(c_2Elist_2EAPPEND(bool),V0v1),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),V1v2)))) ) ) ) )))))).
fof(conj_thm_2Ebitstring_2Eword__join__v2w__rwt,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0bad_20domain] : ( mem(V0bad_20domain,bool) => ! [V1v1] : ( mem(V1v1,ty_2Elist_2Elist(bool)) => ! [V2v2] : ( mem(V2v2,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__join(A_27a,A_27b),ap(c_2Ebitstring_2Ev2w(A_27a),V1v1)),ap(c_2Ebitstring_2Ev2w(A_27b),V2v2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,ty_2Esum_2Esum(A_27a,A_27b))),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(c_2Ebitstring_2Ev2w(ty_2Esum_2Esum(A_27a,A_27b)),ap(ap(c_2Elist_2EAPPEND(bool),V1v1),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),V2v2)))),ap(ap(ap(ap(c_2Ecombin_2EFAIL(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)))),bool),c_2Ewords_2Eword__join(A_27a,A_27b)),V0bad_20domain),ap(c_2Ebitstring_2Ev2w(A_27a),V1v1)),ap(c_2Ebitstring_2Ev2w(A_27b),V2v2))) ) ) ) ))))).
fof(conj_thm_2Ebitstring_2Eword__concat__v2w__rwt,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0bad_20domain] : ( mem(V0bad_20domain,bool) => ! [V1v1] : ( mem(V1v1,ty_2Elist_2Elist(bool)) => ! [V2v2] : ( mem(V2v2,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27c),ap(c_2Ebitstring_2Ev2w(A_27a),V1v1)),ap(c_2Ebitstring_2Ev2w(A_27b),V2v2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,A_27c)),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(c_2Ebitstring_2Ev2w(A_27c),ap(ap(c_2Ebitstring_2Efixwidth,ap(ap(c_2Earithmetic_2EMIN,ap(c_2Efcp_2Edimindex(A_27c),c_2Ebool_2Ethe__value(A_27c))),ap(ap(c_2Earithmetic_2E_2B,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(ap(c_2Elist_2EAPPEND(bool),V1v1),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),V2v2))))),ap(ap(ap(ap(c_2Ecombin_2EFAIL(arr(ty_2Efcp_2Ecart(bool,A_27a),arr(ty_2Efcp_2Ecart(bool,A_27b),ty_2Efcp_2Ecart(bool,A_27c))),bool),c_2Ewords_2Eword__concat(A_27a,A_27b,A_27c)),V0bad_20domain),ap(c_2Ebitstring_2Ev2w(A_27a),V1v1)),ap(c_2Ebitstring_2Ev2w(A_27b),V2v2))) ) ) ) )))))).
fof(conj_thm_2Ebitstring_2Eword__reduce__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(bool,arr(bool,bool))) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(ap(c_2Ewords_2Eword__reduce(A_27a),V0f),ap(c_2Ebitstring_2Ev2w(A_27a),V1v)) = ap(ap(c_2Ebool_2ELET(ty_2Elist_2Elist(bool),ty_2Efcp_2Ecart(bool,ty_2Eone_2Eone)),f2307(V0f)),ap(ap(c_2Ebitstring_2Efixwidth,ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a))),V1v)) ) ) )))).
fof(conj_thm_2Ebitstring_2Ereduce__and__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Ereduce__and(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(ap(c_2Ewords_2Eword__reduce(A_27a),c_2Ebool_2E_2F_5C),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) ) )))).
fof(conj_thm_2Ebitstring_2Ereduce__or__v2w,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Ereduce__or(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) = ap(ap(c_2Ewords_2Eword__reduce(A_27a),c_2Ebool_2E_5C_2F),ap(c_2Ebitstring_2Ev2w(A_27a),V0v)) ) )))).
fof(conj_thm_2Ebitstring_2Eextract__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Enum_2Enum) => ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(bool),V2v)),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(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0h)),V1l) ) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Efcp_2Edimindex(A_27b),c_2Ebool_2Ethe__value(A_27b))),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))) ) ) => ( ap(ap(ap(c_2Ewords_2Eword__extract(A_27a,A_27b),V0h),V1l),ap(c_2Ebitstring_2Ev2w(A_27a),V2v)) = ap(c_2Ebitstring_2Ev2w(A_27b),ap(ap(ap(c_2Ebitstring_2Efield,V0h),V1l),V2v)) ) ) ) ) ))))).
fof(conj_thm_2Ebitstring_2Eword__bit__last__shiftr,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0i),ap(c_2Efcp_2Edimindex(A_27a),c_2Ebool_2Ethe__value(A_27a)))) => ( p(ap(ap(c_2Ewords_2Eword__bit(A_27a),V0i),ap(c_2Ebitstring_2Ev2w(A_27a),V1v))) <=> p(ap(ap(c_2Ebool_2ELET(ty_2Elist_2Elist(bool),bool),f2308),ap(ap(c_2Ebitstring_2Eshiftr,V1v),V0i))) ) ) ) )))).
fof(conj_thm_2Ebitstring_2Eops__to__v2w,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) =>  ! [A_27e]: ( ne(A_27e) =>  ! [A_27f]: ( ne(A_27f) =>  ! [A_27g]: ( ne(A_27g) =>  ! [A_27h]: ( ne(A_27h) =>  ! [A_27i]: ( ne(A_27i) =>  ! [A_27j]: ( ne(A_27j) =>  ! [A_27k]: ( ne(A_27k) =>  ! [A_27l]: ( ne(A_27l) =>  ! [A_27m]: ( ne(A_27m) =>  ! [A_27n]: ( ne(A_27n) =>  ! [A_27o]: ( ne(A_27o) =>  ! [A_27p]: ( ne(A_27p) =>  ! [A_27q]: ( ne(A_27q) =>  ! [A_27r]: ( ne(A_27r) =>  ! [A_27s]: ( ne(A_27s) =>  ! [A_27t]: ( ne(A_27t) => ( ( ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__or(A_27c),ap(c_2Ebitstring_2Ev2w(A_27c),V0v)),ap(c_2Ewords_2En2w(A_27c),V1n)) = ap(ap(c_2Ewords_2Eword__or(A_27c),ap(c_2Ebitstring_2Ev2w(A_27c),V0v)),ap(c_2Ebitstring_2Ev2w(A_27c),ap(c_2Ebitstring_2En2v,V1n))) ) ) ) ) & ( ( ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__or(A_27d),ap(c_2Ewords_2En2w(A_27d),V3n)),ap(c_2Ebitstring_2Ev2w(A_27d),V2v)) = ap(ap(c_2Ewords_2Eword__or(A_27d),ap(c_2Ebitstring_2Ev2w(A_27d),ap(c_2Ebitstring_2En2v,V3n))),ap(c_2Ebitstring_2Ev2w(A_27d),V2v)) ) ) ) ) & ( ( ! [V4v] : ( mem(V4v,ty_2Elist_2Elist(bool)) => ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__and(A_27e),ap(c_2Ebitstring_2Ev2w(A_27e),V4v)),ap(c_2Ewords_2En2w(A_27e),V5n)) = ap(ap(c_2Ewords_2Eword__and(A_27e),ap(c_2Ebitstring_2Ev2w(A_27e),V4v)),ap(c_2Ebitstring_2Ev2w(A_27e),ap(c_2Ebitstring_2En2v,V5n))) ) ) ) ) & ( ( ! [V6v] : ( mem(V6v,ty_2Elist_2Elist(bool)) => ! [V7n] : ( mem(V7n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__and(A_27f),ap(c_2Ewords_2En2w(A_27f),V7n)),ap(c_2Ebitstring_2Ev2w(A_27f),V6v)) = ap(ap(c_2Ewords_2Eword__and(A_27f),ap(c_2Ebitstring_2Ev2w(A_27f),ap(c_2Ebitstring_2En2v,V7n))),ap(c_2Ebitstring_2Ev2w(A_27f),V6v)) ) ) ) ) & ( ( ! [V8v] : ( mem(V8v,ty_2Elist_2Elist(bool)) => ! [V9n] : ( mem(V9n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__xor(A_27g),ap(c_2Ebitstring_2Ev2w(A_27g),V8v)),ap(c_2Ewords_2En2w(A_27g),V9n)) = ap(ap(c_2Ewords_2Eword__xor(A_27g),ap(c_2Ebitstring_2Ev2w(A_27g),V8v)),ap(c_2Ebitstring_2Ev2w(A_27g),ap(c_2Ebitstring_2En2v,V9n))) ) ) ) ) & ( ( ! [V10v] : ( mem(V10v,ty_2Elist_2Elist(bool)) => ! [V11n] : ( mem(V11n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__xor(A_27h),ap(c_2Ewords_2En2w(A_27h),V11n)),ap(c_2Ebitstring_2Ev2w(A_27h),V10v)) = ap(ap(c_2Ewords_2Eword__xor(A_27h),ap(c_2Ebitstring_2Ev2w(A_27h),ap(c_2Ebitstring_2En2v,V11n))),ap(c_2Ebitstring_2Ev2w(A_27h),V10v)) ) ) ) ) & ( ( ! [V12v] : ( mem(V12v,ty_2Elist_2Elist(bool)) => ! [V13n] : ( mem(V13n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__nor(A_27i),ap(c_2Ebitstring_2Ev2w(A_27i),V12v)),ap(c_2Ewords_2En2w(A_27i),V13n)) = ap(ap(c_2Ewords_2Eword__nor(A_27i),ap(c_2Ebitstring_2Ev2w(A_27i),V12v)),ap(c_2Ebitstring_2Ev2w(A_27i),ap(c_2Ebitstring_2En2v,V13n))) ) ) ) ) & ( ( ! [V14v] : ( mem(V14v,ty_2Elist_2Elist(bool)) => ! [V15n] : ( mem(V15n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__nor(A_27j),ap(c_2Ewords_2En2w(A_27j),V15n)),ap(c_2Ebitstring_2Ev2w(A_27j),V14v)) = ap(ap(c_2Ewords_2Eword__nor(A_27j),ap(c_2Ebitstring_2Ev2w(A_27j),ap(c_2Ebitstring_2En2v,V15n))),ap(c_2Ebitstring_2Ev2w(A_27j),V14v)) ) ) ) ) & ( ( ! [V16v] : ( mem(V16v,ty_2Elist_2Elist(bool)) => ! [V17n] : ( mem(V17n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__nand(A_27k),ap(c_2Ebitstring_2Ev2w(A_27k),V16v)),ap(c_2Ewords_2En2w(A_27k),V17n)) = ap(ap(c_2Ewords_2Eword__nand(A_27k),ap(c_2Ebitstring_2Ev2w(A_27k),V16v)),ap(c_2Ebitstring_2Ev2w(A_27k),ap(c_2Ebitstring_2En2v,V17n))) ) ) ) ) & ( ( ! [V18v] : ( mem(V18v,ty_2Elist_2Elist(bool)) => ! [V19n] : ( mem(V19n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__nand(A_27l),ap(c_2Ewords_2En2w(A_27l),V19n)),ap(c_2Ebitstring_2Ev2w(A_27l),V18v)) = ap(ap(c_2Ewords_2Eword__nand(A_27l),ap(c_2Ebitstring_2Ev2w(A_27l),ap(c_2Ebitstring_2En2v,V19n))),ap(c_2Ebitstring_2Ev2w(A_27l),V18v)) ) ) ) ) & ( ( ! [V20v] : ( mem(V20v,ty_2Elist_2Elist(bool)) => ! [V21n] : ( mem(V21n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__xnor(A_27m),ap(c_2Ebitstring_2Ev2w(A_27m),V20v)),ap(c_2Ewords_2En2w(A_27m),V21n)) = ap(ap(c_2Ewords_2Eword__xnor(A_27m),ap(c_2Ebitstring_2Ev2w(A_27m),V20v)),ap(c_2Ebitstring_2Ev2w(A_27m),ap(c_2Ebitstring_2En2v,V21n))) ) ) ) ) & ( ( ! [V22v] : ( mem(V22v,ty_2Elist_2Elist(bool)) => ! [V23n] : ( mem(V23n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__xnor(A_27n),ap(c_2Ewords_2En2w(A_27n),V23n)),ap(c_2Ebitstring_2Ev2w(A_27n),V22v)) = ap(ap(c_2Ewords_2Eword__xnor(A_27n),ap(c_2Ebitstring_2Ev2w(A_27n),ap(c_2Ebitstring_2En2v,V23n))),ap(c_2Ebitstring_2Ev2w(A_27n),V22v)) ) ) ) ) & ( ( ! [V24v] : ( mem(V24v,ty_2Elist_2Elist(bool)) => ! [V25n] : ( mem(V25n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27o),ap(c_2Ebitstring_2Ev2w(A_27a),V24v)),ap(c_2Ewords_2En2w(A_27b),V25n)) = ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27o),ap(c_2Ebitstring_2Ev2w(A_27a),V24v)),ap(c_2Ebitstring_2Ev2w(A_27b),ap(c_2Ebitstring_2En2v,V25n))) ) ) ) ) & ( ( ! [V26v] : ( mem(V26v,ty_2Elist_2Elist(bool)) => ! [V27n] : ( mem(V27n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27p),ap(c_2Ewords_2En2w(A_27a),V27n)),ap(c_2Ebitstring_2Ev2w(A_27b),V26v)) = ap(ap(c_2Ewords_2Eword__concat(A_27a,A_27b,A_27p),ap(c_2Ebitstring_2Ev2w(A_27a),ap(c_2Ebitstring_2En2v,V27n))),ap(c_2Ebitstring_2Ev2w(A_27b),V26v)) ) ) ) ) & ( ( ! [V28v] : ( mem(V28v,ty_2Elist_2Elist(bool)) => ! [V29n] : ( mem(V29n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__join(A_27q,A_27r),ap(c_2Ebitstring_2Ev2w(A_27q),V28v)),ap(c_2Ewords_2En2w(A_27r),V29n)) = ap(ap(c_2Ewords_2Eword__join(A_27q,A_27r),ap(c_2Ebitstring_2Ev2w(A_27q),V28v)),ap(c_2Ebitstring_2Ev2w(A_27r),ap(c_2Ebitstring_2En2v,V29n))) ) ) ) ) & ! [V30v] : ( mem(V30v,ty_2Elist_2Elist(bool)) => ! [V31n] : ( mem(V31n,ty_2Enum_2Enum) => ( ap(ap(c_2Ewords_2Eword__join(A_27s,A_27t),ap(c_2Ewords_2En2w(A_27s),V31n)),ap(c_2Ebitstring_2Ev2w(A_27t),V30v)) = ap(ap(c_2Ewords_2Eword__join(A_27s,A_27t),ap(c_2Ebitstring_2Ev2w(A_27s),ap(c_2Ebitstring_2En2v,V31n))),ap(c_2Ebitstring_2Ev2w(A_27t),V30v)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))))))))))))))))))))))).
fof(conj_thm_2Ebitstring_2Eops__to__n2w,conjecture,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) =>  ! [A_27e]: ( ne(A_27e) =>  ! [A_27f]: ( ne(A_27f) =>  ! [A_27g]: ( ne(A_27g) =>  ! [A_27h]: ( ne(A_27h) =>  ! [A_27i]: ( ne(A_27i) =>  ! [A_27j]: ( ne(A_27j) =>  ! [A_27k]: ( ne(A_27k) =>  ! [A_27l]: ( ne(A_27l) =>  ! [A_27m]: ( ne(A_27m) =>  ! [A_27n]: ( ne(A_27n) =>  ! [A_27o]: ( ne(A_27o) => ( ( ! [V0v] : ( mem(V0v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Eword__2comp(A_27b),ap(c_2Ebitstring_2Ev2w(A_27b),V0v)) = ap(c_2Ewords_2Eword__2comp(A_27b),ap(c_2Ewords_2En2w(A_27b),ap(c_2Ebitstring_2Ev2n,V0v))) ) ) ) & ( ( ! [V1v] : ( mem(V1v,ty_2Elist_2Elist(bool)) => ( ap(c_2Ewords_2Eword__log2(A_27c),ap(c_2Ebitstring_2Ev2w(A_27c),V1v)) = ap(c_2Ewords_2Eword__log2(A_27c),ap(c_2Ewords_2En2w(A_27c),ap(c_2Ebitstring_2Ev2n,V1v))) ) ) ) & ( ( ! [V2v] : ( mem(V2v,ty_2Elist_2Elist(bool)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ( ap(c_2Ebitstring_2Ev2w(A_27a),V2v) = ap(c_2Ewords_2En2w(A_27a),V3n) ) <=> ( ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V2v)) = ap(c_2Ewords_2En2w(A_27a),V3n) ) ) ) ) ) & ( ( ! [V4v] : ( mem(V4v,ty_2Elist_2Elist(bool)) => ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ( ( ap(c_2Ewords_2En2w(A_27a),V5n) = ap(c_2Ebitstring_2Ev2w(A_27a),V4v) ) <=> ( ap(c_2Ewords_2En2w(A_27a),V5n) = ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V4v)) ) ) ) ) ) & ( ( ! [V6v] : ( mem(V6v,ty_2Elist_2Elist(bool)) => ! [V7w] : ( mem(V7w,ty_2Efcp_2Ecart(bool,A_27d)) => ( ap(ap(c_2Ewords_2Eword__add(A_27d),ap(c_2Ebitstring_2Ev2w(A_27d),V6v)),V7w) = ap(ap(c_2Ewords_2Eword__add(A_27d),ap(c_2Ewords_2En2w(A_27d),ap(c_2Ebitstring_2Ev2n,V6v))),V7w) ) ) ) ) & ( ( ! [V8v] : ( mem(V8v,ty_2Elist_2Elist(bool)) => ! [V9w] : ( mem(V9w,ty_2Efcp_2Ecart(bool,A_27e)) => ( ap(ap(c_2Ewords_2Eword__add(A_27e),V9w),ap(c_2Ebitstring_2Ev2w(A_27e),V8v)) = ap(ap(c_2Ewords_2Eword__add(A_27e),V9w),ap(c_2Ewords_2En2w(A_27e),ap(c_2Ebitstring_2Ev2n,V8v))) ) ) ) ) & ( ( ! [V10v] : ( mem(V10v,ty_2Elist_2Elist(bool)) => ! [V11w] : ( mem(V11w,ty_2Efcp_2Ecart(bool,A_27f)) => ( ap(ap(c_2Ewords_2Eword__sub(A_27f),ap(c_2Ebitstring_2Ev2w(A_27f),V10v)),V11w) = ap(ap(c_2Ewords_2Eword__sub(A_27f),ap(c_2Ewords_2En2w(A_27f),ap(c_2Ebitstring_2Ev2n,V10v))),V11w) ) ) ) ) & ( ( ! [V12v] : ( mem(V12v,ty_2Elist_2Elist(bool)) => ! [V13w] : ( mem(V13w,ty_2Efcp_2Ecart(bool,A_27g)) => ( ap(ap(c_2Ewords_2Eword__sub(A_27g),V13w),ap(c_2Ebitstring_2Ev2w(A_27g),V12v)) = ap(ap(c_2Ewords_2Eword__sub(A_27g),V13w),ap(c_2Ewords_2En2w(A_27g),ap(c_2Ebitstring_2Ev2n,V12v))) ) ) ) ) & ( ( ! [V14v] : ( mem(V14v,ty_2Elist_2Elist(bool)) => ! [V15w] : ( mem(V15w,ty_2Efcp_2Ecart(bool,A_27h)) => ( ap(ap(c_2Ewords_2Eword__mul(A_27h),ap(c_2Ebitstring_2Ev2w(A_27h),V14v)),V15w) = ap(ap(c_2Ewords_2Eword__mul(A_27h),ap(c_2Ewords_2En2w(A_27h),ap(c_2Ebitstring_2Ev2n,V14v))),V15w) ) ) ) ) & ( ( ! [V16v] : ( mem(V16v,ty_2Elist_2Elist(bool)) => ! [V17w] : ( mem(V17w,ty_2Efcp_2Ecart(bool,A_27i)) => ( ap(ap(c_2Ewords_2Eword__mul(A_27i),V17w),ap(c_2Ebitstring_2Ev2w(A_27i),V16v)) = ap(ap(c_2Ewords_2Eword__mul(A_27i),V17w),ap(c_2Ewords_2En2w(A_27i),ap(c_2Ebitstring_2Ev2n,V16v))) ) ) ) ) & ( ( ! [V18v] : ( mem(V18v,ty_2Elist_2Elist(bool)) => ! [V19w] : ( mem(V19w,ty_2Efcp_2Ecart(bool,A_27j)) => ( ap(ap(c_2Ewords_2Eword__quot(A_27j),ap(c_2Ebitstring_2Ev2w(A_27j),V18v)),V19w) = ap(ap(c_2Ewords_2Eword__quot(A_27j),ap(c_2Ewords_2En2w(A_27j),ap(c_2Ebitstring_2Ev2n,V18v))),V19w) ) ) ) ) & ( ( ! [V20v] : ( mem(V20v,ty_2Elist_2Elist(bool)) => ! [V21w] : ( mem(V21w,ty_2Efcp_2Ecart(bool,A_27k)) => ( ap(ap(c_2Ewords_2Eword__quot(A_27k),V21w),ap(c_2Ebitstring_2Ev2w(A_27k),V20v)) = ap(ap(c_2Ewords_2Eword__quot(A_27k),V21w),ap(c_2Ewords_2En2w(A_27k),ap(c_2Ebitstring_2Ev2n,V20v))) ) ) ) ) & ( ( ! [V22v] : ( mem(V22v,ty_2Elist_2Elist(bool)) => ! [V23w] : ( mem(V23w,ty_2Efcp_2Ecart(bool,A_27l)) => ( ap(ap(c_2Ewords_2Eword__div(A_27l),ap(c_2Ebitstring_2Ev2w(A_27l),V22v)),V23w) = ap(ap(c_2Ewords_2Eword__div(A_27l),ap(c_2Ewords_2En2w(A_27l),ap(c_2Ebitstring_2Ev2n,V22v))),V23w) ) ) ) ) & ( ( ! [V24v] : ( mem(V24v,ty_2Elist_2Elist(bool)) => ! [V25w] : ( mem(V25w,ty_2Efcp_2Ecart(bool,A_27m)) => ( ap(ap(c_2Ewords_2Eword__div(A_27m),V25w),ap(c_2Ebitstring_2Ev2w(A_27m),V24v)) = ap(ap(c_2Ewords_2Eword__div(A_27m),V25w),ap(c_2Ewords_2En2w(A_27m),ap(c_2Ebitstring_2Ev2n,V24v))) ) ) ) ) & ( ( ! [V26v] : ( mem(V26v,ty_2Elist_2Elist(bool)) => ! [V27w] : ( mem(V27w,ty_2Efcp_2Ecart(bool,A_27n)) => ( ap(ap(c_2Ewords_2Eword__mod(A_27n),ap(c_2Ebitstring_2Ev2w(A_27n),V26v)),V27w) = ap(ap(c_2Ewords_2Eword__mod(A_27n),ap(c_2Ewords_2En2w(A_27n),ap(c_2Ebitstring_2Ev2n,V26v))),V27w) ) ) ) ) & ( ( ! [V28v] : ( mem(V28v,ty_2Elist_2Elist(bool)) => ! [V29w] : ( mem(V29w,ty_2Efcp_2Ecart(bool,A_27o)) => ( ap(ap(c_2Ewords_2Eword__mod(A_27o),V29w),ap(c_2Ebitstring_2Ev2w(A_27o),V28v)) = ap(ap(c_2Ewords_2Eword__mod(A_27o),V29w),ap(c_2Ewords_2En2w(A_27o),ap(c_2Ebitstring_2Ev2n,V28v))) ) ) ) ) & ( ( ! [V30v] : ( mem(V30v,ty_2Elist_2Elist(bool)) => ! [V31w] : ( mem(V31w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__lt(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V30v)),V31w)) <=> p(ap(ap(c_2Ewords_2Eword__lt(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V30v))),V31w)) ) ) ) ) & ( ( ! [V32v] : ( mem(V32v,ty_2Elist_2Elist(bool)) => ! [V33w] : ( mem(V33w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__lt(A_27a),V33w),ap(c_2Ebitstring_2Ev2w(A_27a),V32v))) <=> p(ap(ap(c_2Ewords_2Eword__lt(A_27a),V33w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V32v)))) ) ) ) ) & ( ( ! [V34v] : ( mem(V34v,ty_2Elist_2Elist(bool)) => ! [V35w] : ( mem(V35w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__gt(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V34v)),V35w)) <=> p(ap(ap(c_2Ewords_2Eword__gt(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V34v))),V35w)) ) ) ) ) & ( ( ! [V36v] : ( mem(V36v,ty_2Elist_2Elist(bool)) => ! [V37w] : ( mem(V37w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__gt(A_27a),V37w),ap(c_2Ebitstring_2Ev2w(A_27a),V36v))) <=> p(ap(ap(c_2Ewords_2Eword__gt(A_27a),V37w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V36v)))) ) ) ) ) & ( ( ! [V38v] : ( mem(V38v,ty_2Elist_2Elist(bool)) => ! [V39w] : ( mem(V39w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__le(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V38v)),V39w)) <=> p(ap(ap(c_2Ewords_2Eword__le(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V38v))),V39w)) ) ) ) ) & ( ( ! [V40v] : ( mem(V40v,ty_2Elist_2Elist(bool)) => ! [V41w] : ( mem(V41w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__le(A_27a),V41w),ap(c_2Ebitstring_2Ev2w(A_27a),V40v))) <=> p(ap(ap(c_2Ewords_2Eword__le(A_27a),V41w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V40v)))) ) ) ) ) & ( ( ! [V42v] : ( mem(V42v,ty_2Elist_2Elist(bool)) => ! [V43w] : ( mem(V43w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__ge(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V42v)),V43w)) <=> p(ap(ap(c_2Ewords_2Eword__ge(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V42v))),V43w)) ) ) ) ) & ( ( ! [V44v] : ( mem(V44v,ty_2Elist_2Elist(bool)) => ! [V45w] : ( mem(V45w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__ge(A_27a),V45w),ap(c_2Ebitstring_2Ev2w(A_27a),V44v))) <=> p(ap(ap(c_2Ewords_2Eword__ge(A_27a),V45w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V44v)))) ) ) ) ) & ( ( ! [V46v] : ( mem(V46v,ty_2Elist_2Elist(bool)) => ! [V47w] : ( mem(V47w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__lo(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V46v)),V47w)) <=> p(ap(ap(c_2Ewords_2Eword__lo(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V46v))),V47w)) ) ) ) ) & ( ( ! [V48v] : ( mem(V48v,ty_2Elist_2Elist(bool)) => ! [V49w] : ( mem(V49w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__lo(A_27a),V49w),ap(c_2Ebitstring_2Ev2w(A_27a),V48v))) <=> p(ap(ap(c_2Ewords_2Eword__lo(A_27a),V49w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V48v)))) ) ) ) ) & ( ( ! [V50v] : ( mem(V50v,ty_2Elist_2Elist(bool)) => ! [V51w] : ( mem(V51w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__hi(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V50v)),V51w)) <=> p(ap(ap(c_2Ewords_2Eword__hi(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V50v))),V51w)) ) ) ) ) & ( ( ! [V52v] : ( mem(V52v,ty_2Elist_2Elist(bool)) => ! [V53w] : ( mem(V53w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__hi(A_27a),V53w),ap(c_2Ebitstring_2Ev2w(A_27a),V52v))) <=> p(ap(ap(c_2Ewords_2Eword__hi(A_27a),V53w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V52v)))) ) ) ) ) & ( ( ! [V54v] : ( mem(V54v,ty_2Elist_2Elist(bool)) => ! [V55w] : ( mem(V55w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__ls(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V54v)),V55w)) <=> p(ap(ap(c_2Ewords_2Eword__ls(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V54v))),V55w)) ) ) ) ) & ( ( ! [V56v] : ( mem(V56v,ty_2Elist_2Elist(bool)) => ! [V57w] : ( mem(V57w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__ls(A_27a),V57w),ap(c_2Ebitstring_2Ev2w(A_27a),V56v))) <=> p(ap(ap(c_2Ewords_2Eword__ls(A_27a),V57w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V56v)))) ) ) ) ) & ( ( ! [V58v] : ( mem(V58v,ty_2Elist_2Elist(bool)) => ! [V59w] : ( mem(V59w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__hs(A_27a),ap(c_2Ebitstring_2Ev2w(A_27a),V58v)),V59w)) <=> p(ap(ap(c_2Ewords_2Eword__hs(A_27a),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V58v))),V59w)) ) ) ) ) & ! [V60v] : ( mem(V60v,ty_2Elist_2Elist(bool)) => ! [V61w] : ( mem(V61w,ty_2Efcp_2Ecart(bool,A_27a)) => ( p(ap(ap(c_2Ewords_2Eword__hs(A_27a),V61w),ap(c_2Ebitstring_2Ev2w(A_27a),V60v))) <=> p(ap(ap(c_2Ewords_2Eword__hs(A_27a),V61w),ap(c_2Ewords_2En2w(A_27a),ap(c_2Ebitstring_2Ev2n,V60v)))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))))))))))))))))).
