include('Axioms/lim^2.ax').
thf(stp_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,type,(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,type,(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal : (tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,type,(surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal : ($i > tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (mem @ (inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ X) @ (ty_2Elist_2Elist@ty_2Erealax_2Ereal)))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@ty_2Erealax_2Ereal)) => (X = (inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ X)))))).
thf(tp_c_2Epoly_2E_23_23,type,(c_2Epoly_2E_23_23:$i)).
thf(mem_c_2Epoly_2E_23_23,axiom,(mem@c_2Epoly_2E_23_23@(arr@ty_2Erealax_2Ereal@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))))).
thf(tp_c_2Epoly_2Edegree,type,(c_2Epoly_2Edegree:$i)).
thf(mem_c_2Epoly_2Edegree,axiom,(mem@c_2Epoly_2Edegree@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Epoly_2Edegree,type,(fo__c_2Epoly_2Edegree:(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Epoly_2Edegree,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((inj__ty_2Enum_2Enum @ (fo__c_2Epoly_2Edegree @ X0)) = (ap @ c_2Epoly_2Edegree @ (inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ X0))))).
thf(tp_c_2Epoly_2Ediff,type,(c_2Epoly_2Ediff:$i)).
thf(mem_c_2Epoly_2Ediff,axiom,(mem@c_2Epoly_2Ediff@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)))).
thf(tp_c_2Epoly_2Enormalize,type,(c_2Epoly_2Enormalize:$i)).
thf(mem_c_2Epoly_2Enormalize,axiom,(mem@c_2Epoly_2Enormalize@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)))).
thf(tp_c_2Epoly_2Epoly,type,(c_2Epoly_2Epoly:$i)).
thf(mem_c_2Epoly_2Epoly,axiom,(mem@c_2Epoly_2Epoly@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Epoly_2Epoly,type,(fo__c_2Epoly_2Epoly:(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal > (tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal)))).
thf(stp_eq_fo_c_2Epoly_2Epoly,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ ((fo__c_2Epoly_2Epoly @ X0) @ X1)) = (ap @ (ap @ c_2Epoly_2Epoly @ (inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ X0)) @ (inj__ty_2Erealax_2Ereal @ X1)))))).
thf(tp_c_2Epoly_2Epoly__add,type,(c_2Epoly_2Epoly__add:$i)).
thf(mem_c_2Epoly_2Epoly__add,axiom,(mem@c_2Epoly_2Epoly__add@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))))).
thf(tp_c_2Epoly_2Epoly__diff__aux,type,(c_2Epoly_2Epoly__diff__aux:$i)).
thf(mem_c_2Epoly_2Epoly__diff__aux,axiom,(mem@c_2Epoly_2Epoly__diff__aux@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))))).
thf(tp_c_2Epoly_2Epoly__divides,type,(c_2Epoly_2Epoly__divides:$i)).
thf(mem_c_2Epoly_2Epoly__divides,axiom,(mem@c_2Epoly_2Epoly__divides@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@bool)))).
thf(tp_c_2Epoly_2Epoly__exp,type,(c_2Epoly_2Epoly__exp:$i)).
thf(mem_c_2Epoly_2Epoly__exp,axiom,(mem@c_2Epoly_2Epoly__exp@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))))).
thf(tp_c_2Epoly_2Epoly__mul,type,(c_2Epoly_2Epoly__mul:$i)).
thf(mem_c_2Epoly_2Epoly__mul,axiom,(mem@c_2Epoly_2Epoly__mul@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))))).
thf(tp_c_2Epoly_2Epoly__neg,type,(c_2Epoly_2Epoly__neg:$i)).
thf(mem_c_2Epoly_2Epoly__neg,axiom,(mem@c_2Epoly_2Epoly__neg@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)))).
thf(tp_c_2Epoly_2Epoly__order,type,(c_2Epoly_2Epoly__order:$i)).
thf(mem_c_2Epoly_2Epoly__order,axiom,(mem@c_2Epoly_2Epoly__order@(arr@ty_2Erealax_2Ereal@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Epoly_2Epoly__order,type,(fo__c_2Epoly_2Epoly__order:(tp__ty_2Erealax_2Ereal > (tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Epoly_2Epoly__order,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Epoly_2Epoly__order @ X0) @ X1)) = (ap @ (ap @ c_2Epoly_2Epoly__order @ (inj__ty_2Erealax_2Ereal @ X0)) @ (inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ X1)))))).
thf(tp_c_2Epoly_2Ersquarefree,type,(c_2Epoly_2Ersquarefree:$i)).
thf(mem_c_2Epoly_2Ersquarefree,axiom,(mem@c_2Epoly_2Ersquarefree@(arr@(ty_2Elist_2Elist@ty_2Erealax_2Ereal)@bool))).
thf(ax_thm_2Epoly_2Epoly__def,axiom,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(inj__ty_2Erealax_2Ereal @ V0x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ( ! [V1h:tp__ty_2Erealax_2Ereal] : ( ! [V2t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))@(inj__ty_2Erealax_2Ereal @ V3x))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V1h))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V3x))@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t))@(inj__ty_2Erealax_2Ereal @ V3x))))))))))).
thf(ax_thm_2Epoly_2Epoly__add__def,axiom,(( ! [V0l2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l2))) = V0l2)) & ( ! [V1h:tp__ty_2Erealax_2Ereal] : ( ! [V2t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V3l2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V1h))@(ap@(c_2Elist_2EHD@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2))))@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t))@(ap@(c_2Elist_2ETL@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2)))))))))))).
thf(ax_thm_2Epoly_2Epoly__cmul__def,axiom,(( ! [V0c:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V0c))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & ( ! [V1c:tp__ty_2Erealax_2Ereal] : ( ! [V2h:tp__ty_2Erealax_2Ereal] : ( ! [V3t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1c))@(inj__ty_2Erealax_2Ereal @ V2h)))@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t)))))))))).
thf(ax_thm_2Epoly_2Epoly__neg__def,axiom,(c_2Epoly_2Epoly__neg = (ap@c_2Epoly_2E_23_23@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(ax_thm_2Epoly_2Epoly__mul__def,axiom,(( ! [V0l2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l2))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & ( ! [V1h:tp__ty_2Erealax_2Ereal] : ( ! [V2t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V3l2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2)))@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3l2)))))))))))).
thf(ax_thm_2Epoly_2Epoly__exp__def,axiom,(( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))) & ( ! [V1p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(inj__ty_2Enum_2Enum @ V2n))))))))).
thf(ax_thm_2Epoly_2Epoly__diff__aux__def,axiom,(( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V0n))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2h:tp__ty_2Erealax_2Ereal] : ( ! [V3t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Erealax_2Ereal @ V2h)))@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t)))))))))).
thf(ax_thm_2Epoly_2Epoly__diff__def,axiom,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(c_2Elist_2ETL@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l)))))))).
thf(conj_thm_2Epoly_2EPOLY__ADD__CLAUSES,lemma,( ! [V0p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2h1:tp__ty_2Erealax_2Ereal] : ( ! [V3t1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V4h2:tp__ty_2Erealax_2Ereal] : ( ! [V5t2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2))) = V0p2) & (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p1))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = V1p1) & ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2h1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t1)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V4h2))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V5t2)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V2h1))@(inj__ty_2Erealax_2Ereal @ V4h2)))@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V5t2)))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__CMUL__CLAUSES,lemma,( ! [V0c:tp__ty_2Erealax_2Ereal] : ( ! [V1h:tp__ty_2Erealax_2Ereal] : ( ! [V2t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V0c))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V0c))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0c))@(inj__ty_2Erealax_2Ereal @ V1h)))@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V0c))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))))))))).
thf(conj_thm_2Epoly_2EPOLY__NEG__CLAUSES,lemma,( ! [V0h:tp__ty_2Erealax_2Ereal] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Epoly__neg@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Epoly__neg@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0h)))@(ap@c_2Epoly_2Epoly__neg@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t))))))))).
thf(conj_thm_2Epoly_2EPOLY__MUL__CLAUSES,lemma,( ! [V0p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1h1:tp__ty_2Erealax_2Ereal] : ( ! [V2k1:tp__ty_2Erealax_2Ereal] : ( ! [V3t1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h1))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1h1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2)))) & ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h1))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2k1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t1))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1h1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2k1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3t1)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p2))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__CLAUSES,lemma,( ! [V0c:tp__ty_2Erealax_2Ereal] : ( ! [V1h:tp__ty_2Erealax_2Ereal] : ( ! [V2t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Ediff@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & (((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Ediff@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0c))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Ediff@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__diff__aux@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2t)))))))))).
thf(conj_thm_2Epoly_2EPOLY__ADD,lemma,( ! [V0p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)))@(inj__ty_2Erealax_2Ereal @ V2x))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__ty_2Erealax_2Ereal @ V2x)))@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2))@(inj__ty_2Erealax_2Ereal @ V2x))))))))).
thf(conj_thm_2Epoly_2EPOLY__CMUL,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1c:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(inj__ty_2Erealax_2Ereal @ V2x))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1c))@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V2x))))))))).
thf(conj_thm_2Epoly_2EPOLY__NEG,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Epoly__neg@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(inj__ty_2Erealax_2Ereal @ V1x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Erealax_2Ereal__neg@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1x)))))))).
thf(conj_thm_2Epoly_2EPOLY__MUL,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p2)))@(inj__ty_2Erealax_2Ereal @ V0x))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p1))@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p2))@(inj__ty_2Erealax_2Ereal @ V0x))))))))).
thf(conj_thm_2Epoly_2EPOLY__EXP,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Erealax_2Ereal @ V2x))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Epow@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V2x)))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__LEMMA,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Elim_2Ediffl@(lam@ty_2Erealax_2Ereal@(^ [V3x:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2Epow@V3x)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l))@V3x)))))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V2x))@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l)))@(inj__ty_2Erealax_2Ereal @ V2x))))@(inj__ty_2Erealax_2Ereal @ V2x))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Elim_2Ediffl@(lam@ty_2Erealax_2Ereal@(^ [V2x:$i] : (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l))@V2x))))@(ap@(ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l)))@(inj__ty_2Erealax_2Ereal @ V1x)))@(inj__ty_2Erealax_2Ereal @ V1x)))))).
thf(conj_thm_2Epoly_2EPOLY__DIFFERENTIABLE,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Elim_2Edifferentiable@(lam@ty_2Erealax_2Ereal@(^ [V2x:$i] : (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l))@V2x))))@(inj__ty_2Erealax_2Ereal @ V1x)))))).
thf(conj_thm_2Epoly_2EPOLY__CONT,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Elim_2Econtl@(lam@ty_2Erealax_2Ereal@(^ [V2x:$i] : (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0l))@V2x))))@(inj__ty_2Erealax_2Ereal @ V1x)))))).
thf(conj_thm_2Epoly_2EPOLY__IVT__POS,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (p@(ap@(ap@c_2Ereal_2Ereal__gt@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => (? [V3x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3x))) & ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V3x))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V3x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))))).
thf(conj_thm_2Epoly_2EPOLY__IVT__NEG,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((p@(ap@(ap@c_2Ereal_2Ereal__gt@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => (? [V3x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3x))) & ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V3x))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V3x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))))).
thf(conj_thm_2Epoly_2EPOLY__MVT,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) => (? [V3x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3x))) & ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V3x))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1a)))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(inj__ty_2Erealax_2Ereal @ V3x))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__ADD__RZERO,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))).
thf(conj_thm_2Epoly_2EPOLY__MUL__ASSOC,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))))))).
thf(conj_thm_2Epoly_2EPOLY__EXP__ADD,lemma,( ! [V0d:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0d)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p))@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p))@(inj__ty_2Enum_2Enum @ V0d))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__AUX__ADD,lemma,( ! [V0p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V2n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1)))@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V2n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__AUX__CMUL,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1c:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V2n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__AUX__NEG,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Epoly_2Epoly__neg@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) = (ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Epoly__neg@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V1n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__AUX__MUL__LEMMA,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(inj__ty_2Enum_2Enum @ V1n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__ADD,lemma,( ! [V0p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1)))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__CMUL,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1c:tp__ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2E_23_23@(inj__ty_2Erealax_2Ereal @ V1c))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__NEG,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@c_2Epoly_2Epoly__neg@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) = (ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Epoly__neg@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__MUL__LEMMA,lemma,( ! [V0t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1h:tp__ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0t)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0t))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0t))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__MUL,lemma,( ! [V0p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2))))@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__EXP,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@c_2Epoly_2E_23_23@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V1n))))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__EXP__PRIME,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n))))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2E_23_23@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n))))@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__ty_2Enum_2Enum @ V0n)))))))).
thf(conj_thm_2Epoly_2EPOLY__LINEAR__REM,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2h:tp__ty_2Erealax_2Ereal] : (? [V3q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (? [V4r:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V4r))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3q))))))))))).
thf(conj_thm_2Epoly_2EPOLY__LINEAR__DIVIDES,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(inj__ty_2Erealax_2Ereal @ V0a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> ((V1p = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) | (? [V2q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (V1p = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))))))))).
thf(conj_thm_2Epoly_2EPOLY__LENGTH__MUL,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@ty_2Erealax_2Ereal)@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(c_2Elist_2ELENGTH@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)))))))).
thf(conj_thm_2Epoly_2EPOLY__ROOTS__INDEX__LEMMA,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))) = V0n)) => (? [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(inj__ty_2Erealax_2Ereal @ V3x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => (? [V4m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4m))@(inj__ty_2Enum_2Enum @ V0n))) & (V3x = (surj__ty_2Erealax_2Ereal @ (ap@V2i@(inj__ty_2Enum_2Enum @ V4m)))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__ROOTS__INDEX__LENGTH,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) => (? [V1i:$i] : ((mem@V1i@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V2x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => (? [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3n))@(ap@(c_2Elist_2ELENGTH@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) & (V2x = (surj__ty_2Erealax_2Ereal @ (ap@V1i@(inj__ty_2Enum_2Enum @ V3n))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__ROOTS__FINITE__LEMMA,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) => (? [V1N:tp__ty_2Enum_2Enum] : (? [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V3x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => (? [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V1N))) & (V3x = (surj__ty_2Erealax_2Ereal @ (ap@V2i@(inj__ty_2Enum_2Enum @ V4n)))))))))))))).
thf(conj_thm_2Epoly_2EFINITE__LEMMA,lemma,( ! [V0i:$i] : ((mem@V0i@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1N:tp__ty_2Enum_2Enum] : ( ! [V2P:$i] : ((mem@V2P@(arr@ty_2Erealax_2Ereal@bool)) => (( ! [V3x:tp__ty_2Erealax_2Ereal] : ((p@(ap@V2P@(inj__ty_2Erealax_2Ereal @ V3x))) => (? [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V1N))) & (V3x = (surj__ty_2Erealax_2Ereal @ (ap@V0i@(inj__ty_2Enum_2Enum @ V4n)))))))) => (? [V5a:tp__ty_2Erealax_2Ereal] : ( ! [V6x:tp__ty_2Erealax_2Ereal] : ((p@(ap@V2P@(inj__ty_2Erealax_2Ereal @ V6x))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V5a))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__ROOTS__FINITE,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) <=> (? [V1N:tp__ty_2Enum_2Enum] : (? [V2i:$i] : ((mem@V2i@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V3x))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => (? [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V1N))) & (V3x = (surj__ty_2Erealax_2Ereal @ (ap@V2i@(inj__ty_2Enum_2Enum @ V4n)))))))))))))).
thf(conj_thm_2Epoly_2EPOLY__ENTIRE__LEMMA,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & (~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))) => (~~ ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))))).
thf(conj_thm_2Epoly_2EPOLY__ENTIRE,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) <=> (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) | ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))))).
thf(conj_thm_2Epoly_2EPOLY__MUL__LCANCEL,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))) <=> (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) | ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)) = (ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r))))))))).
thf(conj_thm_2Epoly_2EPOLY__EXP__EQ__0,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V1n))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) <=> (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & (~~ (V1n = fo__c_2Enum_2E0))))))).
thf(conj_thm_2Epoly_2EPOLY__PRIME__EQ__0,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : (~~ ((ap@c_2Epoly_2Epoly@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))).
thf(conj_thm_2Epoly_2EPOLY__EXP__PRIME__EQ__0,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (~~ ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__ty_2Enum_2Enum @ V1n))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))))).
thf(conj_thm_2Epoly_2EPOLY__ZERO__LEMMA,lemma,( ! [V0h:tp__ty_2Erealax_2Ereal] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) => ((V0h = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))))).
thf(conj_thm_2Epoly_2EPOLY__ZERO,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) <=> (p@(ap@(ap@(c_2Elist_2EEVERY@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V1c:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@V1c)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__AUX__ISZERO,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Elist_2EEVERY@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V2c:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@V2c)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))@(ap@(ap@c_2Epoly_2Epoly__diff__aux@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) <=> (p@(ap@(ap@(c_2Elist_2EEVERY@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V3c:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@V3c)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__ISZERO,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) => (? [V1h:tp__ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1h))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__ZERO,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) => ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))).
thf(conj_thm_2Epoly_2EPOLY__DIFF__WELLDEF,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) => ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)))))))).
thf(ax_thm_2Epoly_2Epoly__divides,axiom,( ! [V0p1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1p2:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2))) <=> (? [V2q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p2)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p1))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q))))))))).
thf(conj_thm_2Epoly_2EPOLY__PRIMES,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))) <=> ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))) | (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__REFL,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__TRANS,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) & (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__EXP,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V2n))))))))).
thf(conj_thm_2Epoly_2EPOLY__EXP__DIVIDES,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V3n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3n)))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Enum_2Enum @ V2m)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__ADD,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) & (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r))))))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__SUB,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) & (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r))))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__SUB2,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r))) & (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(ap@(ap@c_2Epoly_2Epoly__add@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2r))))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q)))))))).
thf(conj_thm_2Epoly_2EPOLY__DIVIDES__ZERO,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) => (p@(ap@(ap@c_2Epoly_2Epoly__divides@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))).
thf(conj_thm_2Epoly_2EPOLY__ORDER__EXISTS,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1d:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@ty_2Erealax_2Ereal)@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p))) = V1d) & (~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))) => (? [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__ty_2Enum_2Enum @ V3n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p))) & (~~ (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2p))))))))))).
thf(conj_thm_2Epoly_2EPOLY__ORDER,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) => (p@(ap@(c_2Ebool_2E_3F_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@V2n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@V2n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))))))).
thf(ax_thm_2Epoly_2Epoly__order,axiom,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Emin_2E_40@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@V2n))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@V2n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p)))))))))))).
thf(conj_thm_2Epoly_2EORDER,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__ty_2Enum_2Enum @ V2n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) & (~~ (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))) <=> ((V2n = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))) & (~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))))))))).
thf(conj_thm_2Epoly_2EORDER__THM,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) => ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) & (~~ (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))))).
thf(conj_thm_2Epoly_2EORDER__UNIQUE,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : (((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__ty_2Enum_2Enum @ V2n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) & (~~ (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))) => (V2n = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))))).
thf(conj_thm_2Epoly_2EORDER__POLY,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2a:tp__ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))))))))).
thf(conj_thm_2Epoly_2EORDER__ROOT,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) | (~~ ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = fo__c_2Enum_2E0))))))).
thf(conj_thm_2Epoly_2EORDER__DIVIDES,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__ty_2Enum_2Enum @ V2n)))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) <=> (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) | (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))))).
thf(conj_thm_2Epoly_2EORDER__DECOMP,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) => (? [V2q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@c_2Epoly_2Epoly__exp@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))) & (~~ (p@(ap@(ap@c_2Epoly_2Epoly__divides@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))))))))).
thf(conj_thm_2Epoly_2EORDER__MUL,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((~~ ((ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1p)))@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))))))))).
thf(conj_thm_2Epoly_2EORDER__DIFF,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : (((~~ ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & (~~ ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = fo__c_2Enum_2E0))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))))).
thf(conj_thm_2Epoly_2EPOLY__SQUAREFREE__DECOMP__ORDER,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2d:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V3e:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V4r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V5s:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((~~ ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2d)))) & (((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3e))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2d)))) & ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2d)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V4r))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V5s))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))))) => ( ! [V6a:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V6a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V6a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))).
thf(ax_thm_2Epoly_2Ersquarefree,axiom,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((p@(ap@c_2Epoly_2Ersquarefree@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) <=> ((~ ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & ( ! [V1a:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = fo__c_2Enum_2E0) | ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epoly_2Epoly__order@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(conj_thm_2Epoly_2ERSQUAREFREE__ROOTS,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((p@(ap@c_2Epoly_2Ersquarefree@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) <=> ( ! [V1a:tp__ty_2Erealax_2Ereal] : (~~ (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(inj__ty_2Erealax_2Ereal @ V1a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Epoly_2ERSQUAREFREE__DECOMP,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1a:tp__ty_2Erealax_2Ereal] : (((p@(ap@c_2Epoly_2Ersquarefree@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) & ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V1a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => (? [V2q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1a)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q)))) & (~~ ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2q))@(inj__ty_2Erealax_2Ereal @ V1a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))).
thf(conj_thm_2Epoly_2EPOLY__SQUAREFREE__DECOMP,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V1q:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V2d:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V3e:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V4r:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [V5s:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((~~ ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))) & (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2d)))) & (((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V3e))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2d)))) & ((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V2d)) = (ap@c_2Epoly_2Epoly@(ap@(ap@c_2Epoly_2Epoly__add@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V4r))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))@(ap@(ap@c_2Epoly_2Epoly__mul@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V5s))@(ap@c_2Epoly_2Ediff@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))))))) => ((p@(ap@c_2Epoly_2Ersquarefree@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))) & ( ! [V6a:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1q))@(inj__ty_2Erealax_2Ereal @ V6a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))@(inj__ty_2Erealax_2Ereal @ V6a))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))))))).
thf(ax_thm_2Epoly_2Enormalize,axiom,(((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Enormalize@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (c_2Elist_2ENIL@ty_2Erealax_2Ereal))) & ( ! [V0h:tp__ty_2Erealax_2Ereal] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@c_2Epoly_2Enormalize@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0h))@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t)))) = (surj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(ap@c_2Epoly_2Enormalize@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t)))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Erealax_2Ereal))@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0h))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0h))@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))))@(ap@(ap@(c_2Elist_2ECONS@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0h))@(ap@c_2Epoly_2Enormalize@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V1t)))))))))).
thf(conj_thm_2Epoly_2EPOLY__NORMALIZE,lemma,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((ap@c_2Epoly_2Epoly@(ap@c_2Epoly_2Enormalize@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))))).
thf(ax_thm_2Epoly_2Edegree,axiom,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ((surj__ty_2Enum_2Enum @ (ap@c_2Epoly_2Edegree@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@(c_2Elist_2ELENGTH@ty_2Erealax_2Ereal)@(ap@c_2Epoly_2Enormalize@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)))))))).
thf(conj_thm_2Epoly_2EDEGREE__ZERO,conjecture,( ! [V0p:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (((ap@c_2Epoly_2Epoly@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p)) = (ap@c_2Epoly_2Epoly@(c_2Elist_2ENIL@ty_2Erealax_2Ereal))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Epoly_2Edegree@(inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal @ V0p))) = fo__c_2Enum_2E0)))).
