include('Axioms/lim_2.ax').
tff(stp_c_ty_2Elist_2Elist_ty_2Erealax_2Ereal,type,(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal : $tType)).
tff(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)).
tff(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)).
tff(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))).
tff(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))))).
tff(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)))))).
tff(tp_c_2Epoly_2E_23_23,type,(c_2Epoly_2E_23_23:$i)).
tff(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))))).
tff(tp_c_2Epoly_2Edegree,type,(c_2Epoly_2Edegree:$i)).
tff(mem_c_2Epoly_2Edegree,axiom,mem(c_2Epoly_2Edegree,arr(ty_2Elist_2Elist(ty_2Erealax_2Ereal),ty_2Enum_2Enum))).
tff(stp_fo_c_2Epoly_2Edegree,type,(fo__c_2Epoly_2Edegree:(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal) > tp__ty_2Enum_2Enum)).
tff(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))))).
tff(tp_c_2Epoly_2Ediff,type,(c_2Epoly_2Ediff:$i)).
tff(mem_c_2Epoly_2Ediff,axiom,mem(c_2Epoly_2Ediff,arr(ty_2Elist_2Elist(ty_2Erealax_2Ereal),ty_2Elist_2Elist(ty_2Erealax_2Ereal)))).
tff(tp_c_2Epoly_2Enormalize,type,(c_2Epoly_2Enormalize:$i)).
tff(mem_c_2Epoly_2Enormalize,axiom,mem(c_2Epoly_2Enormalize,arr(ty_2Elist_2Elist(ty_2Erealax_2Ereal),ty_2Elist_2Elist(ty_2Erealax_2Ereal)))).
tff(tp_c_2Epoly_2Epoly,type,(c_2Epoly_2Epoly:$i)).
tff(mem_c_2Epoly_2Epoly,axiom,mem(c_2Epoly_2Epoly,arr(ty_2Elist_2Elist(ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(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)).
tff(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)))))).
tff(tp_c_2Epoly_2Epoly__add,type,(c_2Epoly_2Epoly__add:$i)).
tff(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))))).
tff(tp_c_2Epoly_2Epoly__diff__aux,type,(c_2Epoly_2Epoly__diff__aux:$i)).
tff(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))))).
tff(tp_c_2Epoly_2Epoly__divides,type,(c_2Epoly_2Epoly__divides:$i)).
tff(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)))).
tff(stp_fo_c_2Epoly_2Epoly__divides,type,(fo__c_2Epoly_2Epoly__divides:(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal * tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal) > tp__o)).
tff(stp_eq_fo_c_2Epoly_2Epoly__divides,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (inj__o(fo__c_2Epoly_2Epoly__divides(X0,X1)) = ap(ap(c_2Epoly_2Epoly__divides,inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal(X0)),inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Epoly_2Epoly__exp,type,(c_2Epoly_2Epoly__exp:$i)).
tff(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))))).
tff(tp_c_2Epoly_2Epoly__mul,type,(c_2Epoly_2Epoly__mul:$i)).
tff(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))))).
tff(tp_c_2Epoly_2Epoly__neg,type,(c_2Epoly_2Epoly__neg:$i)).
tff(mem_c_2Epoly_2Epoly__neg,axiom,mem(c_2Epoly_2Epoly__neg,arr(ty_2Elist_2Elist(ty_2Erealax_2Ereal),ty_2Elist_2Elist(ty_2Erealax_2Ereal)))).
tff(tp_c_2Epoly_2Epoly__order,type,(c_2Epoly_2Epoly__order:$i)).
tff(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)))).
tff(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)).
tff(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)))))).
tff(tp_c_2Epoly_2Ersquarefree,type,(c_2Epoly_2Ersquarefree:$i)).
tff(mem_c_2Epoly_2Ersquarefree,axiom,mem(c_2Epoly_2Ersquarefree,arr(ty_2Elist_2Elist(ty_2Erealax_2Ereal),bool))).
tff(stp_fo_c_2Epoly_2Ersquarefree,type,(fo__c_2Epoly_2Ersquarefree:(tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal) > tp__o)).
tff(stp_eq_fo_c_2Epoly_2Ersquarefree,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal] : (inj__o(fo__c_2Epoly_2Ersquarefree(X0)) = ap(c_2Epoly_2Ersquarefree,inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal(X0))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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,f2921(V1n,V0l)),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)))))))).
tff(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,f2922(V0l)),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))))))).
tff(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,f2922(V0l)),inj__ty_2Erealax_2Ereal(V1x))))))).
tff(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,f2922(V0l)),inj__ty_2Erealax_2Ereal(V1x))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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)))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))).
tff(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)))))))).
tff(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))))))))).
tff(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),f2923),inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal(V0p))))))).
tff(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),f2924),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),f2925),inj__c_ty_2Elist_2Elist_ty_2Erealax_2Ereal(V0p)))))))).
tff(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))))))))).
tff(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))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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),f2926(V0p,V1a)))))))).
tff(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),f2927(V1p,V0a))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))).
tff(conj_thm_2Epoly_2ERSQUAREFREE__ROOTS,conjecture,(( ! [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))))))))))).
