include('Axioms/real_sigma^2.ax').
thf(tp_c_2Eintegral_2Eintegrable,type,(c_2Eintegral_2Eintegrable:$i)).
thf(mem_c_2Eintegral_2Eintegrable,axiom,(mem@c_2Eintegral_2Eintegrable@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@bool)))).
thf(tp_c_2Eintegral_2Eintegral,type,(c_2Eintegral_2Eintegral:$i)).
thf(mem_c_2Eintegral_2Eintegral,axiom,(mem@c_2Eintegral_2Eintegral@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal)))).
thf(conj_thm_2Eintegral_2ESUM__SPLIT,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3p:tp__ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2n)))@V1f))@(ap@(ap@c_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V2n)))@(inj__ty_2Enum_2Enum @ V3p)))@V1f))) = (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 @ V0m))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3p))))@V1f))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__APPEND__EXPLICIT,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : ( ! [V3g:$i] : ((mem@V3g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V4d1:$i] : ((mem@V4d1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V5p1:$i] : ((mem@V5p1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V6d2:$i] : ((mem@V6d2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V7p2:$i] : ((mem@V7p2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4d1)@V5p1))) & ((p@(ap@(ap@c_2Etransc_2Efine@V3g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4d1)@V5p1))) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V2c)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6d2)@V7p2))) & (p@(ap@(ap@c_2Etransc_2Efine@V3g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6d2)@V7p2)))))) => ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V2c)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@(lam@ty_2Enum_2Enum@(^ [V8n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@V8n)@(ap@c_2Etransc_2Edsize@V4d1)))@(ap@V4d1@V8n))@(ap@V6d2@(ap@(ap@c_2Earithmetic_2E_2D@V8n)@(ap@c_2Etransc_2Edsize@V4d1)))))))@(lam@ty_2Enum_2Enum@(^ [V9n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@V9n)@(ap@c_2Etransc_2Edsize@V4d1)))@(ap@V5p1@V9n))@(ap@V7p2@(ap@(ap@c_2Earithmetic_2E_2D@V9n)@(ap@c_2Etransc_2Edsize@V4d1))))))))) & ((p@(ap@(ap@c_2Etransc_2Efine@V3g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@(lam@ty_2Enum_2Enum@(^ [V10n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@V10n)@(ap@c_2Etransc_2Edsize@V4d1)))@(ap@V4d1@V10n))@(ap@V6d2@(ap@(ap@c_2Earithmetic_2E_2D@V10n)@(ap@c_2Etransc_2Edsize@V4d1)))))))@(lam@ty_2Enum_2Enum@(^ [V11n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@V11n)@(ap@c_2Etransc_2Edsize@V4d1)))@(ap@V5p1@V11n))@(ap@V7p2@(ap@(ap@c_2Earithmetic_2E_2D@V11n)@(ap@c_2Etransc_2Edsize@V4d1))))))))) & ( ! [V12f:$i] : ((mem@V12f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@(lam@ty_2Enum_2Enum@(^ [V13n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@V13n)@(ap@c_2Etransc_2Edsize@V4d1)))@(ap@V4d1@V13n))@(ap@V6d2@(ap@(ap@c_2Earithmetic_2E_2D@V13n)@(ap@c_2Etransc_2Edsize@V4d1)))))))@(lam@ty_2Enum_2Enum@(^ [V14n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Eprim__rec_2E_3C@V14n)@(ap@c_2Etransc_2Edsize@V4d1)))@(ap@V5p1@V14n))@(ap@V7p2@(ap@(ap@c_2Earithmetic_2E_2D@V14n)@(ap@c_2Etransc_2Edsize@V4d1))))))))@V12f)) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4d1)@V5p1))@V12f))@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6d2)@V7p2))@V12f))))))))))))))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__APPEND__STRONG,lemma,( ! [V0g:$i] : ((mem@V0g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3c:tp__ty_2Erealax_2Ereal] : ( ! [V4D1:$i] : ((mem@V4D1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V5p1:$i] : ((mem@V5p1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V6D2:$i] : ((mem@V6D2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V7p2:$i] : ((mem@V7p2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4D1)@V5p1))) & ((p@(ap@(ap@c_2Etransc_2Efine@V0g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4D1)@V5p1))) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6D2)@V7p2))) & (p@(ap@(ap@c_2Etransc_2Efine@V0g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6D2)@V7p2)))))) => (? [V8D:$i] : ((mem@V8D@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & (? [V9p:$i] : ((mem@V9p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3c)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8D)@V9p))) & ((p@(ap@(ap@c_2Etransc_2Efine@V0g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8D)@V9p))) & ( ! [V10f:$i] : ((mem@V10f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8D)@V9p))@V10f)) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4D1)@V5p1))@V10f))@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6D2)@V7p2))@V10f))))))))))))))))))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__APPEND,lemma,( ! [V0g:$i] : ((mem@V0g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3c:tp__ty_2Erealax_2Ereal] : (((? [V4D1:$i] : ((mem@V4D1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & (? [V5p1:$i] : ((mem@V5p1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4D1)@V5p1))) & (p@(ap@(ap@c_2Etransc_2Efine@V0g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V4D1)@V5p1)))))))) & (? [V6D2:$i] : ((mem@V6D2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & (? [V7p2:$i] : ((mem@V7p2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6D2)@V7p2))) & (p@(ap@(ap@c_2Etransc_2Efine@V0g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6D2)@V7p2))))))))) => (? [V8D:$i] : ((mem@V8D@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & (? [V9p:$i] : ((mem@V9p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3c)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8D)@V9p))) & (p@(ap@(ap@c_2Etransc_2Efine@V0g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8D)@V9p))))))))))))))).
thf(ax_thm_2Eintegral_2Eintegrable__def,axiom,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ((p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2f)) <=> (? [V3i:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2f)@(inj__ty_2Erealax_2Ereal @ V3i)))))))))).
thf(ax_thm_2Eintegral_2Eintegral__def,axiom,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Eintegral_2Eintegral@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2f)) = (surj__ty_2Erealax_2Ereal @ (ap@(c_2Emin_2E_40@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V3i:$i] : (ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2f)@V3i))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__DINT,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)@(ap@(ap@c_2Eintegral_2Eintegral@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__BOUNDS,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0d)) => ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(ap@V0d@(inj__ty_2Enum_2Enum @ V3n)))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0d@(inj__ty_2Enum_2Enum @ V3n)))@(inj__ty_2Erealax_2Ereal @ V2b))))))))))).
thf(conj_thm_2Eintegral_2ETDIV__BOUNDS,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1p:$i] : ((mem@V1p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V0d)@V1p))) => ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(ap@V0d@(inj__ty_2Enum_2Enum @ V4n)))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0d@(inj__ty_2Enum_2Enum @ V4n)))@(inj__ty_2Erealax_2Ereal @ V3b))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(ap@V1p@(inj__ty_2Enum_2Enum @ V4n)))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V1p@(inj__ty_2Enum_2Enum @ V4n)))@(inj__ty_2Erealax_2Ereal @ V3b))))))))))))))).
thf(conj_thm_2Eintegral_2ETDIV__LE,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1p:$i] : ((mem@V1p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V0d)@V1p))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b))))))))))).
thf(conj_thm_2Eintegral_2EDINT__WRONG,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V3i:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V0a))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2f)@(inj__ty_2Erealax_2Ereal @ V3i)))))))))).
thf(conj_thm_2Eintegral_2EDINT__INTEGRAL,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3i:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V3i)))) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Eintegral_2Eintegral@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)) = V3i)))))))).
thf(conj_thm_2Eintegral_2EDINT__NEG,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3i:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V3i))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(lam@ty_2Erealax_2Ereal@(^ [V4x:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@V0f@V4x)))))@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V3i))))))))))).
thf(conj_thm_2Eintegral_2EDINT__0,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(lam@ty_2Erealax_2Ereal@(^ [V2x:$i] : (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_2Eintegral_2EDINT__ADD,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : ( ! [V5j:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V5j)))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@(lam@ty_2Erealax_2Ereal@(^ [V6x:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@V6x))@(ap@V1g@V6x)))))@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V4i))@(inj__ty_2Erealax_2Ereal @ V5j)))))))))))))).
thf(conj_thm_2Eintegral_2EDINT__SUB,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : ( ! [V5j:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V5j)))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@(lam@ty_2Erealax_2Ereal@(^ [V6x:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0f@V6x))@(ap@V1g@V6x)))))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V4i))@(inj__ty_2Erealax_2Ereal @ V5j)))))))))))))).
thf(conj_thm_2Eintegral_2EDSIZE__EQ,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2D:$i] : ((mem@V2D@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2D)) => ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Ereal__sub@(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))@(ap@c_2Etransc_2Edsize@V2D)))@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V2D@(ap@c_2Enum_2ESUC@V3n)))@(ap@V2D@V3n))))))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V0a)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Eintegral_2EDINT__CONST,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(lam@ty_2Erealax_2Ereal@(^ [V3x:$i] : (inj__ty_2Erealax_2Ereal @ V2c))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V2c))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V0a))))))))).
thf(conj_thm_2Eintegral_2EDINT__CMUL,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3c:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(lam@ty_2Erealax_2Ereal@(^ [V5x:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V3c))@(ap@V0f@V5x)))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V3c))@(inj__ty_2Erealax_2Ereal @ V4i)))))))))))).
thf(conj_thm_2Eintegral_2EDINT__LINEAR,lemma,( ! [V0m:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V3g:$i] : ((mem@V3g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V4a:tp__ty_2Erealax_2Ereal] : ( ! [V5b:tp__ty_2Erealax_2Ereal] : ( ! [V6i:tp__ty_2Erealax_2Ereal] : ( ! [V7j:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V5b)))@V2f)@(inj__ty_2Erealax_2Ereal @ V6i))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V5b)))@V3g)@(inj__ty_2Erealax_2Ereal @ V7j)))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V5b)))@(lam@ty_2Erealax_2Ereal@(^ [V8x:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0m))@(ap@V2f@V8x)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1n))@(ap@V3g@V8x))))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0m))@(inj__ty_2Erealax_2Ereal @ V6i)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1n))@(inj__ty_2Erealax_2Ereal @ V7j))))))))))))))))).
thf(conj_thm_2Eintegral_2ELT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false)) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))) <=> ((V1m = V2n) | (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))))))))).
thf(conj_thm_2Eintegral_2ELE__0,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))))).
thf(conj_thm_2Eintegral_2ELT__0,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Eintegral_2EEQ__SUC,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) <=> (V0m = V1n))))).
thf(conj_thm_2Eintegral_2ELE__LT,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) | (V0m = V1n)))))).
thf(conj_thm_2Eintegral_2ELT__LE,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) & (~~ (V0m = V1n))))))).
thf(conj_thm_2Eintegral_2EREAL__LT__MIN,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V2z))@(ap@(ap@c_2Ereal_2Emin@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))) <=> ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V0x))) & (p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V1y))))))))).
thf(conj_thm_2Eintegral_2EREAL__LE__RMUL1,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V2z)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V2z)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1y))@(inj__ty_2Erealax_2Ereal @ V2z))))))))).
thf(conj_thm_2Eintegral_2EREAL__LE__LMUL1,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V0x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1y))@(inj__ty_2Erealax_2Ereal @ V2z)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V2z))))))))).
thf(conj_thm_2Eintegral_2EINTEGRAL__LE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4i:$i] : ((mem@V4i@A_27a) => ( ! [V5j:$i] : ((mem@V5j@A_27b) => (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b))) & ((p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)) & ((p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)) & ( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V6x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V3b)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V6x)))@(ap@V1g@(inj__ty_2Erealax_2Ereal @ V6x))))))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Eintegral_2Eintegral@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f))@(ap@(ap@c_2Eintegral_2Eintegral@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g))))))))))))))))).
thf(conj_thm_2Eintegral_2EDINT__LE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : ( ! [V5j:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b))) & ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) & ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V5j))) & ( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V6x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V3b)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V6x)))@(ap@V1g@(inj__ty_2Erealax_2Ereal @ V6x))))))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V4i))@(inj__ty_2Erealax_2Ereal @ V5j))))))))))))).
thf(conj_thm_2Eintegral_2EDINT__TRIANGLE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3i:tp__ty_2Erealax_2Ereal] : ( ! [V4j:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V3i))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(lam@ty_2Erealax_2Ereal@(^ [V5x:$i] : (ap@c_2Ereal_2Eabs@(ap@V0f@V5x)))))@(inj__ty_2Erealax_2Ereal @ V4j))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V3i)))@(inj__ty_2Erealax_2Ereal @ V4j))))))))))).
thf(conj_thm_2Eintegral_2EDINT__EQ,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : ( ! [V5j:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b))) & ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) & ((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V5j))) & ( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V6x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V3b)))) => ((surj__ty_2Erealax_2Ereal @ (ap@V0f@(inj__ty_2Erealax_2Ereal @ V6x))) = (surj__ty_2Erealax_2Ereal @ (ap@V1g@(inj__ty_2Erealax_2Ereal @ V6x))))))))) => (V4i = V5j))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRAL__EQ,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) & ( ! [V5x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V5x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V5x))@(inj__ty_2Erealax_2Ereal @ V3b)))) => ((surj__ty_2Erealax_2Ereal @ (ap@V0f@(inj__ty_2Erealax_2Ereal @ V5x))) = (surj__ty_2Erealax_2Ereal @ (ap@V1g@(inj__ty_2Erealax_2Ereal @ V5x))))))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V4i)))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRATION__BY__PARTS,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2f_27:$i] : ((mem@V2f_27@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V3g_27:$i] : ((mem@V3g_27@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V4a:tp__ty_2Erealax_2Ereal] : ( ! [V5b:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V5b))) & (( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V6x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V5b)))) => (p@(ap@(ap@(ap@c_2Elim_2Ediffl@V0f)@(ap@V2f_27@(inj__ty_2Erealax_2Ereal @ V6x)))@(inj__ty_2Erealax_2Ereal @ V6x))))) & ( ! [V7x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V7x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V7x))@(inj__ty_2Erealax_2Ereal @ V5b)))) => (p@(ap@(ap@(ap@c_2Elim_2Ediffl@V1g)@(ap@V3g_27@(inj__ty_2Erealax_2Ereal @ V7x)))@(inj__ty_2Erealax_2Ereal @ V7x))))))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V4a))@(inj__ty_2Erealax_2Ereal @ V5b)))@(lam@ty_2Erealax_2Ereal@(^ [V8x:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@V2f_27@V8x))@(ap@V1g@V8x)))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@V0f@V8x))@(ap@V3g_27@V8x))))))@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V5b)))@(ap@V1g@(inj__ty_2Erealax_2Ereal @ V5b))))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V4a)))@(ap@V1g@(inj__ty_2Erealax_2Ereal @ V4a)))))))))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__LE__SUC,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0d)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0d@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V0d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__MONO__LE,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0d)) => ( ! [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__lte@(ap@V0d@(inj__ty_2Enum_2Enum @ V3m)))@(ap@V0d@(inj__ty_2Enum_2Enum @ V4n))))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__MONO__LE__SUC,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0d)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0d@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V0d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__DSIZE__LE,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2d:$i] : ((mem@V2d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2d)) & ((surj__ty_2Erealax_2Ereal @ (ap@V2d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))) = (surj__ty_2Erealax_2Ereal @ (ap@V2d@(inj__ty_2Enum_2Enum @ V3n))))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Etransc_2Edsize@V2d))@(inj__ty_2Enum_2Enum @ V3n)))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__DSIZE__GE,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2d:$i] : ((mem@V2d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2d)) & (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@V2d@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V2d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))@(ap@c_2Etransc_2Edsize@V2d)))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__DSIZE__EQ,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2d:$i] : ((mem@V2d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2d)) & ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@V2d@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V2d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))) & ((surj__ty_2Erealax_2Ereal @ (ap@V2d@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))) = (surj__ty_2Erealax_2Ereal @ (ap@V2d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Etransc_2Edsize@V2d)) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__DSIZE__EQ__ALT,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2d:$i] : ((mem@V2d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@V2d)) & (((surj__ty_2Erealax_2Ereal @ (ap@V2d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))) = (surj__ty_2Erealax_2Ereal @ (ap@V2d@(inj__ty_2Enum_2Enum @ V3n)))) & ( ! [V4i:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4i))@(inj__ty_2Enum_2Enum @ V3n))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@V2d@(inj__ty_2Enum_2Enum @ V4i)))@(ap@V2d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V4i))))))))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Etransc_2Edsize@V2d)) = V3n)))))))).
thf(conj_thm_2Eintegral_2Enum__MAX,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => (((? [V1x:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V1x)))) & (? [V2M:tp__ty_2Enum_2Enum] : ( ! [V3x:tp__ty_2Enum_2Enum] : ((p@(ap@V0P@(inj__ty_2Enum_2Enum @ V3x))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3x))@(inj__ty_2Enum_2Enum @ V2M))))))) <=> (? [V4m:tp__ty_2Enum_2Enum] : ((p@(ap@V0P@(inj__ty_2Enum_2Enum @ V4m))) & ( ! [V5x:tp__ty_2Enum_2Enum] : ((p@(ap@V0P@(inj__ty_2Enum_2Enum @ V5x))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V5x))@(inj__ty_2Enum_2Enum @ V4m))))))))))).
thf(conj_thm_2Eintegral_2EDIVISION__INTERMEDIATE,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3c:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Etransc_2Edivision@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0d)) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3c))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V3c))@(inj__ty_2Erealax_2Ereal @ V2b))))) => (? [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V4n))@(ap@c_2Etransc_2Edsize@V0d))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@V0d@(inj__ty_2Enum_2Enum @ V4n)))@(inj__ty_2Erealax_2Ereal @ V3c))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V3c))@(ap@V0d@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V4n))))))))))))))).
thf(conj_thm_2Eintegral_2EDINT__COMBINE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3c:tp__ty_2Erealax_2Ereal] : ( ! [V4i:tp__ty_2Erealax_2Ereal] : ( ! [V5j: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@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V4i))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c)))@V0f)@(inj__ty_2Erealax_2Ereal @ V5j)))))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3c)))@V0f)@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V4i))@(inj__ty_2Erealax_2Ereal @ V5j))))))))))))).
thf(conj_thm_2Eintegral_2ESUM__EQ__0,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (( ! [V3r:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V3r))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3r))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))) => ((surj__ty_2Erealax_2Ereal @ (ap@V2f@(inj__ty_2Enum_2Enum @ V3r))) = (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_2Ereal_2Esum@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))@V2f)) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Eintegral_2EDINT__DELTA__LEFT,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(lam@ty_2Erealax_2Ereal@(^ [V2x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@V2x)@(inj__ty_2Erealax_2Ereal @ V0a)))@(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@(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_2Eintegral_2EDINT__DELTA__RIGHT,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(lam@ty_2Erealax_2Ereal@(^ [V2x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@V2x)@(inj__ty_2Erealax_2Ereal @ V1b)))@(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@(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_2Eintegral_2EDINT__DELTA,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(lam@ty_2Erealax_2Ereal@(^ [V3x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@V3x)@(inj__ty_2Erealax_2Ereal @ V2c)))@(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@(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_2Eintegral_2EDINT__POINT__SPIKE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4c:tp__ty_2Erealax_2Ereal] : ( ! [V5i:tp__ty_2Erealax_2Ereal] : ((( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V6x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V3b))) & (~~ (V6x = V4c)))) => ((surj__ty_2Erealax_2Ereal @ (ap@V0f@(inj__ty_2Erealax_2Ereal @ V6x))) = (surj__ty_2Erealax_2Ereal @ (ap@V1g@(inj__ty_2Erealax_2Ereal @ V6x)))))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V5i)))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V5i))))))))))))).
thf(conj_thm_2Eintegral_2EDINT__FINITE__SPIKE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4s:$i] : ((mem@V4s@(arr@ty_2Erealax_2Ereal@bool)) => ( ! [V5i:tp__ty_2Erealax_2Ereal] : (((p@(ap@(c_2Epred__set_2EFINITE@ty_2Erealax_2Ereal)@V4s)) & (( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V6x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V3b))) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V6x))@V4s))))) => ((surj__ty_2Erealax_2Ereal @ (ap@V0f@(inj__ty_2Erealax_2Ereal @ V6x))) = (surj__ty_2Erealax_2Ereal @ (ap@V1g@(inj__ty_2Erealax_2Ereal @ V6x)))))) & (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)@(inj__ty_2Erealax_2Ereal @ V5i))))) => (p@(ap@(ap@(ap@c_2Etransc_2EDint@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)@(inj__ty_2Erealax_2Ereal @ V5i)))))))))))))).
thf(conj_thm_2Eintegral_2EREAL__POW__LBOUND,lemma,( ! [V0x:tp__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)))@(inj__ty_2Erealax_2Ereal @ V0x))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Erealax_2Ereal__add@(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_2Erealax_2Ereal__mul@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Erealax_2Ereal @ V0x))))@(ap@(ap@c_2Ereal_2Epow@(ap@(ap@c_2Erealax_2Ereal__add@(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)))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Eintegral_2EREAL__ARCH__POW,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(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))) => (? [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V1y))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Enum_2Enum @ V2n))))))))).
thf(conj_thm_2Eintegral_2EREAL__ARCH__POW2,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : (? [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Eintegral_2EREAL__POW__LE__1,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(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 @ V1x))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(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_2Epow@(inj__ty_2Erealax_2Ereal @ V1x))@(inj__ty_2Enum_2Enum @ V0n)))))))).
thf(conj_thm_2Eintegral_2EREAL__POW__MONO,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(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 @ V2x))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V2x))@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V2x))@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Eintegral_2EREAL__LE__INV2,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y: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 @ V0x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Erealax_2Einv@(inj__ty_2Erealax_2Ereal @ V1y)))@(ap@c_2Erealax_2Einv@(inj__ty_2Erealax_2Ereal @ V0x)))))))).
thf(conj_thm_2Eintegral_2EGAUGE__MIN__FINITE,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Erealax_2Ereal@bool)) => ( ! [V1gs:$i] : ((mem@V1gs@(arr@ty_2Enum_2Enum@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))) => ( ! [V2n:tp__ty_2Enum_2Enum] : (( ! [V3m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@c_2Etransc_2Egauge@V0s)@(ap@V1gs@(inj__ty_2Enum_2Enum @ V3m)))))) => (? [V4g:$i] : ((mem@V4g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) & ((p@(ap@(ap@c_2Etransc_2Egauge@V0s)@V4g)) & ( ! [V5d:$i] : ((mem@V5d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V6p:$i] : ((mem@V6p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ((p@(ap@(ap@c_2Etransc_2Efine@V4g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V5d)@V6p))) => ( ! [V7m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V7m))@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@c_2Etransc_2Efine@(ap@V1gs@(inj__ty_2Enum_2Enum @ V7m)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V5d)@V6p)))))))))))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__CAUCHY,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)) <=> ( ! [V3e: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 @ V3e))) => (? [V4g:$i] : ((mem@V4g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) & ((p@(ap@(ap@c_2Etransc_2Egauge@(lam@ty_2Erealax_2Ereal@(^ [V5x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@V5x))@(ap@(ap@c_2Ereal_2Ereal__lte@V5x)@(inj__ty_2Erealax_2Ereal @ V2b))))))@V4g)) & ( ! [V6d1:$i] : ((mem@V6d1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V7p1:$i] : ((mem@V7p1@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V8d2:$i] : ((mem@V8d2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V9p2:$i] : ((mem@V9p2@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6d1)@V7p1))) & ((p@(ap@(ap@c_2Etransc_2Efine@V4g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6d1)@V7p1))) & ((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8d2)@V9p2))) & (p@(ap@(ap@c_2Etransc_2Efine@V4g)@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8d2)@V9p2)))))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V6d1)@V7p1))@V0f))@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V8d2)@V9p2))@V0f))))@(inj__ty_2Erealax_2Ereal @ V3e))))))))))))))))))))))).
thf(conj_thm_2Eintegral_2ESUM__DIFFS,lemma,( ! [V0d:$i] : ((mem@V0d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n: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 @ V1m))@(inj__ty_2Enum_2Enum @ V2n)))@(lam@ty_2Enum_2Enum@(^ [V3i:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0d@(ap@c_2Enum_2ESUC@V3i)))@(ap@V0d@V3i)))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0d@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))))@(ap@V0d@(inj__ty_2Enum_2Enum @ V1m)))))))))).
thf(conj_thm_2Eintegral_2ERSUM__BOUND,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2d:$i] : ((mem@V2d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3p:$i] : ((mem@V3p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V4e:tp__ty_2Erealax_2Ereal] : ( ! [V5f:$i] : ((mem@V5f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V2d)@V3p))) & ( ! [V6x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V6x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V1b)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@V5f@(inj__ty_2Erealax_2Ereal @ V6x))))@(inj__ty_2Erealax_2Ereal @ V4e)))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V2d)@V3p))@V5f)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V4e))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V0a)))))))))))))))).
thf(conj_thm_2Eintegral_2ERSUM__DIFF__BOUND,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2d:$i] : ((mem@V2d@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V3p:$i] : ((mem@V3p@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)) => ( ! [V4e:tp__ty_2Erealax_2Ereal] : ( ! [V5f:$i] : ((mem@V5f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V6g:$i] : ((mem@V6g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => (((p@(ap@(ap@c_2Etransc_2Etdiv@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V2d)@V3p))) & ( ! [V7x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V7x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V7x))@(inj__ty_2Erealax_2Ereal @ V1b)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V5f@(inj__ty_2Erealax_2Ereal @ V7x)))@(ap@V6g@(inj__ty_2Erealax_2Ereal @ V7x)))))@(inj__ty_2Erealax_2Ereal @ V4e)))))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V2d)@V3p))@V5f))@(ap@(ap@c_2Etransc_2Ersum@(ap@(ap@(c_2Epair_2E_2C@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal))@V2d)@V3p))@V6g))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V4e))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V0a)))))))))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__LIMIT,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (( ! [V3e: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 @ V3e))) => (? [V4g:$i] : ((mem@V4g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) & (( ! [V5x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V5x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V5x))@(inj__ty_2Erealax_2Ereal @ V2b)))) => (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V5x)))@(ap@V4g@(inj__ty_2Erealax_2Ereal @ V5x)))))@(inj__ty_2Erealax_2Ereal @ V3e))))) & (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V4g))))))) => (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__CONST,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V1b)))@(lam@ty_2Erealax_2Ereal@(^ [V3x:$i] : (inj__ty_2Erealax_2Ereal @ V2c))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__ADD,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b))) & ((p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f)) & (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g)))) => (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@(lam@ty_2Erealax_2Ereal@(^ [V4x:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@V4x))@(ap@V1g@V4x)))))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__CMUL,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [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_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f))) => (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@(lam@ty_2Erealax_2Ereal@(^ [V4x:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V3c))@(ap@V0f@V4x))))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__COMBINE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [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@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)) & (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c)))@V0f))))) => (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3c)))@V0f))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__POINT__SPIKE,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3b:tp__ty_2Erealax_2Ereal] : ( ! [V4c:tp__ty_2Erealax_2Ereal] : ((( ! [V5x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V5x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V5x))@(inj__ty_2Erealax_2Ereal @ V3b))) & (~~ (V5x = V4c)))) => ((surj__ty_2Erealax_2Ereal @ (ap@V0f@(inj__ty_2Erealax_2Ereal @ V5x))) = (surj__ty_2Erealax_2Ereal @ (ap@V1g@(inj__ty_2Erealax_2Ereal @ V5x)))))) & (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V0f))) => (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V2a))@(inj__ty_2Erealax_2Ereal @ V3b)))@V1g))))))))))).
thf(conj_thm_2Eintegral_2ESUP__INTERVAL,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Erealax_2Ereal@bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ((? [V3x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V3x))@(inj__ty_2Erealax_2Ereal @ V2b))) & (p@(ap@V0P@(inj__ty_2Erealax_2Ereal @ V3x)))))) => (? [V4s:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V4s))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V4s))@(inj__ty_2Erealax_2Ereal @ V2b))) & ( ! [V5y:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V5y))@(inj__ty_2Erealax_2Ereal @ V4s))) <=> (? [V6x:tp__ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V6x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((p@(ap@V0P@(inj__ty_2Erealax_2Ereal @ V6x))) & (p@(ap@(ap@c_2Erealax_2Ereal__lt@(inj__ty_2Erealax_2Ereal @ V5y))@(inj__ty_2Erealax_2Ereal @ V6x)))))))))))))))))).
thf(conj_thm_2Eintegral_2EBOLZANO__LEMMA__ALT,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Erealax_2Ereal@(arr@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@(ap@V0P@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & (p@(ap@(ap@V0P@(inj__ty_2Erealax_2Ereal @ V2b))@(inj__ty_2Erealax_2Ereal @ V3c)))))) => (p@(ap@(ap@V0P@(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@(ap@V0P@(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@(ap@V0P@(inj__ty_2Erealax_2Ereal @ V8a))@(inj__ty_2Erealax_2Ereal @ V9b)))))))))).
thf(conj_thm_2Eintegral_2ECONT__UNIFORM,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b))) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V3x))@(inj__ty_2Erealax_2Ereal @ V2b)))) => (p@(ap@(ap@c_2Elim_2Econtl@V0f)@(inj__ty_2Erealax_2Ereal @ V3x)))))) => ( ! [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))) => (? [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))) & ( ! [V6x:tp__ty_2Erealax_2Ereal] : ( ! [V7y:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V6x))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V2b))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V7y))) & ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V7y))@(inj__ty_2Erealax_2Ereal @ V2b))) & (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V6x))@(inj__ty_2Erealax_2Ereal @ V7y))))@(inj__ty_2Erealax_2Ereal @ V5d))))))) => (p@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Eabs@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V6x)))@(ap@V0f@(inj__ty_2Erealax_2Ereal @ V7y)))))@(inj__ty_2Erealax_2Ereal @ V4e)))))))))))))))).
thf(conj_thm_2Eintegral_2EINTEGRABLE__CONTINUOUS,conjecture,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (( ! [V3x:tp__ty_2Erealax_2Ereal] : (((p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V3x))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(inj__ty_2Erealax_2Ereal @ V3x))@(inj__ty_2Erealax_2Ereal @ V2b)))) => (p@(ap@(ap@c_2Elim_2Econtl@V0f)@(inj__ty_2Erealax_2Ereal @ V3x))))) => (p@(ap@(ap@c_2Eintegral_2Eintegrable@(ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V1a))@(inj__ty_2Erealax_2Ereal @ V2b)))@V0f)))))))).
