include('Axioms/cardinal^2.ax').
thf(tp_c_2EASCIInumbers_2EHEX,type,(c_2EASCIInumbers_2EHEX:$i)).
thf(mem_c_2EASCIInumbers_2EHEX,axiom,(mem@c_2EASCIInumbers_2EHEX@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar))).
thf(stp_fo_c_2EASCIInumbers_2EHEX,type,(fo__c_2EASCIInumbers_2EHEX:(tp__ty_2Enum_2Enum > tp__ty_2Estring_2Echar))).
thf(stp_eq_fo_c_2EASCIInumbers_2EHEX,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Estring_2Echar @ (fo__c_2EASCIInumbers_2EHEX @ X0)) = (ap @ c_2EASCIInumbers_2EHEX @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2EASCIInumbers_2EUNHEX,type,(c_2EASCIInumbers_2EUNHEX:$i)).
thf(mem_c_2EASCIInumbers_2EUNHEX,axiom,(mem@c_2EASCIInumbers_2EUNHEX@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum))).
thf(stp_fo_c_2EASCIInumbers_2EUNHEX,type,(fo__c_2EASCIInumbers_2EUNHEX:(tp__ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EASCIInumbers_2EUNHEX,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2EASCIInumbers_2EUNHEX @ X0)) = (ap @ c_2EASCIInumbers_2EUNHEX @ (inj__ty_2Estring_2Echar @ X0))))).
thf(tp_c_2EASCIInumbers_2EfromBinString,type,(c_2EASCIInumbers_2EfromBinString:$i)).
thf(mem_c_2EASCIInumbers_2EfromBinString,axiom,(mem@c_2EASCIInumbers_2EfromBinString@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@(ty_2Eoption_2Eoption@ty_2Enum_2Enum)))).
thf(tp_c_2EASCIInumbers_2EfromDecString,type,(c_2EASCIInumbers_2EfromDecString:$i)).
thf(mem_c_2EASCIInumbers_2EfromDecString,axiom,(mem@c_2EASCIInumbers_2EfromDecString@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@(ty_2Eoption_2Eoption@ty_2Enum_2Enum)))).
thf(tp_c_2EASCIInumbers_2EfromHexString,type,(c_2EASCIInumbers_2EfromHexString:$i)).
thf(mem_c_2EASCIInumbers_2EfromHexString,axiom,(mem@c_2EASCIInumbers_2EfromHexString@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@(ty_2Eoption_2Eoption@ty_2Enum_2Enum)))).
thf(tp_c_2EASCIInumbers_2En2s,type,(c_2EASCIInumbers_2En2s:$i)).
thf(mem_c_2EASCIInumbers_2En2s,axiom,(mem@c_2EASCIInumbers_2En2s@(arr@ty_2Enum_2Enum@(arr@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))))).
thf(tp_c_2EASCIInumbers_2Enum__from__bin__string,type,(c_2EASCIInumbers_2Enum__from__bin__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__from__bin__string,axiom,(mem@c_2EASCIInumbers_2Enum__from__bin__string@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))).
thf(stp_fo_c_2EASCIInumbers_2Enum__from__bin__string,type,(fo__c_2EASCIInumbers_2Enum__from__bin__string:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EASCIInumbers_2Enum__from__bin__string,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2EASCIInumbers_2Enum__from__bin__string @ X0)) = (ap @ c_2EASCIInumbers_2Enum__from__bin__string @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X0))))).
thf(tp_c_2EASCIInumbers_2Enum__from__dec__string,type,(c_2EASCIInumbers_2Enum__from__dec__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__from__dec__string,axiom,(mem@c_2EASCIInumbers_2Enum__from__dec__string@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))).
thf(stp_fo_c_2EASCIInumbers_2Enum__from__dec__string,type,(fo__c_2EASCIInumbers_2Enum__from__dec__string:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EASCIInumbers_2Enum__from__dec__string,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2EASCIInumbers_2Enum__from__dec__string @ X0)) = (ap @ c_2EASCIInumbers_2Enum__from__dec__string @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X0))))).
thf(tp_c_2EASCIInumbers_2Enum__from__hex__string,type,(c_2EASCIInumbers_2Enum__from__hex__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__from__hex__string,axiom,(mem@c_2EASCIInumbers_2Enum__from__hex__string@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))).
thf(stp_fo_c_2EASCIInumbers_2Enum__from__hex__string,type,(fo__c_2EASCIInumbers_2Enum__from__hex__string:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EASCIInumbers_2Enum__from__hex__string,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2EASCIInumbers_2Enum__from__hex__string @ X0)) = (ap @ c_2EASCIInumbers_2Enum__from__hex__string @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X0))))).
thf(tp_c_2EASCIInumbers_2Enum__from__oct__string,type,(c_2EASCIInumbers_2Enum__from__oct__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__from__oct__string,axiom,(mem@c_2EASCIInumbers_2Enum__from__oct__string@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))).
thf(stp_fo_c_2EASCIInumbers_2Enum__from__oct__string,type,(fo__c_2EASCIInumbers_2Enum__from__oct__string:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EASCIInumbers_2Enum__from__oct__string,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2EASCIInumbers_2Enum__from__oct__string @ X0)) = (ap @ c_2EASCIInumbers_2Enum__from__oct__string @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X0))))).
thf(tp_c_2EASCIInumbers_2Enum__to__bin__string,type,(c_2EASCIInumbers_2Enum__to__bin__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__to__bin__string,axiom,(mem@c_2EASCIInumbers_2Enum__to__bin__string@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2EASCIInumbers_2Enum__to__dec__string,type,(c_2EASCIInumbers_2Enum__to__dec__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__to__dec__string,axiom,(mem@c_2EASCIInumbers_2Enum__to__dec__string@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2EASCIInumbers_2Enum__to__hex__string,type,(c_2EASCIInumbers_2Enum__to__hex__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__to__hex__string,axiom,(mem@c_2EASCIInumbers_2Enum__to__hex__string@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2EASCIInumbers_2Enum__to__oct__string,type,(c_2EASCIInumbers_2Enum__to__oct__string:$i)).
thf(mem_c_2EASCIInumbers_2Enum__to__oct__string,axiom,(mem@c_2EASCIInumbers_2Enum__to__oct__string@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2EASCIInumbers_2Es2n,type,(c_2EASCIInumbers_2Es2n:$i)).
thf(mem_c_2EASCIInumbers_2Es2n,axiom,(mem@c_2EASCIInumbers_2Es2n@(arr@ty_2Enum_2Enum@(arr@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))))).
thf(ax_thm_2EASCIInumbers_2Es2n__def,axiom,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)) => ( ! [V2s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V0b))@V1f)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(inj__ty_2Enum_2Enum @ V0b))@(ap@(ap@(c_2Elist_2EMAP@ty_2Estring_2Echar@ty_2Enum_2Enum)@V1f)@(ap@(c_2Elist_2EREVERSE@ty_2Estring_2Echar)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))))))))))).
thf(ax_thm_2EASCIInumbers_2En2s__def,axiom,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(ap@c_2EASCIInumbers_2En2s@(inj__ty_2Enum_2Enum @ V0b))@V1f)@(inj__ty_2Enum_2Enum @ V2n))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(c_2Elist_2EREVERSE@ty_2Estring_2Echar)@(ap@(ap@(c_2Elist_2EMAP@ty_2Enum_2Enum@ty_2Estring_2Echar)@V1f)@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2n))))))))))).
thf(ax_thm_2EASCIInumbers_2EHEX__primitive__def,axiom,(c_2EASCIInumbers_2EHEX = (ap@(ap@(c_2Erelation_2EWFREC@ty_2Enum_2Enum@ty_2Estring_2Echar)@(ap@(c_2Emin_2E_40@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@(lam@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))@(^ [V0R:$i] : (ap@(c_2Erelation_2EWF@ty_2Enum_2Enum)@V0R)))))@(lam@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)@(^ [V1HEX:$i] : (lam@ty_2Enum_2Enum@(^ [V2a:$i] : (ap@(ap@(c_2Ebool_2Eliteral__case@ty_2Enum_2Enum@ty_2Estring_2Echar)@(lam@ty_2Enum_2Enum@(^ [V3v:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Estring_2Echar)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3v)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(ap@(c_2Ecombin_2EI@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(c_2Ebool_2EARB@ty_2Estring_2Echar))))))))))))))))))))@V2a)))))))).
thf(conj_thm_2EASCIInumbers_2EHEX__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => (((p@(ap@V0P@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((p@(ap@V0P@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ( ! [V1v18:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V1v18)))))))))))))))))))) => ( ! [V2v:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V2v)))))))).
thf(conj_thm_2EASCIInumbers_2EHEX__def,lemma,(((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & (((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))))))))))))))).
thf(ax_thm_2EASCIInumbers_2EUNHEX__primitive__def,axiom,(c_2EASCIInumbers_2EUNHEX = (ap@(ap@(c_2Erelation_2EWFREC@ty_2Estring_2Echar@ty_2Enum_2Enum)@(ap@(c_2Emin_2E_40@(arr@ty_2Estring_2Echar@(arr@ty_2Estring_2Echar@bool)))@(lam@(arr@ty_2Estring_2Echar@(arr@ty_2Estring_2Echar@bool))@(^ [V0R:$i] : (ap@(c_2Erelation_2EWF@ty_2Estring_2Echar)@V0R)))))@(lam@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)@(^ [V1UNHEX:$i] : (lam@ty_2Estring_2Echar@(^ [V2a:$i] : (ap@(ap@(c_2Ebool_2Eliteral__case@ty_2Estring_2Echar@ty_2Enum_2Enum)@(lam@ty_2Estring_2Echar@(^ [V3v:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V3v)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(c_2Ecombin_2EI@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(c_2Ebool_2EARB@ty_2Enum_2Enum))))))))))))))))))))))))))@V2a)))))))).
thf(conj_thm_2EASCIInumbers_2EUNHEX__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Estring_2Echar@bool)) => (((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ((p@(ap@V0P@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) & ( ! [V1v24:tp__ty_2Estring_2Echar] : (p@(ap@V0P@(inj__ty_2Estring_2Echar @ V1v24)))))))))))))))))))))))))) => ( ! [V2v:tp__ty_2Estring_2Echar] : (p@(ap@V0P@(inj__ty_2Estring_2Echar @ V2v)))))))).
thf(conj_thm_2EASCIInumbers_2EUNHEX__def,lemma,(((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = fo__c_2Enum_2E0) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) & ((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))))))))))))))))))).
thf(ax_thm_2EASCIInumbers_2Enum__from__bin__string__def,axiom,(c_2EASCIInumbers_2Enum__from__bin__string = (ap@(ap@c_2EASCIInumbers_2Es2n@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2EASCIInumbers_2EUNHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__from__oct__string__def,axiom,(c_2EASCIInumbers_2Enum__from__oct__string = (ap@(ap@c_2EASCIInumbers_2Es2n@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@c_2EASCIInumbers_2EUNHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__from__dec__string__def,axiom,(c_2EASCIInumbers_2Enum__from__dec__string = (ap@(ap@c_2EASCIInumbers_2Es2n@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@c_2EASCIInumbers_2EUNHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__from__hex__string__def,axiom,(c_2EASCIInumbers_2Enum__from__hex__string = (ap@(ap@c_2EASCIInumbers_2Es2n@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@c_2EASCIInumbers_2EUNHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__to__bin__string__def,axiom,(c_2EASCIInumbers_2Enum__to__bin__string = (ap@(ap@c_2EASCIInumbers_2En2s@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@c_2EASCIInumbers_2EHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__to__oct__string__def,axiom,(c_2EASCIInumbers_2Enum__to__oct__string = (ap@(ap@c_2EASCIInumbers_2En2s@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@c_2EASCIInumbers_2EHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__to__dec__string__def,axiom,(c_2EASCIInumbers_2Enum__to__dec__string = (ap@(ap@c_2EASCIInumbers_2En2s@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@c_2EASCIInumbers_2EHEX))).
thf(ax_thm_2EASCIInumbers_2Enum__to__hex__string__def,axiom,(c_2EASCIInumbers_2Enum__to__hex__string = (ap@(ap@c_2EASCIInumbers_2En2s@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@c_2EASCIInumbers_2EHEX))).
thf(ax_thm_2EASCIInumbers_2EfromBinString__def,axiom,( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EfromBinString@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@ty_2Enum_2Enum))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Estring_2Echar))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))@(c_2Elist_2ENIL@ty_2Estring_2Echar))))@(ap@(ap@(c_2Elist_2EEVERY@ty_2Estring_2Echar)@(lam@ty_2Estring_2Echar@(^ [V1c:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V1c)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@(ap@(c_2Emin_2E_3D@ty_2Estring_2Echar)@V1c)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))@(ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@c_2EASCIInumbers_2Enum__from__bin__string@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))@(c_2Eoption_2ENONE@ty_2Enum_2Enum)))))).
thf(ax_thm_2EASCIInumbers_2EfromDecString__def,axiom,( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EfromDecString@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@ty_2Enum_2Enum))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Estring_2Echar))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))@(c_2Elist_2ENIL@ty_2Estring_2Echar))))@(ap@(ap@(c_2Elist_2EEVERY@ty_2Estring_2Echar)@c_2Estring_2EisDigit)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))@(ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@c_2EASCIInumbers_2Enum__from__dec__string@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))@(c_2Eoption_2ENONE@ty_2Enum_2Enum)))))).
thf(ax_thm_2EASCIInumbers_2EfromHexString__def,axiom,( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EfromHexString@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@ty_2Enum_2Enum))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Estring_2Echar))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))@(c_2Elist_2ENIL@ty_2Estring_2Echar))))@(ap@(ap@(c_2Elist_2EEVERY@ty_2Estring_2Echar)@c_2Estring_2EisHexDigit)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))@(ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@c_2EASCIInumbers_2Enum__from__hex__string@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))@(c_2Eoption_2ENONE@ty_2Enum_2Enum)))))).
thf(conj_thm_2EASCIInumbers_2Es2n__compute,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)) => ( ! [V2s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V0b))@V1f)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(inj__ty_2Enum_2Enum @ V0b))@(ap@(ap@(c_2Elist_2EMAP@ty_2Estring_2Echar@ty_2Enum_2Enum)@V1f)@(ap@(c_2Elist_2EREVERSE@ty_2Estring_2Echar)@(ap@c_2Estring_2EEXPLODE@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s)))))))))))).
thf(conj_thm_2EASCIInumbers_2En2s__compute,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(ap@c_2EASCIInumbers_2En2s@(inj__ty_2Enum_2Enum @ V0b))@V1f)@(inj__ty_2Enum_2Enum @ V2n))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2Estring_2EIMPLODE@(ap@(c_2Elist_2EREVERSE@ty_2Estring_2Echar)@(ap@(ap@(c_2Elist_2EMAP@ty_2Enum_2Enum@ty_2Estring_2Echar)@V1f)@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2n)))))))))))).
thf(conj_thm_2EASCIInumbers_2EUNHEX__HEX,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) => ((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2EASCIInumbers_2EHEX@(inj__ty_2Enum_2Enum @ V0n)))) = V0n)))).
thf(conj_thm_2EASCIInumbers_2EHEX__UNHEX,lemma,( ! [V0c:tp__ty_2Estring_2Echar] : ((p@(ap@c_2Estring_2EisHexDigit@(inj__ty_2Estring_2Echar @ V0c))) => ((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2EASCIInumbers_2EUNHEX@(inj__ty_2Estring_2Echar @ V0c)))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2EtoUpper@(inj__ty_2Estring_2Echar @ V0c))))))).
thf(conj_thm_2EASCIInumbers_2EDEC__UNDEC,lemma,( ! [V0c:tp__ty_2Estring_2Echar] : ((p@(ap@c_2Estring_2EisDigit@(inj__ty_2Estring_2Echar @ V0c))) => ((surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@c_2EASCIInumbers_2EUNHEX@(inj__ty_2Estring_2Echar @ V0c)))) = V0c)))).
thf(conj_thm_2EASCIInumbers_2Es2n__n2s,lemma,( ! [V0c2n:$i] : ((mem@V0c2n@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)) => ( ! [V1n2c:$i] : ((mem@V1n2c@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)) => ( ! [V2b:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2b))) & ( ! [V4x:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4x))@(inj__ty_2Enum_2Enum @ V2b))) => ((surj__ty_2Enum_2Enum @ (ap@V0c2n@(ap@V1n2c@(inj__ty_2Enum_2Enum @ V4x)))) = V4x)))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V2b))@V0c2n)@(ap@(ap@(ap@c_2EASCIInumbers_2En2s@(inj__ty_2Enum_2Enum @ V2b))@V1n2c)@(inj__ty_2Enum_2Enum @ V3n)))) = V3n))))))))).
thf(conj_thm_2EASCIInumbers_2En2s__s2n,lemma,( ! [V0c2n:$i] : ((mem@V0c2n@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)) => ( ! [V1n2c:$i] : ((mem@V1n2c@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)) => ( ! [V2b:tp__ty_2Enum_2Enum] : ( ! [V3s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2b))) & (p@(ap@(ap@(c_2Elist_2EEVERY@ty_2Estring_2Echar)@(ap@(ap@(c_2Ecombin_2Eo@ty_2Estring_2Echar@bool@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ V2b)))@V0c2n))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V3s)))) => ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(ap@c_2EASCIInumbers_2En2s@(inj__ty_2Enum_2Enum @ V2b))@V1n2c)@(ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V2b))@V0c2n)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V3s)))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Estring_2Echar))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V2b))@V0c2n)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V3s)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Estring_2Echar)@(ap@V1n2c@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(c_2Elist_2ENIL@ty_2Estring_2Echar)))@(ap@(ap@(c_2Elist_2EMAP@ty_2Estring_2Echar@ty_2Estring_2Echar)@(ap@(ap@(c_2Ecombin_2Eo@ty_2Estring_2Echar@ty_2Estring_2Echar@ty_2Enum_2Enum)@V1n2c)@V0c2n))@(ap@(ap@(c_2Erich__list_2ELASTN@ty_2Estring_2Echar)@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Elogroot_2ELOG@(inj__ty_2Enum_2Enum @ V2b))@(ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V2b))@V0c2n)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V3s)))))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V3s)))))))))))))).
thf(conj_thm_2EASCIInumbers_2EtoNum__toString,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2Enum__from__dec__string@(ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V0n)))) = V0n))).
thf(conj_thm_2EASCIInumbers_2EtoString__toNum__cancel,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2Enum__from__dec__string@(ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V0n)))) = V0n))).
thf(conj_thm_2EASCIInumbers_2EtoString__inj,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V0n))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m))))).
thf(conj_thm_2EASCIInumbers_2EtoString__11,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V0n))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m))))).
thf(conj_thm_2EASCIInumbers_2ESTRCAT__toString__inj,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(c_2Elist_2EAPPEND@ty_2Estring_2Echar)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))@(ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(c_2Elist_2EAPPEND@ty_2Estring_2Echar)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))@(ap@c_2EASCIInumbers_2Enum__to__dec__string@(inj__ty_2Enum_2Enum @ V1m))))) <=> (V0n = V1m)))))).
thf(conj_thm_2EASCIInumbers_2EBIT__num__from__bin__string,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (((p@(ap@(ap@(c_2Elist_2EEVERY@ty_2Estring_2Echar)@(ap@(ap@(c_2Ecombin_2Eo@ty_2Estring_2Echar@bool@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2E_3E@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@c_2EASCIInumbers_2EUNHEX))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V1s))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0x))@(ap@(c_2Elist_2ELENGTH@ty_2Estring_2Echar)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V1s))))) => ((p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V0x))@(ap@c_2EASCIInumbers_2Enum__from__bin__string@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V1s)))) <=> ((surj__ty_2Enum_2Enum @ (ap@c_2EASCIInumbers_2EUNHEX@(ap@c_2Estring_2ESUB@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V1s))@(ap@c_2Eprim__rec_2EPRE@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@ty_2Estring_2Echar)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V1s)))@(inj__ty_2Enum_2Enum @ V0x))))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2EASCIInumbers_2ESUB__num__to__bin__string,conjecture,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0x))@(ap@(c_2Elist_2ELENGTH@ty_2Estring_2Echar)@(ap@c_2EASCIInumbers_2Enum__to__bin__string@(inj__ty_2Enum_2Enum @ V1n))))) => ((surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ESUB@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum)@(ap@c_2EASCIInumbers_2Enum__to__bin__string@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V0x)))) = (surj__ty_2Estring_2Echar @ (ap@c_2EASCIInumbers_2EHEX@(ap@(ap@c_2Ebit_2EBITV@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Eprim__rec_2EPRE@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@ty_2Estring_2Echar)@(ap@c_2EASCIInumbers_2Enum__to__bin__string@(inj__ty_2Enum_2Enum @ V1n))))@(inj__ty_2Enum_2Enum @ V0x))))))))))).
