include('Axioms/real_sigma_2.ax').
tff(tp_c_2Eintegral_2Eintegrable,type,(c_2Eintegral_2Eintegrable:$i)).
tff(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)))).
tff(tp_c_2Eintegral_2Eintegral,type,(c_2Eintegral_2Eintegral:$i)).
tff(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)))).
tff(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)))))))))).
tff(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)),f3193(V6d2,V4d1)),f3194(V5p1,V4d1,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)),f3195(V6d2,V4d1)),f3196(V5p1,V4d1,V7p2)))) & ( ! [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)),f3197(V6d2,V4d1)),f3198(V5p1,V4d1,V7p2))),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)))))))))))))))))))))))).
tff(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)))))))))))))))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))).
tff(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),f3199(V2f,V1b,V0a))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))),f3200(V0f)),ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V3i)))))))))))).
tff(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))),k(ty_2Erealax_2Ereal,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)))))))).
tff(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))),f3201(V0f,V1g)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V4i)),inj__ty_2Erealax_2Ereal(V5j))))))))))))))).
tff(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))),f3202(V0f,V1g)),ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V4i)),inj__ty_2Erealax_2Ereal(V5j))))))))))))))).
tff(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))),f3203(V2D))),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))))))))))).
tff(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))),k(ty_2Erealax_2Ereal,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)))))))))).
tff(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))),f3204(V0f,V3c)),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V3c)),inj__ty_2Erealax_2Ereal(V4i))))))))))))).
tff(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))),f3205(V2f,V0m,V3g,V1n)),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)))))))))))))))))).
tff(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)))))))))).
tff(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)))))).
tff(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))))))).
tff(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)))))).
tff(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))))))).
tff(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)))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))))).
tff(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))),f3206(V0f)),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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))),f3207(V2f_27,V1g,V0f,V3g_27)),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))))))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))).
tff(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))),f3208(V0a)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(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))),f3209(V1b)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(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))),f3210(V2c)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))))))))))))))))).
tff(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,f3211(V1a,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)))))))))))))))))))))))).
tff(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))),f3212(V0d))) = 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))))))))))).
tff(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))))))))))))))))).
tff(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))))))))))))))))))).
tff(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))))))))).
tff(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))),k(ty_2Erealax_2Ereal,inj__ty_2Erealax_2Ereal(V2c))))))))).
tff(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))),f3213(V0f,V1g)))))))))))).
tff(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))),f3214(V0f,V3c))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))).
tff(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))))))))))))))))).
tff(conj_thm_2Eintegral_2EINTEGRABLE__CONTINUOUS,lemma,(( ! [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))))))))).
tff(conj_thm_2Eintegral_2EINTEGRABLE__SPLIT__SIDES,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(V3c))) & (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3c)),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)))) => (? [V4i:tp__ty_2Erealax_2Ereal] : ( ! [V5e: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(V5e))) => (? [V6g:$i] : (mem(V6g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) & (p(ap(ap(c_2Etransc_2Egauge,f3215(V1a,V2b)),V6g)) & ( ! [V8d1:$i] : (mem(V8d1,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V9p1:$i] : (mem(V9p1,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V10d2:$i] : (mem(V10d2,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V11p2:$i] : (mem(V11p2,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)),V8d1),V9p1))) & (p(ap(ap(c_2Etransc_2Efine,V6g),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V8d1),V9p1))) & (p(ap(ap(c_2Etransc_2Etdiv,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3c)),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)),V10d2),V11p2))) & p(ap(ap(c_2Etransc_2Efine,V6g),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V10d2),V11p2)))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,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)),V8d1),V9p1)),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)),V10d2),V11p2)),V0f))),inj__ty_2Erealax_2Ereal(V4i)))),inj__ty_2Erealax_2Ereal(V5e)))))))))))))))))))))))))).
tff(conj_thm_2Eintegral_2EINTEGRABLE__SUBINTERVAL__LEFT,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(V3c))) & (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3c)),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(V3c))),V0f)))))))))).
tff(conj_thm_2Eintegral_2EINTEGRABLE__SUBINTERVAL__RIGHT,conjecture,(( ! [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(V3c))) & (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3c)),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(V3c)),inj__ty_2Erealax_2Ereal(V2b))),V0f)))))))))).
