include('Axioms/rat^2.ax').
thf(tp_c_2Eseq_2E_2D_2D_3E,type,(c_2Eseq_2E_2D_2D_3E:$i)).
thf(mem_c_2Eseq_2E_2D_2D_3E,axiom,(mem@c_2Eseq_2E_2D_2D_3E@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Erealax_2Ereal@bool)))).
thf(tp_c_2Eseq_2Ecauchy,type,(c_2Eseq_2Ecauchy:$i)).
thf(mem_c_2Eseq_2Ecauchy,axiom,(mem@c_2Eseq_2Ecauchy@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@bool))).
thf(tp_c_2Eseq_2Econvergent,type,(c_2Eseq_2Econvergent:$i)).
thf(mem_c_2Eseq_2Econvergent,axiom,(mem@c_2Eseq_2Econvergent@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@bool))).
thf(tp_c_2Eseq_2Elim,type,(c_2Eseq_2Elim:$i)).
thf(mem_c_2Eseq_2Elim,axiom,(mem@c_2Eseq_2Elim@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal))).
thf(tp_c_2Eseq_2Emono,type,(c_2Eseq_2Emono:$i)).
thf(mem_c_2Eseq_2Emono,axiom,(mem@c_2Eseq_2Emono@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@bool))).
thf(tp_c_2Eseq_2Emono__decreasing,type,(c_2Eseq_2Emono__decreasing:$i)).
thf(mem_c_2Eseq_2Emono__decreasing,axiom,(mem@c_2Eseq_2Emono__decreasing@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@bool))).
thf(tp_c_2Eseq_2Emono__increasing,type,(c_2Eseq_2Emono__increasing:$i)).
thf(mem_c_2Eseq_2Emono__increasing,axiom,(mem@c_2Eseq_2Emono__increasing@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@bool))).
thf(tp_c_2Eseq_2Esubseq,type,(c_2Eseq_2Esubseq:$i)).
thf(mem_c_2Eseq_2Esubseq,axiom,(mem@c_2Eseq_2Esubseq@(arr@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool))).
thf(tp_c_2Eseq_2Esuminf,type,(c_2Eseq_2Esuminf:$i)).
thf(mem_c_2Eseq_2Esuminf,axiom,(mem@c_2Eseq_2Esuminf@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal))).
thf(tp_c_2Eseq_2Esummable,type,(c_2Eseq_2Esummable:$i)).
thf(mem_c_2Eseq_2Esummable,axiom,(mem@c_2Eseq_2Esummable@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@bool))).
thf(tp_c_2Eseq_2Esums,type,(c_2Eseq_2Esums:$i)).
thf(mem_c_2Eseq_2Esums,axiom,(mem@c_2Eseq_2Esums@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Erealax_2Ereal@bool)))).
thf(ax_thm_2Eseq_2Etends__num__real,axiom,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) <=> (p@(ap@(ap@(ap@(c_2Enets_2Etends@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Etopology_2Etopology@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@(ap@(c_2Emetric_2Emtop@ty_2Erealax_2Ereal)@c_2Emetric_2Emr1))@c_2Earithmetic_2E_3E_3D)))))))).
thf(conj_thm_2Eseq_2ESEQ,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) <=> ( ! [V2e:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V2e))) => (? [V3N:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V3N))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0x@(inj__ty_2Enum_2Enum @ V4n)))@(inj__ty_2Erealax_2Ereal @ V1x0))))@(inj__ty_2Erealax_2Ereal @ V2e))))))))))))).
thf(conj_thm_2Eseq_2ESEQ__CONST,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V1x:$i] : (inj__ty_2Erealax_2Ereal @ V0k))))@(inj__ty_2Erealax_2Ereal @ V0k))))).
thf(conj_thm_2Eseq_2ESEQ__ADD,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : ((mem@V2y@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2y)@(inj__ty_2Erealax_2Ereal @ V3y0)))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0x@V4n))@(ap@V2y@V4n)))))@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V3y0)))))))))))).
thf(conj_thm_2Eseq_2ESEQ__MUL,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : ((mem@V2y@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2y)@(inj__ty_2Erealax_2Ereal @ V3y0)))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@V0x@V4n))@(ap@V2y@V4n)))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V3y0)))))))))))).
thf(conj_thm_2Eseq_2ESEQ__NEG,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) <=> (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@V0x@V2n)))))@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1x0))))))))).
thf(conj_thm_2Eseq_2ESEQ__INV,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & (~~ (V1x0 = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Erealax_2Einv@(ap@V0x@V2n)))))@(ap@c_2Erealax_2Einv@(inj__ty_2Erealax_2Ereal @ V1x0))))))))).
thf(conj_thm_2Eseq_2ESEQ__SUB,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : ((mem@V2y@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2y)@(inj__ty_2Erealax_2Ereal @ V3y0)))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0x@V4n))@(ap@V2y@V4n)))))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V3y0)))))))))))).
thf(conj_thm_2Eseq_2ESEQ__DIV,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : ((mem@V2y@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2y)@(inj__ty_2Erealax_2Ereal @ V3y0))) & (~~ (V3y0 = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Ereal_2E_2F@(ap@V0x@V4n))@(ap@V2y@V4n)))))@(ap@(ap@c_2Ereal_2E_2F@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V3y0)))))))))))).
thf(conj_thm_2Eseq_2ESEQ__UNIQ,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x1:tp__ty_2Erealax_2Ereal] : ( ! [V2x2:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V1x1))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0x)@(inj__ty_2Erealax_2Ereal @ V2x2)))) => (V1x1 = V2x2))))))).
thf(ax_thm_2Eseq_2Econvergent,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Econvergent@V0f)) <=> (? [V1l:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1l)))))))).
thf(ax_thm_2Eseq_2Ecauchy,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Ecauchy@V0f)) <=> ( ! [V1e:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V1e))) => (? [V2N:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V2N))) & (p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V2N)))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0f@(inj__ty_2Enum_2Enum @ V3m)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V4n)))))@(inj__ty_2Erealax_2Ereal @ V1e))))))))))))).
thf(ax_thm_2Eseq_2Elim,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((surj__ty_2Erealax_2Ereal @ (ap@c_2Eseq_2Elim@V0f)) = (surj__ty_2Erealax_2Ereal @ (ap@(c_2Emin_2E_40@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V1l:$i] : (ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@V1l))))))))).
thf(conj_thm_2Eseq_2ESEQ__LIM,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Econvergent@V0f)) <=> (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(ap@c_2Eseq_2Elim@V0f))))))).
thf(ax_thm_2Eseq_2Esubseq,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@c_2Eseq_2Esubseq@V0f)) <=> ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@V0f@(inj__ty_2Enum_2Enum @ V1m)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))))))))).
thf(conj_thm_2Eseq_2ESUBSEQ__SUC,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@c_2Eseq_2Esubseq@V0f)) <=> ( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n)))@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(ax_thm_2Eseq_2Emono,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Emono@V0f)) <=> (( ! [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_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V1m)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))))) | ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V4n))) => (p@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@V0f@(inj__ty_2Enum_2Enum @ V3m)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V4n)))))))))))).
thf(conj_thm_2Eseq_2EMONO__SUC,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Emono@V0f)) <=> (( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))) | ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))))))))).
thf(conj_thm_2Eseq_2EMAX__LEMMA,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1N:tp__ty_2Enum_2Enum] : (? [V2k:tp__ty_2Erealax_2Ereal] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V1N))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@V0s@(inj__ty_2Enum_2Enum @ V3n))))@(inj__ty_2Erealax_2Ereal @ V2k)))))))))).
thf(conj_thm_2Eseq_2ESEQ__BOUNDED,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0s)) <=> (? [V1k:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@V0s@(inj__ty_2Enum_2Enum @ V2n))))@(inj__ty_2Erealax_2Ereal @ V1k))))))))).
thf(conj_thm_2Eseq_2ESEQ__BOUNDED__2,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1k:tp__ty_2Erealax_2Ereal] : ( ! [V2k_27:tp__ty_2Erealax_2Ereal] : (( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1k))@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(inj__ty_2Erealax_2Ereal @ V2k_27))))) => (p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0f)))))))).
thf(conj_thm_2Eseq_2ESEQ__CBOUNDED,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Ecauchy@V0f)) => (p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0f)))))).
thf(conj_thm_2Eseq_2ESEQ__ICONV,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0f)) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@V0f@(inj__ty_2Enum_2Enum @ V1m)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))))))) => (p@(ap@c_2Eseq_2Econvergent@V0f)))))).
thf(conj_thm_2Eseq_2ESEQ__NEG__CONV,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Econvergent@V0f)) <=> (p@(ap@c_2Eseq_2Econvergent@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@V0f@V1n)))))))))).
thf(conj_thm_2Eseq_2ESEQ__NEG__BOUNDED,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@V0f@V1n)))))) <=> (p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0f)))))).
thf(conj_thm_2Eseq_2ESEQ__BCONV,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0f)) & (p@(ap@c_2Eseq_2Emono@V0f))) => (p@(ap@c_2Eseq_2Econvergent@V0f)))))).
thf(conj_thm_2Eseq_2ESEQ__MONOSUB,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (? [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) & ((p@(ap@c_2Eseq_2Esubseq@V1f)) & (p@(ap@c_2Eseq_2Emono@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@V0s@(ap@V1f@V2n)))))))))))).
thf(conj_thm_2Eseq_2ESEQ__SBOUNDED,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@V0s)) => (p@(ap@(ap@(c_2Enets_2Ebounded@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Emetric_2Emetric@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))@c_2Emetric_2Emr1)@c_2Earithmetic_2E_3E_3D))@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@V0s@(ap@V1f@V2n)))))))))))).
thf(conj_thm_2Eseq_2ESEQ__SUBLE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@c_2Eseq_2Esubseq@V0f)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Eseq_2ESEQ__DIRECT,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@c_2Eseq_2Esubseq@V0f)) => ( ! [V1N1:tp__ty_2Enum_2Enum] : ( ! [V2N2:tp__ty_2Enum_2Enum] : (? [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V1N1))) & (p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(inj__ty_2Enum_2Enum @ V2N2))))))))))).
thf(conj_thm_2Eseq_2ESEQ__CAUCHY,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Ecauchy@V0f)) <=> (p@(ap@c_2Eseq_2Econvergent@V0f)))))).
thf(conj_thm_2Eseq_2ESEQ__LE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2l:tp__ty_2Erealax_2Ereal] : ( ! [V3m:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V2l))) & ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V1g)@(inj__ty_2Erealax_2Ereal @ V3m))) & (? [V4N:tp__ty_2Enum_2Enum] : ( ! [V5n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V5n))@(inj__ty_2Enum_2Enum @ V4N))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V5n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V5n))))))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2l))@(inj__ty_2Erealax_2Ereal @ V3m))))))))))).
thf(conj_thm_2Eseq_2ESEQ__SUC,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1l))) <=> (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@V0f@(ap@c_2Enum_2ESUC@V2n)))))@(inj__ty_2Erealax_2Ereal @ V1l)))))))).
thf(conj_thm_2Eseq_2ESEQ__ABS,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V1n)))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Eseq_2ESEQ__ABS__IMP,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1l))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V2n)))))@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V1l))))))))).
thf(conj_thm_2Eseq_2ESEQ__INV0,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (( ! [V1y:tp__ty_2Erealax_2Ereal] : (? [V2N:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2N))) => (p@(ap@(ap@c_2Ereal_2Ereal__gt@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(inj__ty_2Erealax_2Ereal @ V1y))))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@c_2Erealax_2Einv@(ap@V0f@V4n)))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Eseq_2ESEQ__POWER__ABS,lemma,( ! [V0c:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V0c)))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V0c)))@V1n))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Eseq_2ESEQ__POWER,lemma,( ! [V0c:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V0c)))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0c))@V1n))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Eseq_2ENEST__LEMMA,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))) & (( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V1g@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))@(ap@V1g@(inj__ty_2Enum_2Enum @ V3n))))) & ( ! [V4n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V4n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V4n))))))) => (? [V5l:tp__ty_2Erealax_2Ereal] : (? [V6m:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V5l))@(inj__ty_2Erealax_2Ereal @ V6m))) & ((( ! [V7n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V7n)))@(inj__ty_2Erealax_2Ereal @ V5l)))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V5l)))) & (( ! [V8n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6m))@(ap@V1g@(inj__ty_2Enum_2Enum @ V8n))))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V1g)@(inj__ty_2Erealax_2Ereal @ V6m)))))))))))))).
thf(conj_thm_2Eseq_2ENEST__LEMMA__UNIQ,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__ge@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))) & (( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V1g@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))@(ap@V1g@(inj__ty_2Enum_2Enum @ V3n))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V4n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V4n))))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V5n:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0f@V5n))@(ap@V1g@V5n)))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))) => (? [V6l:tp__ty_2Erealax_2Ereal] : ((( ! [V7n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V7n)))@(inj__ty_2Erealax_2Ereal @ V6l)))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V6l)))) & (( ! [V8n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6l))@(ap@V1g@(inj__ty_2Enum_2Enum @ V8n))))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V1g)@(inj__ty_2Erealax_2Ereal @ V6l)))))))))))).
thf(stp_c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal,type,(tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal,type,(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal : (tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal,type,(surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal : ($i > tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (mem @ (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X) @ (ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => (X = (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X)))))).
thf(conj_thm_2Eseq_2EBOLZANO__LEMMA,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@bool)) => ((( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3c:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c))) & ((p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))) & (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c))))))) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3c)))))))) & ( ! [V4x:tp__ty_2Erealax_2Ereal] : (? [V5d:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V5d))) & ( ! [V6a:tp__ty_2Erealax_2Ereal] : ( ! [V7b:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6a))@(inj__ty_2Erealax_2Ereal @ V4x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V4x))@(inj__ty_2Erealax_2Ereal @ V7b))) & (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V7b))@(inj__ty_2Erealax_2Ereal @ V6a)))@(inj__ty_2Erealax_2Ereal @ V5d))))) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V6a))@(inj__ty_2Erealax_2Ereal @ V7b))))))))))) => ( ! [V8a:tp__ty_2Erealax_2Ereal] : ( ! [V9b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V8a))@(inj__ty_2Erealax_2Ereal @ V9b))) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V8a))@(inj__ty_2Erealax_2Ereal @ V9b))))))))))).
thf(ax_thm_2Eseq_2Esums,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1s:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0f)@(inj__ty_2Erealax_2Ereal @ V1s))) <=> (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V2n))@V0f))))@(inj__ty_2Erealax_2Ereal @ V1s)))))))).
thf(ax_thm_2Eseq_2Esummable,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@V0f)) <=> (? [V1s:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2Esums@V0f)@(inj__ty_2Erealax_2Ereal @ V1s)))))))).
thf(ax_thm_2Eseq_2Esuminf,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((surj__ty_2Erealax_2Ereal @ (ap@c_2Eseq_2Esuminf@V0f)) = (surj__ty_2Erealax_2Ereal @ (ap@(c_2Emin_2E_40@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V1s:$i] : (ap@(ap@c_2Eseq_2Esums@V0f)@V1s))))))))).
thf(conj_thm_2Eseq_2ESUM__SUMMABLE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0f)@(inj__ty_2Erealax_2Ereal @ V1l))) => (p@(ap@c_2Eseq_2Esummable@V0f))))))).
thf(conj_thm_2Eseq_2ESUMMABLE__SUM,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@V0f)) => (p@(ap@(ap@c_2Eseq_2Esums@V0f)@(ap@c_2Eseq_2Esuminf@V0f))))))).
thf(conj_thm_2Eseq_2ESUM__UNIQ,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0f)@(inj__ty_2Erealax_2Ereal @ V1x))) => (V1x = (surj__ty_2Erealax_2Ereal @ (ap@c_2Eseq_2Esuminf@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__0,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2m))) => ((surj__ty_2Erealax_2Ereal @ (ap@V0f@(inj__ty_2Enum_2Enum @ V2m))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => (p@(ap@(ap@c_2Eseq_2Esums@V0f)@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__POS__LE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (((p@(ap@c_2Eseq_2Esummable@V0f)) & ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2m))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2m))))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))@V0f))@(ap@c_2Eseq_2Esuminf@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__POS__LT,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (((p@(ap@c_2Eseq_2Esummable@V0f)) & ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2m))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2m))))))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))@V0f))@(ap@c_2Eseq_2Esuminf@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__GROUP,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1k:tp__ty_2Enum_2Enum] : (((p@(ap@c_2Eseq_2Esummable@V0f)) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1k)))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2A@V2n)@(inj__ty_2Enum_2Enum @ V1k)))@(inj__ty_2Enum_2Enum @ V1k)))@V0f))))@(ap@c_2Eseq_2Esuminf@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__PAIR,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@V0f)) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V1n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V0f))))@(ap@c_2Eseq_2Esuminf@V0f))))))).
thf(conj_thm_2Eseq_2ESER__OFFSET,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@V0f)) => ( ! [V1k:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@V0f@(ap@(ap@c_2Earithmetic_2E_2B@V2n)@(inj__ty_2Enum_2Enum @ V1k))))))@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@c_2Eseq_2Esuminf@V0f))@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1k)))@V0f))))))))).
thf(conj_thm_2Eseq_2ESER__POS__LT__PAIR,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (((p@(ap@c_2Eseq_2Esummable@V0f)) & ( ! [V2d:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2d)))))@(ap@V0f@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V2d)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))@V0f))@(ap@c_2Eseq_2Esuminf@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__ADD,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : ((mem@V2y@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2Esums@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & (p@(ap@(ap@c_2Eseq_2Esums@V2y)@(inj__ty_2Erealax_2Ereal @ V3y0)))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0x@V4n))@(ap@V2y@V4n)))))@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V3y0)))))))))))).
thf(conj_thm_2Eseq_2ESER__CMUL,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V2c))@(ap@V0x@V3n)))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V2c))@(inj__ty_2Erealax_2Ereal @ V1x0)))))))))).
thf(conj_thm_2Eseq_2ESER__NEG,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@V0x@V2n)))))@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V1x0))))))))).
thf(conj_thm_2Eseq_2ESER__SUB,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : ((mem@V2y@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2Esums@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) & (p@(ap@(ap@c_2Eseq_2Esums@V2y)@(inj__ty_2Erealax_2Ereal @ V3y0)))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0x@V4n))@(ap@V2y@V4n)))))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V3y0)))))))))))).
thf(conj_thm_2Eseq_2ESER__CDIV,lemma,( ! [V0x:$i] : ((mem@V0x@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0x)@(inj__ty_2Erealax_2Ereal @ V1x0))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@c_2Ereal_2E_2F@(ap@V0x@V3n))@(inj__ty_2Erealax_2Ereal @ V2c)))))@(ap@(ap@c_2Ereal_2E_2F@(inj__ty_2Erealax_2Ereal @ V1x0))@(inj__ty_2Erealax_2Ereal @ V2c)))))))))).
thf(conj_thm_2Eseq_2ESER__CAUCHY,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@V0f)) <=> ( ! [V1e:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V1e))) => (? [V2N:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V2N))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V4n)))@V0f)))@(inj__ty_2Erealax_2Ereal @ V1e))))))))))))).
thf(conj_thm_2Eseq_2ESER__ZERO,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@V0f)) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Eseq_2ESER__COMPAR,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((? [V2N:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2N))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n))))@(ap@V1g@(inj__ty_2Enum_2Enum @ V3n))))))) & (p@(ap@c_2Eseq_2Esummable@V1g))) => (p@(ap@c_2Eseq_2Esummable@V0f)))))))).
thf(conj_thm_2Eseq_2ESER__COMPARA,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((? [V2N:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2N))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n))))@(ap@V1g@(inj__ty_2Enum_2Enum @ V3n))))))) & (p@(ap@c_2Eseq_2Esummable@V1g))) => (p@(ap@c_2Eseq_2Esummable@(lam@ty_2Enum_2Enum@(^ [V4k:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V4k)))))))))))).
thf(conj_thm_2Eseq_2ESER__LE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V2n))))) & ((p@(ap@c_2Eseq_2Esummable@V0f)) & (p@(ap@c_2Eseq_2Esummable@V1g)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Eseq_2Esuminf@V0f))@(ap@c_2Eseq_2Esuminf@V1g))))))))).
thf(conj_thm_2Eseq_2ESER__LE2,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))@(ap@V1g@(inj__ty_2Enum_2Enum @ V2n))))) & (p@(ap@c_2Eseq_2Esummable@V1g))) => ((p@(ap@c_2Eseq_2Esummable@V0f)) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Eseq_2Esuminf@V0f))@(ap@c_2Eseq_2Esuminf@V1g)))))))))).
thf(conj_thm_2Eseq_2ESER__ACONV,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V1n)))))) => (p@(ap@c_2Eseq_2Esummable@V0f)))))).
thf(conj_thm_2Eseq_2ESER__ABS,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Esummable@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V1n)))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@c_2Eseq_2Esuminf@V0f)))@(ap@c_2Eseq_2Esuminf@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V2n))))))))))).
thf(conj_thm_2Eseq_2EGP__FINITE,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((~~ (V0x = (surj__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))))))) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V2n))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2E_2F@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Enum_2Enum @ V1n)))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))).
thf(conj_thm_2Eseq_2EGP,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n))))@(ap@c_2Erealax_2Einv@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Erealax_2Ereal @ V0x)))))))).
thf(conj_thm_2Eseq_2EABS__NEG__LEMMA,lemma,( ! [V0c:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0c))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V1x)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0c))@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V2y))))) => (V1x = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Eseq_2ESER__RATIO,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1c:tp__ty_2Erealax_2Ereal] : ( ! [V2N:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1c))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2N))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1c))@(ap@c_2Ereal_2Eabs@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n))))))))) => (p@(ap@c_2Eseq_2Esummable@V0f)))))))).
thf(conj_thm_2Eseq_2ELE__SEQ__IMP__LE__LIM,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@V2f@(inj__ty_2Enum_2Enum @ V3n))))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2f)@(inj__ty_2Erealax_2Ereal @ V1y)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y))))))))).
thf(conj_thm_2Eseq_2ESEQ__LE__IMP__LIM__LE,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V2f@(inj__ty_2Enum_2Enum @ V3n)))@(inj__ty_2Erealax_2Ereal @ V0x)))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2f)@(inj__ty_2Erealax_2Ereal @ V1y)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1y))@(inj__ty_2Erealax_2Ereal @ V0x))))))))).
thf(conj_thm_2Eseq_2ESEQ__MONO__LE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V0f@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1x)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))@(inj__ty_2Erealax_2Ereal @ V1x))))))))).
thf(conj_thm_2Eseq_2ESEQ__LE__MONO,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n))))) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1x)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1x))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))))))))).
thf(ax_thm_2Eseq_2Emono__increasing__def,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Emono__increasing@V0f)) <=> ( ! [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_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V1m)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))))))))).
thf(conj_thm_2Eseq_2Emono__increasing__suc,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Emono__increasing@V0f)) <=> ( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n)))@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(ax_thm_2Eseq_2Emono__decreasing__def,axiom,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Emono__decreasing@V0f)) <=> ( ! [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_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1m))))))))))).
thf(conj_thm_2Eseq_2Emono__decreasing__suc,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@c_2Eseq_2Emono__decreasing@V0f)) <=> ( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Eseq_2Emono__increasing__converges__to__sup,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1r:tp__ty_2Erealax_2Ereal] : (((p@(ap@c_2Eseq_2Emono__increasing@V0f)) & (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1r)))) => (V1r = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Esup@(ap@(ap@(c_2Epred__set_2EIMAGE@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@V0f)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum)))))))))).
thf(conj_thm_2Eseq_2EINCREASING__SEQ,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ((( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n)))@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))))) & (( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(inj__ty_2Erealax_2Ereal @ V1l)))) & ( ! [V4e:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V4e))) => (? [V5n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1l))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@(inj__ty_2Enum_2Enum @ V5n)))@(inj__ty_2Erealax_2Ereal @ V4e))))))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V1l)))))))).
thf(conj_thm_2Eseq_2EMAX__LE__X,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2EMAX@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V2k))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2k))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2k))))))))).
thf(conj_thm_2Eseq_2EX__LE__MAX,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2k))@(ap@(ap@c_2Earithmetic_2EMAX@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2k))@(inj__ty_2Enum_2Enum @ V0m))) | (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2k))@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Eseq_2ETRANSFORM__2D__NUM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))) => ((( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V1m)))))) & ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V3m))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V4n))))))) => ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V6n))))))))).
thf(conj_thm_2Eseq_2ETRIANGLE__2D__NUM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))) => (( ! [V1d:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1d))@(inj__ty_2Enum_2Enum @ V2n)))))) => ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V4n))) => (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V4n)))))))))).
thf(conj_thm_2Eseq_2ESEQ__SANDWICH,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2h:$i] : ((mem@V2h@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3l:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V0f)@(inj__ty_2Erealax_2Ereal @ V3l))) & ((p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V2h)@(inj__ty_2Erealax_2Ereal @ V3l))) & ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V4n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V4n)))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V1g@(inj__ty_2Enum_2Enum @ V4n)))@(ap@V2h@(inj__ty_2Enum_2Enum @ V4n)))))))) => (p@(ap@(ap@c_2Eseq_2E_2D_2D_3E@V1g)@(inj__ty_2Erealax_2Ereal @ V3l)))))))))))).
thf(conj_thm_2Eseq_2ESER__POS,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@c_2Eseq_2Esummable@V0f)) & ( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n)))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Eseq_2Esuminf@V0f))))))).
thf(conj_thm_2Eseq_2ESER__POS__MONO,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))) => (p@(ap@c_2Eseq_2Emono@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V2n))@V0f))))))))).
thf(conj_thm_2Eseq_2EPOS__SUMMABLE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))) & (? [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3n)))@V0f))@(inj__ty_2Erealax_2Ereal @ V2x)))))) => (p@(ap@c_2Eseq_2Esummable@V0f)))))).
thf(conj_thm_2Eseq_2ESUMMABLE__LE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x:tp__ty_2Erealax_2Ereal] : (((p@(ap@c_2Eseq_2Esummable@V0f)) & ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2n)))@V0f))@(inj__ty_2Erealax_2Ereal @ V1x))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Eseq_2Esuminf@V0f))@(inj__ty_2Erealax_2Ereal @ V1x)))))))).
thf(conj_thm_2Eseq_2ESUMS__EQ,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eseq_2Esums@V0f)@(inj__ty_2Erealax_2Ereal @ V1x))) <=> ((p@(ap@c_2Eseq_2Esummable@V0f)) & ((surj__ty_2Erealax_2Ereal @ (ap@c_2Eseq_2Esuminf@V0f)) = V1x))))))).
thf(conj_thm_2Eseq_2ESUMINF__POS,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))) & (p@(ap@c_2Eseq_2Esummable@V0f))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Eseq_2Esuminf@V0f))))))).
thf(conj_thm_2Eseq_2ESUM__PICK,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n)))@(lam@ty_2Enum_2Enum@(^ [V3m:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3m)@(inj__ty_2Enum_2Enum @ V1k)))@(inj__ty_2Erealax_2Ereal @ V2x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Erealax_2Ereal @ V2x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Eseq_2ESUM__LT,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((( ! [V4r:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V4r))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4r))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2Enum_2Enum @ V2m))))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@V0f@(inj__ty_2Enum_2Enum @ V4r)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V4r)))))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3n)))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3n)))@V0f))@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3n)))@V1g))))))))))).
thf(conj_thm_2Eseq_2ESUM__CONST__R,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1r:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n)))@(ap@(c_2Ecombin_2EK@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(inj__ty_2Erealax_2Ereal @ V1r)))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Erealax_2Ereal @ V1r))))))).
thf(conj_thm_2Eseq_2ESUMS__ZERO,lemma,(p@(ap@(ap@c_2Eseq_2Esums@(ap@(c_2Ecombin_2EK@ty_2Erealax_2Ereal@ty_2Enum_2Enum)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Eseq_2ELT__SUC,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0a))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1b)))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b))) | (V0a = V1b)))))).
thf(conj_thm_2Eseq_2ELE__SUC,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0a))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1b)))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b))) | (V0a = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1b))))))))).
thf(conj_thm_2Eseq_2EK__PARTIAL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Ecombin_2EK@A_27a@A_27b)@V0x) = (lam@A_27b@(^ [V1z:$i] : V0x)))))))).
thf(conj_thm_2Eseq_2EHALF__POS,lemma,(p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Eseq_2EHALF__LT__1,lemma,(p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Eseq_2EHALF__CANCEL,lemma,((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__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))))))).
thf(conj_thm_2Eseq_2EX__HALF__HALF,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(inj__ty_2Erealax_2Ereal @ V0x)))) = V0x))).
thf(conj_thm_2Eseq_2EONE__MINUS__HALF,lemma,((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Ereal__sub@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Eseq_2ENUM__2D__BIJ__BIG__SQUARE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))) => ( ! [V1N:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@V0f)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@(ap@(ap@(c_2Epred__set_2ECROSS@ty_2Enum_2Enum@ty_2Enum_2Enum)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum)))) => (? [V2k:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(ap@(c_2Epred__set_2EIMAGE@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@V0f)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1N))))@(ap@(ap@(c_2Epred__set_2ECROSS@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V2k)))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V2k))))))))))).
thf(conj_thm_2Eseq_2ENUM__2D__BIJ__SMALL__SQUARE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))) => ( ! [V1k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@V0f)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@(ap@(ap@(c_2Epred__set_2ECROSS@ty_2Enum_2Enum@ty_2Enum_2Enum)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum)))) => (? [V2N:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(ap@(c_2Epred__set_2ECROSS@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1k)))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1k))))@(ap@(ap@(c_2Epred__set_2EIMAGE@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@V0f)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V2N))))))))))).
thf(conj_thm_2Eseq_2ESUMINF__ADD,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@c_2Eseq_2Esummable@V0f)) & (p@(ap@c_2Eseq_2Esummable@V1g))) => ((p@(ap@c_2Eseq_2Esummable@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@V2n))@(ap@V1g@V2n)))))) & ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@c_2Eseq_2Esuminf@V0f))@(ap@c_2Eseq_2Esuminf@V1g))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Eseq_2Esuminf@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@V3n))@(ap@V1g@V3n)))))))))))))).
thf(conj_thm_2Eseq_2ESUMINF__2D,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2h:$i] : ((mem@V2h@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))) => ((( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@V0f@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V4n)))))) & (( ! [V5n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Eseq_2Esums@(ap@V0f@(inj__ty_2Enum_2Enum @ V5n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V5n))))) & ((p@(ap@c_2Eseq_2Esummable@V1g)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@V2h)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@(ap@(ap@(c_2Epred__set_2ECROSS@ty_2Enum_2Enum@ty_2Enum_2Enum)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))))))) => (p@(ap@(ap@c_2Eseq_2Esums@(ap@(ap@(c_2Ecombin_2Eo@ty_2Enum_2Enum@ty_2Erealax_2Ereal@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@V0f))@V2h))@(ap@c_2Eseq_2Esuminf@V1g))))))))))).
thf(conj_thm_2Eseq_2EPOW__HALF__SER,lemma,(p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V0n:$i] : (ap@(ap@c_2Ereal_2Epow@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Earithmetic_2E_2B@V0n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Eseq_2ESER__POS__COMPARE,conjecture,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))))) & ((p@(ap@c_2Eseq_2Esummable@V1g)) & ( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V1g@(inj__ty_2Enum_2Enum @ V3n))))))) => ((p@(ap@c_2Eseq_2Esummable@V0f)) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Eseq_2Esuminf@V0f))@(ap@c_2Eseq_2Esuminf@V1g)))))))))).
