include('Axioms/HL4001^2.ax').
thf(tp_c_2Ebool_2EBOUNDED,type,(c_2Ebool_2EBOUNDED:$i)).
thf(mem_c_2Ebool_2EBOUNDED,axiom,(mem@c_2Ebool_2EBOUNDED@(arr@bool@bool))).
thf(tp_ty_2Einteger_2Eint,type,( ty_2Einteger_2Eint:del )).
thf(stp_ty_2Einteger_2Eint,type,(tp__ty_2Einteger_2Eint : $tType)).
thf(stp_inj_ty_2Einteger_2Eint,type,(inj__ty_2Einteger_2Eint : (tp__ty_2Einteger_2Eint > $i))).
thf(stp_surj_ty_2Einteger_2Eint,type,(surj__ty_2Einteger_2Eint : ($i > tp__ty_2Einteger_2Eint))).
thf(stp_inj_surj_ty_2Einteger_2Eint,axiom,( ! [X:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (inj__ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_ty_2Einteger_2Eint,axiom,( ! [X:tp__ty_2Einteger_2Eint] : (mem @ (inj__ty_2Einteger_2Eint @ X) @ ty_2Einteger_2Eint))).
thf(stp_iso_mem_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ ty_2Einteger_2Eint) => (X = (inj__ty_2Einteger_2Eint @ (surj__ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2EintExtension_2ESGN,type,(c_2EintExtension_2ESGN:$i)).
thf(mem_c_2EintExtension_2ESGN,axiom,(mem@c_2EintExtension_2ESGN@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint))).
thf(stp_fo_c_2EintExtension_2ESGN,type,(fo__c_2EintExtension_2ESGN:(tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2EintExtension_2ESGN,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ (fo__c_2EintExtension_2ESGN @ X0)) = (ap @ c_2EintExtension_2ESGN @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2Ebool_2E_3F,type,(c_2Ebool_2E_3F:(del>$i))).
thf(mem_c_2Ebool_2E_3F,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_3F@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_ex_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_3F@A)@Q)) <=> (? [X:$i] : ((mem@X@A) & (p@(ap@Q@X))))))))).
thf(tp_c_2Emarker_2EAbbrev,type,(c_2Emarker_2EAbbrev:$i)).
thf(mem_c_2Emarker_2EAbbrev,axiom,(mem@c_2Emarker_2EAbbrev@(arr@bool@bool))).
thf(tp_c_2Emarker_2ECong,type,(c_2Emarker_2ECong:$i)).
thf(mem_c_2Emarker_2ECong,axiom,(mem@c_2Emarker_2ECong@(arr@bool@bool))).
thf(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum:del )).
thf(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
thf(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : (tp__ty_2Enum_2Enum > $i))).
thf(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : ($i > tp__ty_2Enum_2Enum))).
thf(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem @ (inj__ty_2Enum_2Enum @ X) @ ty_2Enum_2Enum))).
thf(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ ty_2Enum_2Enum) => (X = (inj__ty_2Enum_2Enum @ (surj__ty_2Enum_2Enum @ X)))))).
thf(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
thf(mem_c_2Earithmetic_2EEVEN,axiom,(mem@c_2Earithmetic_2EEVEN@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
thf(mem_c_2Earithmetic_2EODD,axiom,(mem@c_2Earithmetic_2EODD@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
thf(mem_c_2Earithmetic_2E_3E_3D,axiom,(mem@c_2Earithmetic_2E_3E_3D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
thf(mem_c_2Earithmetic_2E_3E,axiom,(mem@c_2Earithmetic_2E_3E@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Eprim__rec_2EPRE,type,(c_2Eprim__rec_2EPRE:$i)).
thf(mem_c_2Eprim__rec_2EPRE,axiom,(mem@c_2Eprim__rec_2EPRE@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eprim__rec_2EPRE,type,(fo__c_2Eprim__rec_2EPRE:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eprim__rec_2EPRE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eprim__rec_2EPRE @ X0)) = (ap @ c_2Eprim__rec_2EPRE @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
thf(mem_c_2Earithmetic_2EEXP,axiom,(mem@c_2Earithmetic_2EEXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2EEXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2EEXP @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2EEXP @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
thf(mem_c_2Earithmetic_2E_2D,axiom,(mem@c_2Earithmetic_2E_2D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2E_2D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2E_2D @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2E_2D @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
thf(mem_c_2Earithmetic_2E_2A,axiom,(mem@c_2Earithmetic_2E_2A@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2E_2A,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2E_2A @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2E_2A @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Enumeral_2EiZ,type,(c_2Enumeral_2EiZ:$i)).
thf(mem_c_2Enumeral_2EiZ,axiom,(mem@c_2Enumeral_2EiZ@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiZ,type,(fo__c_2Enumeral_2EiZ:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enumeral_2EiZ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enumeral_2EiZ @ X0)) = (ap @ c_2Enumeral_2EiZ @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
thf(mem_c_2Earithmetic_2E_2B,axiom,(mem@c_2Earithmetic_2E_2B@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Earithmetic_2E_2B,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Earithmetic_2E_2B @ X0) @ X1)) = (ap @ (ap @ c_2Earithmetic_2E_2B @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
thf(mem_c_2Earithmetic_2EBIT2,axiom,(mem@c_2Earithmetic_2EBIT2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Earithmetic_2EBIT2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Earithmetic_2EBIT2 @ X0)) = (ap @ c_2Earithmetic_2EBIT2 @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
thf(mem_c_2Ebool_2ET,axiom,(mem@c_2Ebool_2ET@bool)).
thf(ax_true_p,axiom,(p@c_2Ebool_2ET)).
thf(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
thf(mem_c_2Earithmetic_2E_3C_3D,axiom,(mem@c_2Earithmetic_2E_3C_3D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_ty_2Efrac_2Efrac,type,( ty_2Efrac_2Efrac:del )).
thf(stp_ty_2Efrac_2Efrac,type,(tp__ty_2Efrac_2Efrac : $tType)).
thf(stp_inj_ty_2Efrac_2Efrac,type,(inj__ty_2Efrac_2Efrac : (tp__ty_2Efrac_2Efrac > $i))).
thf(stp_surj_ty_2Efrac_2Efrac,type,(surj__ty_2Efrac_2Efrac : ($i > tp__ty_2Efrac_2Efrac))).
thf(stp_inj_surj_ty_2Efrac_2Efrac,axiom,( ! [X:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Efrac_2Efrac @ (inj__ty_2Efrac_2Efrac @ X)) = X))).
thf(stp_inj_mem_ty_2Efrac_2Efrac,axiom,( ! [X:tp__ty_2Efrac_2Efrac] : (mem @ (inj__ty_2Efrac_2Efrac @ X) @ ty_2Efrac_2Efrac))).
thf(stp_iso_mem_ty_2Efrac_2Efrac,axiom,( ! [X:$i] : ((mem @ X @ ty_2Efrac_2Efrac) => (X = (inj__ty_2Efrac_2Efrac @ (surj__ty_2Efrac_2Efrac @ X)))))).
thf(tp_c_2Erat_2Erat__equiv,type,(c_2Erat_2Erat__equiv:$i)).
thf(mem_c_2Erat_2Erat__equiv,axiom,(mem@c_2Erat_2Erat__equiv@(arr@ty_2Efrac_2Efrac@(arr@ty_2Efrac_2Efrac@bool)))).
thf(tp_c_2Equotient_2EQUOTIENT,type,(c_2Equotient_2EQUOTIENT:(del>(del>$i)))).
thf(mem_c_2Equotient_2EQUOTIENT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Equotient_2EQUOTIENT@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27b@A_27a)@bool))))))).
thf(tp_c_2Efrac_2Efrac__0,type,(c_2Efrac_2Efrac__0:$i)).
thf(mem_c_2Efrac_2Efrac__0,axiom,(mem@c_2Efrac_2Efrac__0@ty_2Efrac_2Efrac)).
thf(stp_fo_c_2Efrac_2Efrac__0,type,(fo__c_2Efrac_2Efrac__0:tp__ty_2Efrac_2Efrac)).
thf(stp_eq_fo_c_2Efrac_2Efrac__0,axiom,((inj__ty_2Efrac_2Efrac @ fo__c_2Efrac_2Efrac__0) = c_2Efrac_2Efrac__0)).
thf(tp_c_2Efrac_2Efrac__sgn,type,(c_2Efrac_2Efrac__sgn:$i)).
thf(mem_c_2Efrac_2Efrac__sgn,axiom,(mem@c_2Efrac_2Efrac__sgn@(arr@ty_2Efrac_2Efrac@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Efrac_2Efrac__sgn,type,(fo__c_2Efrac_2Efrac__sgn:(tp__ty_2Efrac_2Efrac > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Efrac_2Efrac__sgn,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Efrac_2Efrac__sgn @ X0)) = (ap @ c_2Efrac_2Efrac__sgn @ (inj__ty_2Efrac_2Efrac @ X0))))).
thf(tp_ty_2Erat_2Erat,type,( ty_2Erat_2Erat:del )).
thf(stp_ty_2Erat_2Erat,type,(tp__ty_2Erat_2Erat : $tType)).
thf(stp_inj_ty_2Erat_2Erat,type,(inj__ty_2Erat_2Erat : (tp__ty_2Erat_2Erat > $i))).
thf(stp_surj_ty_2Erat_2Erat,type,(surj__ty_2Erat_2Erat : ($i > tp__ty_2Erat_2Erat))).
thf(stp_inj_surj_ty_2Erat_2Erat,axiom,( ! [X:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (inj__ty_2Erat_2Erat @ X)) = X))).
thf(stp_inj_mem_ty_2Erat_2Erat,axiom,( ! [X:tp__ty_2Erat_2Erat] : (mem @ (inj__ty_2Erat_2Erat @ X) @ ty_2Erat_2Erat))).
thf(stp_iso_mem_ty_2Erat_2Erat,axiom,( ! [X:$i] : ((mem @ X @ ty_2Erat_2Erat) => (X = (inj__ty_2Erat_2Erat @ (surj__ty_2Erat_2Erat @ X)))))).
thf(tp_c_2Erat_2Erep__rat,type,(c_2Erat_2Erep__rat:$i)).
thf(mem_c_2Erat_2Erep__rat,axiom,(mem@c_2Erat_2Erep__rat@(arr@ty_2Erat_2Erat@ty_2Efrac_2Efrac))).
thf(stp_fo_c_2Erat_2Erep__rat,type,(fo__c_2Erat_2Erep__rat:(tp__ty_2Erat_2Erat > tp__ty_2Efrac_2Efrac))).
thf(stp_eq_fo_c_2Erat_2Erep__rat,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ((inj__ty_2Efrac_2Efrac @ (fo__c_2Erat_2Erep__rat @ X0)) = (ap @ c_2Erat_2Erep__rat @ (inj__ty_2Erat_2Erat @ X0))))).
thf(tp_c_2Efrac_2Efrac__ainv,type,(c_2Efrac_2Efrac__ainv:$i)).
thf(mem_c_2Efrac_2Efrac__ainv,axiom,(mem@c_2Efrac_2Efrac__ainv@(arr@ty_2Efrac_2Efrac@ty_2Efrac_2Efrac))).
thf(stp_fo_c_2Efrac_2Efrac__ainv,type,(fo__c_2Efrac_2Efrac__ainv:(tp__ty_2Efrac_2Efrac > tp__ty_2Efrac_2Efrac))).
thf(stp_eq_fo_c_2Efrac_2Efrac__ainv,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : ((inj__ty_2Efrac_2Efrac @ (fo__c_2Efrac_2Efrac__ainv @ X0)) = (ap @ c_2Efrac_2Efrac__ainv @ (inj__ty_2Efrac_2Efrac @ X0))))).
thf(tp_c_2Efrac_2Efrac__dnm,type,(c_2Efrac_2Efrac__dnm:$i)).
thf(mem_c_2Efrac_2Efrac__dnm,axiom,(mem@c_2Efrac_2Efrac__dnm@(arr@ty_2Efrac_2Efrac@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Efrac_2Efrac__dnm,type,(fo__c_2Efrac_2Efrac__dnm:(tp__ty_2Efrac_2Efrac > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Efrac_2Efrac__dnm,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Efrac_2Efrac__dnm @ X0)) = (ap @ c_2Efrac_2Efrac__dnm @ (inj__ty_2Efrac_2Efrac @ X0))))).
thf(tp_c_2Efrac_2Efrac__nmr,type,(c_2Efrac_2Efrac__nmr:$i)).
thf(mem_c_2Efrac_2Efrac__nmr,axiom,(mem@c_2Efrac_2Efrac__nmr@(arr@ty_2Efrac_2Efrac@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Efrac_2Efrac__nmr,type,(fo__c_2Efrac_2Efrac__nmr:(tp__ty_2Efrac_2Efrac > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Efrac_2Efrac__nmr,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Efrac_2Efrac__nmr @ X0)) = (ap @ c_2Efrac_2Efrac__nmr @ (inj__ty_2Efrac_2Efrac @ X0))))).
thf(tp_ty_2Epair_2Eprod,type,( ty_2Epair_2Eprod: del > del >del )).
thf(tp_c_2Epair_2E_2C,type,(c_2Epair_2E_2C:(del>(del>$i)))).
thf(mem_c_2Epair_2E_2C,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epair_2E_2C@A_27a@A_27b)@(arr@A_27a@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@A_27b))))))).
thf(stp_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : (tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(surj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : ($i > tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : ((surj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X) @ (ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (surj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2Efrac_2Eabs__frac,type,(c_2Efrac_2Eabs__frac:$i)).
thf(mem_c_2Efrac_2Eabs__frac,axiom,(mem@c_2Efrac_2Eabs__frac@(arr@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@ty_2Efrac_2Efrac))).
thf(stp_fo_c_2Efrac_2Eabs__frac,type,(fo__c_2Efrac_2Eabs__frac:(tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint > tp__ty_2Efrac_2Efrac))).
thf(stp_eq_fo_c_2Efrac_2Eabs__frac,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : ((inj__ty_2Efrac_2Efrac @ (fo__c_2Efrac_2Eabs__frac @ X0)) = (ap @ c_2Efrac_2Eabs__frac @ (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2Erat_2Eabs__rat,type,(c_2Erat_2Eabs__rat:$i)).
thf(mem_c_2Erat_2Eabs__rat,axiom,(mem@c_2Erat_2Eabs__rat@(arr@ty_2Efrac_2Efrac@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Eabs__rat,type,(fo__c_2Erat_2Eabs__rat:(tp__ty_2Efrac_2Efrac > tp__ty_2Erat_2Erat))).
thf(stp_eq_fo_c_2Erat_2Eabs__rat,axiom,( ! [X0:tp__ty_2Efrac_2Efrac] : ((inj__ty_2Erat_2Erat @ (fo__c_2Erat_2Eabs__rat @ X0)) = (ap @ c_2Erat_2Eabs__rat @ (inj__ty_2Efrac_2Efrac @ X0))))).
thf(tp_c_2Erat_2Erat__gre,type,(c_2Erat_2Erat__gre:$i)).
thf(mem_c_2Erat_2Erat__gre,axiom,(mem@c_2Erat_2Erat__gre@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Einteger_2Eint__mul,type,(c_2Einteger_2Eint__mul:$i)).
thf(mem_c_2Einteger_2Eint__mul,axiom,(mem@c_2Einteger_2Eint__mul@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2Einteger_2Eint__mul,type,(fo__c_2Einteger_2Eint__mul:(tp__ty_2Einteger_2Eint > (tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2Einteger_2Eint__mul,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2Einteger_2Eint__mul @ X0) @ X1)) = (ap @ (ap @ c_2Einteger_2Eint__mul @ (inj__ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Einteger_2Eint @ X1)))))).
thf(tp_c_2Erat_2Erat__mul,type,(c_2Erat_2Erat__mul:$i)).
thf(mem_c_2Erat_2Erat__mul,axiom,(mem@c_2Erat_2Erat__mul@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__mul,type,(fo__c_2Erat_2Erat__mul:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(stp_eq_fo_c_2Erat_2Erat__mul,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : ((inj__ty_2Erat_2Erat @ ((fo__c_2Erat_2Erat__mul @ X0) @ X1)) = (ap @ (ap @ c_2Erat_2Erat__mul @ (inj__ty_2Erat_2Erat @ X0)) @ (inj__ty_2Erat_2Erat @ X1)))))).
thf(tp_c_2Erat_2Erat__minv,type,(c_2Erat_2Erat__minv:$i)).
thf(mem_c_2Erat_2Erat__minv,axiom,(mem@c_2Erat_2Erat__minv@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__minv,type,(fo__c_2Erat_2Erat__minv:(tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat))).
thf(stp_eq_fo_c_2Erat_2Erat__minv,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ((inj__ty_2Erat_2Erat @ (fo__c_2Erat_2Erat__minv @ X0)) = (ap @ c_2Erat_2Erat__minv @ (inj__ty_2Erat_2Erat @ X0))))).
thf(tp_c_2Erat_2Erat__leq,type,(c_2Erat_2Erat__leq:$i)).
thf(mem_c_2Erat_2Erat__leq,axiom,(mem@c_2Erat_2Erat__leq@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Erat_2Erat__sub,type,(c_2Erat_2Erat__sub:$i)).
thf(mem_c_2Erat_2Erat__sub,axiom,(mem@c_2Erat_2Erat__sub@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__sub,type,(fo__c_2Erat_2Erat__sub:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(stp_eq_fo_c_2Erat_2Erat__sub,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : ((inj__ty_2Erat_2Erat @ ((fo__c_2Erat_2Erat__sub @ X0) @ X1)) = (ap @ (ap @ c_2Erat_2Erat__sub @ (inj__ty_2Erat_2Erat @ X0)) @ (inj__ty_2Erat_2Erat @ X1)))))).
thf(tp_c_2Erat_2Erat__les,type,(c_2Erat_2Erat__les:$i)).
thf(mem_c_2Erat_2Erat__les,axiom,(mem@c_2Erat_2Erat__les@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@bool)))).
thf(tp_c_2Erat_2Erat__add,type,(c_2Erat_2Erat__add:$i)).
thf(mem_c_2Erat_2Erat__add,axiom,(mem@c_2Erat_2Erat__add@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__add,type,(fo__c_2Erat_2Erat__add:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(stp_eq_fo_c_2Erat_2Erat__add,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : ((inj__ty_2Erat_2Erat @ ((fo__c_2Erat_2Erat__add @ X0) @ X1)) = (ap @ (ap @ c_2Erat_2Erat__add @ (inj__ty_2Erat_2Erat @ X0)) @ (inj__ty_2Erat_2Erat @ X1)))))).
thf(tp_c_2Enum_2ESUC,type,(c_2Enum_2ESUC:$i)).
thf(mem_c_2Enum_2ESUC,axiom,(mem@c_2Enum_2ESUC@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enum_2ESUC,type,(fo__c_2Enum_2ESUC:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enum_2ESUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enum_2ESUC @ X0)) = (ap @ c_2Enum_2ESUC @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Erat_2Erat__0,type,(c_2Erat_2Erat__0:$i)).
thf(mem_c_2Erat_2Erat__0,axiom,(mem@c_2Erat_2Erat__0@ty_2Erat_2Erat)).
thf(stp_fo_c_2Erat_2Erat__0,type,(fo__c_2Erat_2Erat__0:tp__ty_2Erat_2Erat)).
thf(stp_eq_fo_c_2Erat_2Erat__0,axiom,((inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__0) = c_2Erat_2Erat__0)).
thf(tp_c_2Erat_2Erat__1,type,(c_2Erat_2Erat__1:$i)).
thf(mem_c_2Erat_2Erat__1,axiom,(mem@c_2Erat_2Erat__1@ty_2Erat_2Erat)).
thf(stp_fo_c_2Erat_2Erat__1,type,(fo__c_2Erat_2Erat__1:tp__ty_2Erat_2Erat)).
thf(stp_eq_fo_c_2Erat_2Erat__1,axiom,((inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__1) = c_2Erat_2Erat__1)).
thf(tp_c_2Einteger_2Eint__neg,type,(c_2Einteger_2Eint__neg:$i)).
thf(mem_c_2Einteger_2Eint__neg,axiom,(mem@c_2Einteger_2Eint__neg@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Einteger_2Eint__neg,type,(fo__c_2Einteger_2Eint__neg:(tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Einteger_2Eint__neg,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__neg @ X0)) = (ap @ c_2Einteger_2Eint__neg @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2Einteger_2ENum,type,(c_2Einteger_2ENum:$i)).
thf(mem_c_2Einteger_2ENum,axiom,(mem@c_2Einteger_2ENum@(arr@ty_2Einteger_2Eint@ty_2Enum_2Enum))).
thf(stp_fo_c_2Einteger_2ENum,type,(fo__c_2Einteger_2ENum:(tp__ty_2Einteger_2Eint > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Einteger_2ENum,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2Enum_2Enum @ (fo__c_2Einteger_2ENum @ X0)) = (ap @ c_2Einteger_2ENum @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2Erat_2Erat__ainv,type,(c_2Erat_2Erat__ainv:$i)).
thf(mem_c_2Erat_2Erat__ainv,axiom,(mem@c_2Erat_2Erat__ainv@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__ainv,type,(fo__c_2Erat_2Erat__ainv:(tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat))).
thf(stp_eq_fo_c_2Erat_2Erat__ainv,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ((inj__ty_2Erat_2Erat @ (fo__c_2Erat_2Erat__ainv @ X0)) = (ap @ c_2Erat_2Erat__ainv @ (inj__ty_2Erat_2Erat @ X0))))).
thf(tp_c_2Einteger_2Eint__lt,type,(c_2Einteger_2Eint__lt:$i)).
thf(mem_c_2Einteger_2Eint__lt,axiom,(mem@c_2Einteger_2Eint__lt@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@bool)))).
thf(tp_c_2Einteger_2EABS,type,(c_2Einteger_2EABS:$i)).
thf(mem_c_2Einteger_2EABS,axiom,(mem@c_2Einteger_2EABS@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Einteger_2EABS,type,(fo__c_2Einteger_2EABS:(tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Einteger_2EABS,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2EABS @ X0)) = (ap @ c_2Einteger_2EABS @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2Einteger_2Eint__le,type,(c_2Einteger_2Eint__le:$i)).
thf(mem_c_2Einteger_2Eint__le,axiom,(mem@c_2Einteger_2Eint__le@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@bool)))).
thf(tp_c_2Eprim__rec_2E_3C,type,(c_2Eprim__rec_2E_3C:$i)).
thf(mem_c_2Eprim__rec_2E_3C,axiom,(mem@c_2Eprim__rec_2E_3C@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Erat_2ERATD,type,(c_2Erat_2ERATD:$i)).
thf(mem_c_2Erat_2ERATD,axiom,(mem@c_2Erat_2ERATD@(arr@ty_2Erat_2Erat@ty_2Enum_2Enum))).
thf(stp_fo_c_2Erat_2ERATD,type,(fo__c_2Erat_2ERATD:(tp__ty_2Erat_2Erat > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Erat_2ERATD,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ((inj__ty_2Enum_2Enum @ (fo__c_2Erat_2ERATD @ X0)) = (ap @ c_2Erat_2ERATD @ (inj__ty_2Erat_2Erat @ X0))))).
thf(tp_c_2Erat_2ERATN,type,(c_2Erat_2ERATN:$i)).
thf(mem_c_2Erat_2ERATN,axiom,(mem@c_2Erat_2ERATN@(arr@ty_2Erat_2Erat@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Erat_2ERATN,type,(fo__c_2Erat_2ERATN:(tp__ty_2Erat_2Erat > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Erat_2ERATN,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Erat_2ERATN @ X0)) = (ap @ c_2Erat_2ERATN @ (inj__ty_2Erat_2Erat @ X0))))).
thf(tp_c_2Erat_2Erat__of__int,type,(c_2Erat_2Erat__of__int:$i)).
thf(mem_c_2Erat_2Erat__of__int,axiom,(mem@c_2Erat_2Erat__of__int@(arr@ty_2Einteger_2Eint@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__of__int,type,(fo__c_2Erat_2Erat__of__int:(tp__ty_2Einteger_2Eint > tp__ty_2Erat_2Erat))).
thf(stp_eq_fo_c_2Erat_2Erat__of__int,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2Erat_2Erat @ (fo__c_2Erat_2Erat__of__int @ X0)) = (ap @ c_2Erat_2Erat__of__int @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2Erat_2Erat__div,type,(c_2Erat_2Erat__div:$i)).
thf(mem_c_2Erat_2Erat__div,axiom,(mem@c_2Erat_2Erat__div@(arr@ty_2Erat_2Erat@(arr@ty_2Erat_2Erat@ty_2Erat_2Erat)))).
thf(stp_fo_c_2Erat_2Erat__div,type,(fo__c_2Erat_2Erat__div:(tp__ty_2Erat_2Erat > (tp__ty_2Erat_2Erat > tp__ty_2Erat_2Erat)))).
thf(stp_eq_fo_c_2Erat_2Erat__div,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ( ! [X1:tp__ty_2Erat_2Erat] : ((inj__ty_2Erat_2Erat @ ((fo__c_2Erat_2Erat__div @ X0) @ X1)) = (ap @ (ap @ c_2Erat_2Erat__div @ (inj__ty_2Erat_2Erat @ X0)) @ (inj__ty_2Erat_2Erat @ X1)))))).
thf(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
thf(mem_c_2Earithmetic_2EZERO,axiom,(mem@c_2Earithmetic_2EZERO@ty_2Enum_2Enum)).
thf(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
thf(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
thf(mem_c_2Earithmetic_2EBIT1,axiom,(mem@c_2Earithmetic_2EBIT1@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Earithmetic_2EBIT1,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Earithmetic_2EBIT1 @ X0)) = (ap @ c_2Earithmetic_2EBIT1 @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
thf(mem_c_2Earithmetic_2ENUMERAL,axiom,(mem@c_2Earithmetic_2ENUMERAL@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Earithmetic_2ENUMERAL,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Earithmetic_2ENUMERAL @ X0)) = (ap @ c_2Earithmetic_2ENUMERAL @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Einteger_2Eint__of__num,type,(c_2Einteger_2Eint__of__num:$i)).
thf(mem_c_2Einteger_2Eint__of__num,axiom,(mem@c_2Einteger_2Eint__of__num@(arr@ty_2Enum_2Enum@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Einteger_2Eint__of__num,type,(fo__c_2Einteger_2Eint__of__num:(tp__ty_2Enum_2Enum > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Einteger_2Eint__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Einteger_2Eint__of__num @ X0)) = (ap @ c_2Einteger_2Eint__of__num @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
thf(mem_c_2Enum_2E0,axiom,(mem@c_2Enum_2E0@ty_2Enum_2Enum)).
thf(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Enum_2E0,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0) = c_2Enum_2E0)).
thf(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:(del>$i))).
thf(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2ECOND@A_27a)@(arr@bool@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Erat_2Erat__of__num,type,(c_2Erat_2Erat__of__num:$i)).
thf(mem_c_2Erat_2Erat__of__num,axiom,(mem@c_2Erat_2Erat__of__num@(arr@ty_2Enum_2Enum@ty_2Erat_2Erat))).
thf(stp_fo_c_2Erat_2Erat__of__num,type,(fo__c_2Erat_2Erat__of__num:(tp__ty_2Enum_2Enum > tp__ty_2Erat_2Erat))).
thf(stp_eq_fo_c_2Erat_2Erat__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Erat_2Erat @ (fo__c_2Erat_2Erat__of__num @ X0)) = (ap @ c_2Erat_2Erat__of__num @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Erat_2Erat__sgn,type,(c_2Erat_2Erat__sgn:$i)).
thf(mem_c_2Erat_2Erat__sgn,axiom,(mem@c_2Erat_2Erat__sgn@(arr@ty_2Erat_2Erat@ty_2Einteger_2Eint))).
thf(stp_fo_c_2Erat_2Erat__sgn,type,(fo__c_2Erat_2Erat__sgn:(tp__ty_2Erat_2Erat > tp__ty_2Einteger_2Eint))).
thf(stp_eq_fo_c_2Erat_2Erat__sgn,axiom,( ! [X0:tp__ty_2Erat_2Erat] : ((inj__ty_2Einteger_2Eint @ (fo__c_2Erat_2Erat__sgn @ X0)) = (ap @ c_2Erat_2Erat__sgn @ (inj__ty_2Erat_2Erat @ X0))))).
thf(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
thf(mem_c_2Ebool_2EF,axiom,(mem@c_2Ebool_2EF@bool)).
thf(ax_false_p,axiom,(~ (p@c_2Ebool_2EF))).
thf(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
thf(mem_c_2Ebool_2E_2F_5C,axiom,(mem@c_2Ebool_2E_2F_5C@(arr@bool@(arr@bool@bool)))).
thf(ax_and_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_2F_5C@Q)@R)) <=> ((p@Q) & (p@R)))))))).
thf(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:(del>$i))).
thf(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_3D@A_27a)@(arr@A_27a@(arr@A_27a@bool))))).
thf(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : ((mem@X@A) => ( ! [Y:$i] : ((mem@Y@A) => ((p@(ap@(ap@(c_2Emin_2E_3D@A)@X)@Y)) <=> (X = Y)))))))).
thf(tp_c_2Ebool_2E_5C_2F,type,(c_2Ebool_2E_5C_2F:$i)).
thf(mem_c_2Ebool_2E_5C_2F,axiom,(mem@c_2Ebool_2E_5C_2F@(arr@bool@(arr@bool@bool)))).
thf(ax_or_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_5C_2F@Q)@R)) <=> ((p@Q) | (p@R)))))))).
thf(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
thf(mem_c_2Ebool_2E_7E,axiom,(mem@c_2Ebool_2E_7E@(arr@bool@bool))).
thf(ax_neg_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ((p@(ap@c_2Ebool_2E_7E@Q)) <=> (~ (p@Q)))))).
thf(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
thf(mem_c_2Emin_2E_3D_3D_3E,axiom,(mem@c_2Emin_2E_3D_3D_3E@(arr@bool@(arr@bool@bool)))).
thf(ax_imp_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Emin_2E_3D_3D_3E@Q)@R)) <=> ((p@Q) => (p@R)))))))).
thf(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:(del>$i))).
thf(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_21@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_21@A)@Q)) <=> ( ! [X:$i] : ((mem@X@A) => (p@(ap@Q@X))))))))).
thf(conj_thm_2Earithmetic_2ETWO,lemma,((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_2Enum_2ESUC@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Earithmetic_2EADD__CLAUSES,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0m))) = V0m) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V0m) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m)))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))) & ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))))))).
thf(conj_thm_2Earithmetic_2ENOT__ZERO__LT__ZERO,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((~ (V0n = fo__c_2Enum_2E0)) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Earithmetic_2ENOT__LT__ZERO__EQ__ZERO,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((~ (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n)))) <=> (V0n = fo__c_2Enum_2E0)))).
thf(conj_thm_2Earithmetic_2EZERO__LESS__EQ,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))))).
thf(conj_thm_2Earithmetic_2ENOT__LESS,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~ (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m))))))).
thf(conj_thm_2Earithmetic_2EMULT__CLAUSES,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0m))) = fo__c_2Enum_2E0) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0m))) = V0m) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = V0m) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m)))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V1n)))) & ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))))))))).
thf(conj_thm_2Earithmetic_2ELESS__EQ__TRANS,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2p)))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2p)))))))).
thf(conj_thm_2Earithmetic_2EEQ__LESS__EQ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((V0m = V1n) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m)))))))).
thf(conj_thm_2Earithmetic_2EADD__MONO__LESS__EQ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2p)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2p)))))))).
thf(conj_thm_2Earithmetic_2ENOT__LEQ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~ (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V0m))))))).
thf(conj_thm_2Earithmetic_2ENOT__NUM__EQ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~ (V0m = V1n)) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m)))@(inj__ty_2Enum_2Enum @ V1n))) | (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V0m)))))))).
thf(conj_thm_2Earithmetic_2ESUC__ONE__ADD,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(ax_thm_2Ebool_2EBOOL__CASES__AX,axiom,( ! [V0t:$i] : ((mem@V0t@bool) => (((p@V0t) <=> $true) | ((p@V0t) <=> $false))))).
thf(ax_thm_2Ebool_2EETA__AX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@A_27b)) => ((lam@A_27a@(^ [V1x:$i] : (ap@V0t@V1x))) = V0t)))))).
thf(conj_thm_2Ebool_2ETRUTH,lemma,$true).
thf(conj_thm_2Ebool_2EIMP__ANTISYM__AX,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => (((p@V0t1) => (p@V1t2)) => (((p@V1t2) => (p@V0t1)) => ((p@V0t1) <=> (p@V1t2))))))))).
thf(conj_thm_2Ebool_2EFALSITY,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ($false => (p@V0t))))).
thf(conj_thm_2Ebool_2EEXCLUDED__MIDDLE,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((p@V0t) | (~ (p@V0t)))))).
thf(conj_thm_2Ebool_2EFORALL__SIMP,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@bool) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@V0t))) <=> (p@V0t)))))).
thf(conj_thm_2Ebool_2EIMP__F,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => (((p@V0t) => $false) => (~ (p@V0t)))))).
thf(conj_thm_2Ebool_2EF__IMP,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (p@V0t)) => ((p@V0t) => $false))))).
thf(conj_thm_2Ebool_2EAND__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true & (p@V0t)) <=> (p@V0t)) & ((((p@V0t) & $true) <=> (p@V0t)) & ((($false & (p@V0t)) <=> $false) & ((((p@V0t) & $false) <=> $false) & (((p@V0t) & (p@V0t)) <=> (p@V0t))))))))).
thf(conj_thm_2Ebool_2EOR__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true | (p@V0t)) <=> $true) & ((((p@V0t) | $true) <=> $true) & ((($false | (p@V0t)) <=> (p@V0t)) & ((((p@V0t) | $false) <=> (p@V0t)) & (((p@V0t) | (p@V0t)) <=> (p@V0t))))))))).
thf(conj_thm_2Ebool_2EIMP__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true => (p@V0t)) <=> (p@V0t)) & ((((p@V0t) => $true) <=> $true) & ((($false => (p@V0t)) <=> $true) & ((((p@V0t) => (p@V0t)) <=> $true) & (((p@V0t) => $false) <=> (~ (p@V0t)))))))))).
thf(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,(( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t)))) & (((~ ($true)) <=> $false) & ((~ ($false)) <=> $true)))).
thf(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((V0x = V0x) <=> $true))))).
thf(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((V0x = V1y) <=> (V1y = V0x)))))))).
thf(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true <=> (p@V0t)) <=> (p@V0t)) & ((((p@V0t) <=> $true) <=> (p@V0t)) & ((($false <=> (p@V0t)) <=> (~ (p@V0t))) & (((p@V0t) <=> $false) <=> (~ (p@V0t))))))))).
thf(conj_thm_2Ebool_2ECOND__CLAUSES,lemma,( ! [A_27a:del]: ( ! [V0t1:$i] : ((mem@V0t1@A_27a) => ( ! [V1t2:$i] : ((mem@V1t2@A_27a) => (((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2ET)@V0t1)@V1t2) = V0t1) & ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2EF)@V0t1)@V1t2) = V1t2)))))))).
thf(conj_thm_2Ebool_2ENOT__FORALL__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((~ ( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@(ap@V0P@V1x))))) <=> (? [V2x:$i] : ((mem@V2x@A_27a) & (~ (p@(ap@V0P@V2x)))))))))).
thf(conj_thm_2Ebool_2ENOT__IMP,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ((~ ((p@V0A) => (p@V1B))) <=> ((p@V0A) & (~ (p@V1B))))))))).
thf(conj_thm_2Ebool_2EDISJ__ASSOC,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ( ! [V2C:$i] : ((mem@V2C@bool) => (((p@V0A) | ((p@V1B) | (p@V2C))) <=> (((p@V0A) | (p@V1B)) | (p@V2C)))))))))).
thf(conj_thm_2Ebool_2EDISJ__SYM,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((p@V0A) | (p@V1B)) <=> ((p@V1B) | (p@V0A)))))))).
thf(conj_thm_2Ebool_2EDE__MORGAN__THM,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((p@V0A) & (p@V1B))) <=> ((~ (p@V0A)) | (~ (p@V1B)))) & ((~ ((p@V0A) | (p@V1B))) <=> ((~ (p@V0A)) & (~ (p@V1B)))))))))).
thf(conj_thm_2Ebool_2EIMP__F__EQ__F,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => (((p@V0t) => $false) <=> ((p@V0t) <=> $false))))).
thf(conj_thm_2Ebool_2EAND__IMP__INTRO,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => ( ! [V2t3:$i] : ((mem@V2t3@bool) => (((p@V0t1) => ((p@V1t2) => (p@V2t3))) <=> (((p@V0t1) & (p@V1t2)) => (p@V2t3)))))))))).
thf(conj_thm_2Ebool_2EIMP__CONG,lemma,( ! [V0x:$i] : ((mem@V0x@bool) => ( ! [V1x_27:$i] : ((mem@V1x_27@bool) => ( ! [V2y:$i] : ((mem@V2y@bool) => ( ! [V3y_27:$i] : ((mem@V3y_27@bool) => ((((p@V0x) <=> (p@V1x_27)) & ((p@V1x_27) => ((p@V2y) <=> (p@V3y_27)))) => (((p@V0x) => (p@V2y)) <=> ((p@V1x_27) => (p@V3y_27))))))))))))).
thf(conj_thm_2Ebool_2ECOND__CONG,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@bool) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3x_27:$i] : ((mem@V3x_27@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => ( ! [V5y_27:$i] : ((mem@V5y_27@A_27a) => ((((p@V0P) <=> (p@V1Q)) & (((p@V1Q) => (V2x = V3x_27)) & ((~ (p@V1Q)) => (V4y = V5y_27)))) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@V0P)@V2x)@V4y) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@V1Q)@V3x_27)@V5y_27))))))))))))))))).
thf(conj_thm_2Ebool_2Ebool__case__thm,lemma,( ! [A_27a:del]: (( ! [V0t1:$i] : ((mem@V0t1@A_27a) => ( ! [V1t2:$i] : ((mem@V1t2@A_27a) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2ET)@V0t1)@V1t2) = V0t1))))) & ( ! [V2t1:$i] : ((mem@V2t1@A_27a) => ( ! [V3t2:$i] : ((mem@V3t2@A_27a) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2EF)@V2t1)@V3t2) = V3t2)))))))).
thf(conj_thm_2Ebool_2EBOUNDED__THM,lemma,( ! [V0v:$i] : ((mem@V0v@bool) => ((p@(ap@c_2Ebool_2EBOUNDED@V0v)) <=> $true)))).
thf(ax_thm_2Efrac_2Efrac__sgn__def,axiom,( ! [V0f1:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Efrac_2Efrac__sgn@(inj__ty_2Efrac_2Efrac @ V0f1))) = (surj__ty_2Einteger_2Eint @ (ap@c_2EintExtension_2ESGN@(ap@c_2Efrac_2Efrac__nmr@(inj__ty_2Efrac_2Efrac @ V0f1))))))).
thf(ax_thm_2Efrac_2Efrac__0__def,axiom,(fo__c_2Efrac_2Efrac__0 = (surj__ty_2Efrac_2Efrac @ (ap@c_2Efrac_2Eabs__frac@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Efrac_2ENMR,lemma,( ! [V0a:tp__ty_2Einteger_2Eint] : ( ! [V1b:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Einteger_2Eint @ V1b))) => ((surj__ty_2Einteger_2Eint @ (ap@c_2Efrac_2Efrac__nmr@(ap@c_2Efrac_2Eabs__frac@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V0a))@(inj__ty_2Einteger_2Eint @ V1b))))) = V0a))))).
thf(conj_thm_2Efrac_2EDNM,lemma,( ! [V0a:tp__ty_2Einteger_2Eint] : ( ! [V1b:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Einteger_2Eint @ V1b))) => ((surj__ty_2Einteger_2Eint @ (ap@c_2Efrac_2Efrac__dnm@(ap@c_2Efrac_2Eabs__frac@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V0a))@(inj__ty_2Einteger_2Eint @ V1b))))) = V1b))))).
thf(conj_thm_2Efrac_2EFRAC__AINV__0,lemma,((surj__ty_2Efrac_2Efrac @ (ap@c_2Efrac_2Efrac__ainv@(inj__ty_2Efrac_2Efrac @ fo__c_2Efrac_2Efrac__0))) = fo__c_2Efrac_2Efrac__0)).
thf(conj_thm_2Efrac_2EFRAC__AINV__AINV,lemma,( ! [V0f1:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Efrac_2Efrac @ (ap@c_2Efrac_2Efrac__ainv@(ap@c_2Efrac_2Efrac__ainv@(inj__ty_2Efrac_2Efrac @ V0f1)))) = V0f1))).
thf(ax_thm_2EintExtension_2ESGN__def,axiom,( ! [V0x:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@c_2EintExtension_2ESGN@(inj__ty_2Einteger_2Eint @ V0x))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Einteger_2Eint)@(ap@(ap@(c_2Emin_2E_3D@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V0x))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Einteger_2Eint)@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V0x))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Einteger_2EINT__MUL__RID,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V0x))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V0x))).
thf(conj_thm_2Einteger_2EINT__NEGNEG,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ V0x)))) = V0x))).
thf(conj_thm_2Einteger_2EINT__LT__01,lemma,(p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Einteger_2EINT__NEG__0,lemma,((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Einteger_2EINT__LE,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0m)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Einteger_2EINT__LT,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0m)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Einteger_2EINT__INJ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0m))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1n)))) <=> (V0m = V1n))))).
thf(conj_thm_2Einteger_2EINT__LT__CALCULATE,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1m))))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n)))) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1m)))) <=> ((~ (V0n = fo__c_2Enum_2E0)) | (~ (V1m = fo__c_2Enum_2E0)))) & ((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1m))))) <=> $false))))))).
thf(conj_thm_2Einteger_2EINT__NUM__CASES,lemma,( ! [V0p:tp__ty_2Einteger_2Eint] : ((? [V1n:tp__ty_2Enum_2Enum] : ((V0p = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1n)))) & (~ (V1n = fo__c_2Enum_2E0)))) | ((? [V2n:tp__ty_2Enum_2Enum] : ((V0p = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2n))))) & (~ (V2n = fo__c_2Enum_2E0)))) | (V0p = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Einteger_2ENUM__OF__INT,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Einteger_2ENum@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n)))) = V0n))).
thf(conj_thm_2Einteger_2EINT__LT__REDUCE,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))))) <=> $true) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))))) <=> $true) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> $false) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0n)))))) <=> $false) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> $false) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> $true) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> $true) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V1m))))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V1m))))) <=> $true) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))))))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V1m))))) <=> $true) & (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V1m)))))) <=> $false) & ((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V0n)))))@(ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V1m)))))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n)))))))))))))))))).
thf(conj_thm_2Einteger_2EINT__EQ__CALCULATE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0m))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V1n)))) <=> (V0m = V1n)))) & (( ! [V2x:tp__ty_2Einteger_2Eint] : ( ! [V3y:tp__ty_2Einteger_2Eint] : (((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ V2x))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ V3y)))) <=> (V2x = V3y)))) & ( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ((((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4n))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V5m))))) <=> ((V4n = fo__c_2Enum_2E0) & (V5m = fo__c_2Enum_2E0))) & (((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4n)))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V5m)))) <=> ((V4n = fo__c_2Enum_2E0) & (V5m = fo__c_2Enum_2E0))))))))).
thf(ax_thm_2Emarker_2EAbbrev__def,axiom,( ! [V0x:$i] : ((mem@V0x@bool) => ((p@(ap@c_2Emarker_2EAbbrev@V0x)) <=> (p@V0x))))).
thf(ax_thm_2Emarker_2ECong__def,axiom,( ! [V0x:$i] : ((mem@V0x@bool) => ((p@(ap@c_2Emarker_2ECong@V0x)) <=> (p@V0x))))).
thf(conj_thm_2Enum_2ENOT__SUC,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (~ ((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n))) = fo__c_2Enum_2E0)))).
thf(conj_thm_2Enum_2EINDUCTION,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => (((p@(ap@V0P@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@V0P@(inj__ty_2Enum_2Enum @ V1n))) => (p@(ap@V0P@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))))) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V2n)))))))).
thf(conj_thm_2Enumeral_2Enumeral__distrib,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) = V0n)) & (( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V1n)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m)))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V4n))) = fo__c_2Enum_2E0)) & (( ! [V5n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V5n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V6n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V7m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V6n))@(inj__ty_2Enum_2Enum @ V7m))))))) & (( ! [V8n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V8n))) = fo__c_2Enum_2E0)) & (( ! [V9n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V9n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V9n)) & (( ! [V10n:tp__ty_2Enum_2Enum] : ( ! [V11m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V10n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V11m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V10n))@(inj__ty_2Enum_2Enum @ V11m))))))) & (( ! [V12n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V12n))))) = fo__c_2Enum_2E0)) & (( ! [V13n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V13n))))) = fo__c_2Enum_2E0)) & (( ! [V14n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V14n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (( ! [V15n:tp__ty_2Enum_2Enum] : ( ! [V16m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V15n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V16m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V15n))@(inj__ty_2Enum_2Enum @ V16m))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (( ! [V17n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V17n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V17n)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & (( ! [V18n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V18n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ V18n)))))) & (( ! [V19n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V19n))) = fo__c_2Enum_2E0) <=> (V19n = fo__c_2Earithmetic_2EZERO))) & (( ! [V20n:tp__ty_2Enum_2Enum] : ((fo__c_2Enum_2E0 = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V20n)))) <=> (V20n = fo__c_2Earithmetic_2EZERO))) & (( ! [V21n:tp__ty_2Enum_2Enum] : ( ! [V22m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V21n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V22m)))) <=> (V21n = V22m)))) & (( ! [V23n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V23n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false)) & (( ! [V24n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V24n)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V24n))))) & (( ! [V25n:tp__ty_2Enum_2Enum] : ( ! [V26m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V25n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V26m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V25n))@(inj__ty_2Enum_2Enum @ V26m)))))) & (( ! [V27n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V27n))) <=> $false)) & (( ! [V28n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V28n)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V28n))))) & (( ! [V29n:tp__ty_2Enum_2Enum] : ( ! [V30m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V29n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V30m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V30m))@(inj__ty_2Enum_2Enum @ V29n)))))) & (( ! [V31n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V31n))) <=> $true)) & (( ! [V32n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V32n)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V32n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (( ! [V33n:tp__ty_2Enum_2Enum] : ( ! [V34m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V33n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V34m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V33n))@(inj__ty_2Enum_2Enum @ V34m)))))) & (( ! [V35n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V35n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true)) & (( ! [V36n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V36n))) <=> (V36n = fo__c_2Enum_2E0))) & (( ! [V37n:tp__ty_2Enum_2Enum] : ( ! [V38m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V37n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V38m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V38m))@(inj__ty_2Enum_2Enum @ V37n)))))) & (( ! [V39n:tp__ty_2Enum_2Enum] : ((p@(ap@c_2Earithmetic_2EODD@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V39n)))) <=> (p@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ V39n))))) & (( ! [V40n:tp__ty_2Enum_2Enum] : ((p@(ap@c_2Earithmetic_2EEVEN@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V40n)))) <=> (p@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ V40n))))) & ((~ (p@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (p@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__eq,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((fo__c_2Earithmetic_2EZERO = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((fo__c_2Earithmetic_2EZERO = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m)) & (((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m)))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__lte,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0n))) <=> $true) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) <=> $false) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) <=> $false) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (~ (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))))) & ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))))))))).
thf(conj_thm_2Eprim__rec_2EINV__SUC__EQ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) <=> (V0m = V1n))))).
thf(conj_thm_2Eprim__rec_2ENOT__LESS__0,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (~ (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(ax_thm_2Equotient_2EQUOTIENT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1abs:$i] : ((mem@V1abs@(arr@A_27a@A_27b)) => ( ! [V2rep:$i] : ((mem@V2rep@(arr@A_27b@A_27a)) => ((p@(ap@(ap@(ap@(c_2Equotient_2EQUOTIENT@A_27a@A_27b)@V0R)@V1abs)@V2rep)) <=> (( ! [V3a:$i] : ((mem@V3a@A_27b) => ((ap@V1abs@(ap@V2rep@V3a)) = V3a))) & (( ! [V4a:$i] : ((mem@V4a@A_27b) => (p@(ap@(ap@V0R@(ap@V2rep@V4a))@(ap@V2rep@V4a))))) & ( ! [V5r:$i] : ((mem@V5r@A_27a) => ( ! [V6s:$i] : ((mem@V6s@A_27a) => ((p@(ap@(ap@V0R@V5r)@V6s)) <=> ((p@(ap@(ap@V0R@V5r)@V5r)) & ((p@(ap@(ap@V0R@V6s)@V6s)) & ((ap@V1abs@V5r) = (ap@V1abs@V6s))))))))))))))))))))).
thf(conj_thm_2Erat_2Erat__def,lemma,(p@(ap@(ap@(ap@(c_2Equotient_2EQUOTIENT@ty_2Efrac_2Efrac@ty_2Erat_2Erat)@c_2Erat_2Erat__equiv)@c_2Erat_2Eabs__rat)@c_2Erat_2Erep__rat))).
thf(ax_thm_2Erat_2Erat__sgn__def,axiom,( ! [V0r:tp__ty_2Erat_2Erat] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Efrac_2Efrac__sgn@(ap@c_2Erat_2Erep__rat@(inj__ty_2Erat_2Erat @ V0r))))))).
thf(ax_thm_2Erat_2Erat__ainv__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@c_2Efrac_2Efrac__ainv@(ap@c_2Erat_2Erep__rat@(inj__ty_2Erat_2Erat @ V0r1)))))))).
thf(ax_thm_2Erat_2Erat__gre__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__gre@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V0r1))))))).
thf(ax_thm_2Erat_2Erat__leq__def,axiom,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__leq@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))) <=> ((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))) | (V0r1 = V1r2)))))).
thf(conj_thm_2Erat_2Erat__0,lemma,((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ fo__c_2Efrac_2Efrac__0))))).
thf(conj_thm_2Erat_2ERAT__SGN__CONG,lemma,( ! [V0f1:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Efrac_2Efrac__sgn@(ap@c_2Erat_2Erep__rat@(ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ V0f1))))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Efrac_2Efrac__sgn@(inj__ty_2Efrac_2Efrac @ V0f1)))))).
thf(conj_thm_2Erat_2ERAT__AINV__CONG,lemma,( ! [V0x:tp__ty_2Efrac_2Efrac] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@c_2Efrac_2Efrac__ainv@(ap@c_2Erat_2Erep__rat@(ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ V0x)))))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@c_2Efrac_2Efrac__ainv@(inj__ty_2Efrac_2Efrac @ V0x))))))).
thf(conj_thm_2Erat_2ERAT__LES__CALCULATE,lemma,( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ V0f1)))@(ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ V1f2)))) <=> (p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Efrac_2Efrac__nmr@(inj__ty_2Efrac_2Efrac @ V0f1)))@(ap@c_2Efrac_2Efrac__dnm@(inj__ty_2Efrac_2Efrac @ V1f2))))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Efrac_2Efrac__nmr@(inj__ty_2Efrac_2Efrac @ V1f2)))@(ap@c_2Efrac_2Efrac__dnm@(inj__ty_2Efrac_2Efrac @ V0f1))))))))).
thf(conj_thm_2Erat_2ERAT__LEQ__CALCULATE,lemma,( ! [V0f1:tp__ty_2Efrac_2Efrac] : ( ! [V1f2:tp__ty_2Efrac_2Efrac] : ((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ V0f1)))@(ap@c_2Erat_2Eabs__rat@(inj__ty_2Efrac_2Efrac @ V1f2)))) <=> (p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Efrac_2Efrac__nmr@(inj__ty_2Efrac_2Efrac @ V0f1)))@(ap@c_2Efrac_2Efrac__dnm@(inj__ty_2Efrac_2Efrac @ V1f2))))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Efrac_2Efrac__nmr@(inj__ty_2Efrac_2Efrac @ V1f2)))@(ap@c_2Efrac_2Efrac__dnm@(inj__ty_2Efrac_2Efrac @ V0f1))))))))).
thf(conj_thm_2Erat_2ERAT__OF__NUM__CALCULATE,lemma,( ! [V0n1:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n1))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Eabs__rat@(ap@c_2Efrac_2Eabs__frac@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0n1)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(conj_thm_2Erat_2ERAT__OF__NUM__LES,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0a)))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V1b)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b))))))).
thf(conj_thm_2Erat_2ERAT__ADD__COMM,lemma,( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0a))@(inj__ty_2Erat_2Erat @ V1b))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V1b))@(inj__ty_2Erat_2Erat @ V0a))))))).
thf(conj_thm_2Erat_2ERAT__SUB__ADDAINV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__sub@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0r1))@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__DIV__MULMINV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(ap@c_2Erat_2Erat__minv@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__AINV__0,lemma,((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Erat_2ERAT__AINV__ADD,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1)))@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__AINV__EQ,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1))) = V1r2) <=> (V0r1 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__EQ__AINV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1))) = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))) <=> (V0r1 = V1r2))))).
thf(conj_thm_2Erat_2ERAT__SGN__CLAUSES,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ((((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r1))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r1))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V0r1 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r1))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) <=> (p@(ap@(ap@c_2Erat_2Erat__gre@(inj__ty_2Erat_2Erat @ V0r1))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Erat_2ERAT__SGN__AINV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__neg@(ap@c_2Erat_2Erat__sgn@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1))))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r1)))))).
thf(conj_thm_2Erat_2ERAT__SGN__MUL,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(ap@(ap@c_2Erat_2Erat__mul@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r1)))@(ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V1r2)))))))).
thf(conj_thm_2Erat_2ERAT__SGN__MINV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ((~ (V0r1 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(ap@c_2Erat_2Erat__minv@(inj__ty_2Erat_2Erat @ V0r1)))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r1))))))).
thf(conj_thm_2Erat_2ERAT__LES__ANTISYM,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))) => (~ (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V0r1)))))))).
thf(conj_thm_2Erat_2ERAT__LEQ__REF,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : (p@(ap@(ap@c_2Erat_2Erat__leq@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V0r1))))).
thf(conj_thm_2Erat_2ERAT__LES__01,lemma,(p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Erat_2ERAT__LES__LEQ__TRANS,lemma,( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (((p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0a))@(inj__ty_2Erat_2Erat @ V1b))) & (p@(ap@(ap@c_2Erat_2Erat__leq@(inj__ty_2Erat_2Erat @ V1b))@(inj__ty_2Erat_2Erat @ V2c)))) => (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0a))@(inj__ty_2Erat_2Erat @ V2c)))))))).
thf(conj_thm_2Erat_2ERAT__LEQ__LES__TRANS,lemma,( ! [V0a:tp__ty_2Erat_2Erat] : ( ! [V1b:tp__ty_2Erat_2Erat] : ( ! [V2c:tp__ty_2Erat_2Erat] : (((p@(ap@(ap@c_2Erat_2Erat__leq@(inj__ty_2Erat_2Erat @ V0a))@(inj__ty_2Erat_2Erat @ V1b))) & (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V1b))@(inj__ty_2Erat_2Erat @ V2c)))) => (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V0a))@(inj__ty_2Erat_2Erat @ V2c)))))))).
thf(conj_thm_2Erat_2ERAT__0LES__0LEQ__ADD,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erat_2Erat @ V0r1))) => ((p@(ap@(ap@c_2Erat_2Erat__leq@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erat_2Erat @ V1r2))) => (p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V1r2))))))))).
thf(conj_thm_2Erat_2ERAT__RSUB__EQ,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : ((V0r1 = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__sub@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> ((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3))) = V1r2)))))).
thf(conj_thm_2Erat_2ERAT__EQ__RADD,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ( ! [V2r3:tp__ty_2Erat_2Erat] : (((surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V0r1))@(inj__ty_2Erat_2Erat @ V2r3))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V2r3)))) <=> (V0r1 = V1r2)))))).
thf(conj_thm_2Erat_2ERAT__LES__AINV,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1)))@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(inj__ty_2Erat_2Erat @ V1r2))@(inj__ty_2Erat_2Erat @ V0r1))))))).
thf(conj_thm_2Erat_2ERAT__AINV__LES,lemma,( ! [V0r1:tp__ty_2Erat_2Erat] : ( ! [V1r2:tp__ty_2Erat_2Erat] : ((p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V0r1)))@(inj__ty_2Erat_2Erat @ V1r2))) <=> (p@(ap@(ap@c_2Erat_2Erat__les@(ap@c_2Erat_2Erat__ainv@(inj__ty_2Erat_2Erat @ V1r2)))@(inj__ty_2Erat_2Erat @ V0r1))))))).
thf(conj_thm_2Erat_2ERAT__OF__NUM,lemma,( ! [A_27a:del]: ( ! [V0n:$i] : ((mem@V0n@A_27a) => (((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Erat_2Erat__0) & ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__add@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Erat_2Erat @ fo__c_2Erat_2Erat__1)))))))))).
thf(conj_thm_2Erat_2ERAT__0,lemma,(fo__c_2Erat_2Erat__0 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Erat_2ERAT__1,lemma,(fo__c_2Erat_2Erat__1 = (surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(ax_thm_2Erat_2Erat__of__int__def,axiom,( ! [V0i:tp__ty_2Einteger_2Eint] : ((surj__ty_2Erat_2Erat @ (ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V0i))) = (surj__ty_2Erat_2Erat @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erat_2Erat)@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V0i))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Erat_2Erat__ainv@(ap@c_2Erat_2Erat__of__num@(ap@c_2Einteger_2ENum@(ap@c_2Einteger_2Eint__neg@(inj__ty_2Einteger_2Eint @ V0i))))))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Einteger_2ENum@(inj__ty_2Einteger_2Eint @ V0i)))))))).
thf(ax_thm_2Erat_2ERATND__THM,axiom,( ! [V0r:tp__ty_2Erat_2Erat] : ((V0r = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@c_2Erat_2Erat__of__int@(ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r)))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r)))) & ((((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ( ! [V1n_27:tp__ty_2Einteger_2Eint] : ( ! [V2d_27:tp__ty_2Enum_2Enum] : (((V0r = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@c_2Erat_2Erat__of__int@(inj__ty_2Einteger_2Eint @ V1n_27)))@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V2d_27))))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2d_27)))) => (p@(ap@(ap@c_2Einteger_2Eint__le@(ap@c_2Einteger_2EABS@(ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))))@(ap@c_2Einteger_2EABS@(inj__ty_2Einteger_2Eint @ V1n_27)))))))))))).
thf(conj_thm_2Erat_2ERATN__RATD__EQ__THM,lemma,( ! [V0r:tp__ty_2Erat_2Erat] : (V0r = (surj__ty_2Erat_2Erat @ (ap@(ap@c_2Erat_2Erat__div@(ap@c_2Erat_2Erat__of__int@(ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))))@(ap@c_2Erat_2Erat__of__num@(ap@c_2Erat_2ERATD@(inj__ty_2Erat_2Erat @ V0r)))))))).
thf(conj_thm_2Erat_2ERAT__SGN__NUM__COND,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(ap@c_2Erat_2Erat__of__num@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Einteger_2Eint)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Esat_2ENOT__NOT,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t))))).
thf(conj_thm_2Esat_2EAND__INV__IMP,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ((p@V0A) => ((~ (p@V0A)) => $false))))).
thf(conj_thm_2Esat_2EOR__DUAL2,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((p@V0A) | (p@V1B))) => $false) <=> (((p@V0A) => $false) => ((~ (p@V1B)) => $false)))))))).
thf(conj_thm_2Esat_2EOR__DUAL3,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((~ (p@V0A)) | (p@V1B))) => $false) <=> ((p@V0A) => ((~ (p@V1B)) => $false)))))))).
thf(conj_thm_2Esat_2EAND__INV2,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => (((~ (p@V0A)) => $false) => (((p@V0A) => $false) => $false))))).
thf(conj_thm_2Esat_2Edc__eq,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) <=> (p@V2r))) <=> (((p@V0p) | ((p@V1q) | (p@V2r))) & (((p@V0p) | ((~ (p@V2r)) | (~ (p@V1q)))) & (((p@V1q) | ((~ (p@V2r)) | (~ (p@V0p)))) & ((p@V2r) | ((~ (p@V1q)) | (~ (p@V0p))))))))))))))).
thf(conj_thm_2Esat_2Edc__conj,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) & (p@V2r))) <=> (((p@V0p) | ((~ (p@V1q)) | (~ (p@V2r)))) & (((p@V1q) | (~ (p@V0p))) & ((p@V2r) | (~ (p@V0p))))))))))))).
thf(conj_thm_2Esat_2Edc__disj,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) | (p@V2r))) <=> (((p@V0p) | (~ (p@V1q))) & (((p@V0p) | (~ (p@V2r))) & ((p@V1q) | ((p@V2r) | (~ (p@V0p)))))))))))))).
thf(conj_thm_2Esat_2Edc__imp,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) => (p@V2r))) <=> (((p@V0p) | (p@V1q)) & (((p@V0p) | (~ (p@V2r))) & ((~ (p@V1q)) | ((p@V2r) | (~ (p@V0p)))))))))))))).
thf(conj_thm_2Esat_2Edc__neg,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => (((p@V0p) <=> (~ (p@V1q))) <=> (((p@V0p) | (p@V1q)) & ((~ (p@V1q)) | (~ (p@V0p)))))))))).
thf(conj_thm_2Esat_2Epth__ni1,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) => (p@V1q))) => (p@V0p))))))).
thf(conj_thm_2Esat_2Epth__ni2,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) => (p@V1q))) => (~ (p@V1q)))))))).
thf(conj_thm_2Esat_2Epth__no1,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) | (p@V1q))) => (~ (p@V0p)))))))).
thf(conj_thm_2Esat_2Epth__no2,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) | (p@V1q))) => (~ (p@V1q)))))))).
thf(conj_thm_2Esat_2Epth__nn,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ((~ (~ (p@V0p))) => (p@V0p))))).
thf(conj_thm_2Erat_2ERAT__SGN__ALT,conjecture,( ! [V0r:tp__ty_2Erat_2Erat] : ((surj__ty_2Einteger_2Eint @ (ap@c_2Erat_2Erat__sgn@(inj__ty_2Erat_2Erat @ V0r))) = (surj__ty_2Einteger_2Eint @ (ap@c_2EintExtension_2ESGN@(ap@c_2Erat_2ERATN@(inj__ty_2Erat_2Erat @ V0r))))))).
