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