include('Axioms/powser_2.ax').
tff(tp_c_2Etransc_2EDint,type,(c_2Etransc_2EDint:$i)).
tff(mem_c_2Etransc_2EDint,axiom,mem(c_2Etransc_2EDint,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool))))).
tff(tp_c_2Etransc_2Eacs,type,(c_2Etransc_2Eacs:$i)).
tff(mem_c_2Etransc_2Eacs,axiom,mem(c_2Etransc_2Eacs,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Eacs,type,(fo__c_2Etransc_2Eacs:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Eacs,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Eacs(X0)) = ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Easn,type,(c_2Etransc_2Easn:$i)).
tff(mem_c_2Etransc_2Easn,axiom,mem(c_2Etransc_2Easn,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Easn,type,(fo__c_2Etransc_2Easn:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Easn,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Easn(X0)) = ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Eatn,type,(c_2Etransc_2Eatn:$i)).
tff(mem_c_2Etransc_2Eatn,axiom,mem(c_2Etransc_2Eatn,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Eatn,type,(fo__c_2Etransc_2Eatn:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Eatn,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Eatn(X0)) = ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Ecos,type,(c_2Etransc_2Ecos:$i)).
tff(mem_c_2Etransc_2Ecos,axiom,mem(c_2Etransc_2Ecos,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Ecos,type,(fo__c_2Etransc_2Ecos:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Ecos,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Ecos(X0)) = ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Edivision,type,(c_2Etransc_2Edivision:$i)).
tff(mem_c_2Etransc_2Edivision,axiom,mem(c_2Etransc_2Edivision,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),bool)))).
tff(tp_c_2Etransc_2Edsize,type,(c_2Etransc_2Edsize:$i)).
tff(mem_c_2Etransc_2Edsize,axiom,mem(c_2Etransc_2Edsize,arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),ty_2Enum_2Enum))).
tff(tp_c_2Etransc_2Eexp,type,(c_2Etransc_2Eexp:$i)).
tff(mem_c_2Etransc_2Eexp,axiom,mem(c_2Etransc_2Eexp,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Eexp,type,(fo__c_2Etransc_2Eexp:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Eexp,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Eexp(X0)) = ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Efine,type,(c_2Etransc_2Efine:$i)).
tff(mem_c_2Etransc_2Efine,axiom,mem(c_2Etransc_2Efine,arr(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),bool)))).
tff(tp_c_2Etransc_2Egauge,type,(c_2Etransc_2Egauge:$i)).
tff(mem_c_2Etransc_2Egauge,axiom,mem(c_2Etransc_2Egauge,arr(arr(ty_2Erealax_2Ereal,bool),arr(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),bool)))).
tff(tp_c_2Etransc_2Eln,type,(c_2Etransc_2Eln:$i)).
tff(mem_c_2Etransc_2Eln,axiom,mem(c_2Etransc_2Eln,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Eln,type,(fo__c_2Etransc_2Eln:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Eln,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Eln(X0)) = ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Epi,type,(c_2Etransc_2Epi:$i)).
tff(mem_c_2Etransc_2Epi,axiom,mem(c_2Etransc_2Epi,ty_2Erealax_2Ereal)).
tff(stp_fo_c_2Etransc_2Epi,type,(fo__c_2Etransc_2Epi:tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Epi,axiom,(inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi) = c_2Etransc_2Epi)).
tff(tp_c_2Etransc_2Eroot,type,(c_2Etransc_2Eroot:$i)).
tff(mem_c_2Etransc_2Eroot,axiom,mem(c_2Etransc_2Eroot,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Etransc_2Eroot,type,(fo__c_2Etransc_2Eroot:(tp__ty_2Enum_2Enum * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Eroot,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Eroot(X0,X1)) = ap(ap(c_2Etransc_2Eroot,inj__ty_2Enum_2Enum(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Etransc_2Erpow,type,(c_2Etransc_2Erpow:$i)).
tff(mem_c_2Etransc_2Erpow,axiom,mem(c_2Etransc_2Erpow,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Etransc_2Erpow,type,(fo__c_2Etransc_2Erpow:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Erpow,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Erpow(X0,X1)) = ap(ap(c_2Etransc_2Erpow,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Etransc_2Ersum,type,(c_2Etransc_2Ersum:$i)).
tff(mem_c_2Etransc_2Ersum,axiom,mem(c_2Etransc_2Ersum,arr(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),arr(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Erealax_2Ereal)))).
tff(tp_c_2Etransc_2Esin,type,(c_2Etransc_2Esin:$i)).
tff(mem_c_2Etransc_2Esin,axiom,mem(c_2Etransc_2Esin,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Esin,type,(fo__c_2Etransc_2Esin:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Esin,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Esin(X0)) = ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Esqrt,type,(c_2Etransc_2Esqrt:$i)).
tff(mem_c_2Etransc_2Esqrt,axiom,mem(c_2Etransc_2Esqrt,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Esqrt,type,(fo__c_2Etransc_2Esqrt:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Esqrt,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Esqrt(X0)) = ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Etan,type,(c_2Etransc_2Etan:$i)).
tff(mem_c_2Etransc_2Etan,axiom,mem(c_2Etransc_2Etan,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Etransc_2Etan,type,(fo__c_2Etransc_2Etan:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Etransc_2Etan,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Etan(X0)) = ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Etransc_2Etdiv,type,(c_2Etransc_2Etdiv:$i)).
tff(mem_c_2Etransc_2Etdiv,axiom,mem(c_2Etransc_2Etdiv,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Epair_2Eprod(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),bool)))).
tff(ax_thm_2Etransc_2Eexp,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Eseq_2Esuminf,f2958(V0x)))))).
tff(ax_thm_2Etransc_2Ecos,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Eseq_2Esuminf,f2960(V0x)))))).
tff(ax_thm_2Etransc_2Esin,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Eseq_2Esuminf,f2962(V0x)))))).
tff(conj_thm_2Etransc_2EEXP__CONVERGES,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Eseq_2Esums,f2958(V0x)),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ESIN__CONVERGES,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Eseq_2Esums,f2962(V0x)),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ECOS__CONVERGES,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Eseq_2Esums,f2960(V0x)),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EEXP__FDIFF,lemma,((ap(c_2Epowser_2Ediffs,f2963) = f2964))).
tff(conj_thm_2Etransc_2ESIN__FDIFF,lemma,((ap(c_2Epowser_2Ediffs,f2965) = f2966))).
tff(conj_thm_2Etransc_2ECOS__FDIFF,lemma,((ap(c_2Epowser_2Ediffs,f2967) = f2968))).
tff(conj_thm_2Etransc_2ESIN__NEGLEMMA,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Eseq_2Esuminf,f2969(V0x))))))).
tff(conj_thm_2Etransc_2EDIFF__EXP,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Eexp),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V0x)))))).
tff(conj_thm_2Etransc_2EDIFF__SIN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Esin),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V0x)))))).
tff(conj_thm_2Etransc_2EDIFF__COS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Ecos),ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))),inj__ty_2Erealax_2Ereal(V0x)))))).
tff(conj_thm_2Etransc_2EDIFF__COMPOSITE,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3g:$i] : (mem(V3g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V4m:tp__ty_2Erealax_2Ereal] : ( ! [V5n:tp__ty_2Enum_2Enum] : (((p(ap(ap(ap(c_2Elim_2Ediffl,V0f),inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V2x))) & (~~ (surj__ty_2Erealax_2Ereal(ap(V0f,inj__ty_2Erealax_2Ereal(V2x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2970(V0f)),ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V1l)),ap(ap(c_2Ereal_2Epow,ap(V0f,inj__ty_2Erealax_2Ereal(V2x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V2x)))) & (((p(ap(ap(ap(c_2Elim_2Ediffl,V0f),inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V2x))) & (p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x))) & (~~ (surj__ty_2Erealax_2Ereal(ap(V3g,inj__ty_2Erealax_2Ereal(V2x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2971(V0f,V3g)),ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1l)),ap(V3g,inj__ty_2Erealax_2Ereal(V2x)))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4m)),ap(V0f,inj__ty_2Erealax_2Ereal(V2x))))),ap(ap(c_2Ereal_2Epow,ap(V3g,inj__ty_2Erealax_2Ereal(V2x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V2x)))) & (((p(ap(ap(ap(c_2Elim_2Ediffl,V0f),inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V2x))) & p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x)))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2972(V0f,V3g)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V4m))),inj__ty_2Erealax_2Ereal(V2x)))) & (((p(ap(ap(ap(c_2Elim_2Ediffl,V0f),inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V2x))) & p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x)))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2973(V0f,V3g)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1l)),ap(V3g,inj__ty_2Erealax_2Ereal(V2x)))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V4m)),ap(V0f,inj__ty_2Erealax_2Ereal(V2x))))),inj__ty_2Erealax_2Ereal(V2x)))) & (((p(ap(ap(ap(c_2Elim_2Ediffl,V0f),inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V2x))) & p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x)))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2974(V0f,V3g)),ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V4m))),inj__ty_2Erealax_2Ereal(V2x)))) & ((p(ap(ap(ap(c_2Elim_2Ediffl,V0f),inj__ty_2Erealax_2Ereal(V1l)),inj__ty_2Erealax_2Ereal(V2x))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2975(V0f)),ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1l))),inj__ty_2Erealax_2Ereal(V2x)))) & ((p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2976(V3g,V5n)),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V5n))),ap(ap(c_2Ereal_2Epow,ap(V3g,inj__ty_2Erealax_2Ereal(V2x))),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V5n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V4m))),inj__ty_2Erealax_2Ereal(V2x)))) & ((p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2977(V3g)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,ap(V3g,inj__ty_2Erealax_2Ereal(V2x)))),inj__ty_2Erealax_2Ereal(V4m))),inj__ty_2Erealax_2Ereal(V2x)))) & ((p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2978(V3g)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,ap(V3g,inj__ty_2Erealax_2Ereal(V2x)))),inj__ty_2Erealax_2Ereal(V4m))),inj__ty_2Erealax_2Ereal(V2x)))) & (p(ap(ap(ap(c_2Elim_2Ediffl,V3g),inj__ty_2Erealax_2Ereal(V4m)),inj__ty_2Erealax_2Ereal(V2x))) => p(ap(ap(ap(c_2Elim_2Ediffl,f2979(V3g)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,ap(V3g,inj__ty_2Erealax_2Ereal(V2x))))),inj__ty_2Erealax_2Ereal(V4m))),inj__ty_2Erealax_2Ereal(V2x))))))))))))))))))))))).
tff(conj_thm_2Etransc_2EEXP__0,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Etransc_2EEXP__LE__X,lemma,(( ! [V0x: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,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))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2EEXP__LT__1,lemma,(( ! [V0x: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_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))))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2EEXP__ADD__MUL,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))),ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x))))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y)))))))).
tff(conj_thm_2Etransc_2EEXP__NEG__MUL,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2EEXP__NEG__MUL2,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2EEXP__NEG,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Einv,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2EEXP__ADD,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2EEXP__POS__LE,lemma,(( ! [V0x: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))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EEXP__NZ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Etransc_2EEXP__POS__LT,lemma,(( ! [V0x: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))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EEXP__N,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1x))),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Etransc_2EEXP__SUB,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2EEXP__MONO__IMP,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2EEXP__MONO__LT,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))))))).
tff(conj_thm_2Etransc_2EEXP__MONO__LE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))))))).
tff(conj_thm_2Etransc_2EEXP__INJ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1y)))) <=> (V0x = V1y)))))).
tff(conj_thm_2Etransc_2EEXP__TOTAL__LEMMA,lemma,(( ! [V0y: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(V0y))) => (? [V1x: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(V1x))) & (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1x))) = V0y)))))))).
tff(conj_thm_2Etransc_2EEXP__TOTAL,lemma,(( ! [V0y: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(V0y))) => (? [V1x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V1x))) = V0y)))))).
tff(ax_thm_2Etransc_2Eln,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2980(V0x)))))).
tff(conj_thm_2Etransc_2ELN__EXP,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x)))) = V0x)))).
tff(conj_thm_2Etransc_2EEXP__LN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x)))) = V0x) <=> 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))))))).
tff(conj_thm_2Etransc_2ELN__MUL,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_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Etransc_2ELN__INJ,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_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => ((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1y)))) <=> (V0x = V1y))))))).
tff(conj_thm_2Etransc_2ELN__1,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ELN__INV,lemma,(( ! [V0x: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))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,ap(c_2Erealax_2Einv,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))))))))).
tff(conj_thm_2Etransc_2ELN__DIV,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_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Etransc_2ELN__MONO__LT,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_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2ELN__MONO__LE,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_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2ELN__POW,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eln,ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V1x)),inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1x)))))))))).
tff(conj_thm_2Etransc_2ELN__LE,lemma,(( ! [V0x: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,ap(c_2Etransc_2Eln,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_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ELN__LT__X,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ELN__POS,lemma,(( ! [V0x: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(V0x))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(ax_thm_2Etransc_2Eroot,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Erealax_2Ereal(V1x))) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2981(V0n,V1x))))))).
tff(ax_thm_2Etransc_2Esqrt,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Erealax_2Ereal(V0x)))))).
tff(conj_thm_2Etransc_2EROOT__LT__LEMMA,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Eexp,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1x))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = V1x)))))).
tff(conj_thm_2Etransc_2EROOT__LN,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V1x))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))))))))))).
tff(conj_thm_2Etransc_2EROOT__0,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Etransc_2EROOT__1,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2EROOT__POS__LT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))))))))).
tff(conj_thm_2Etransc_2EROOT__POW__POS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = V1x)))))).
tff(conj_thm_2Etransc_2EPOW__ROOT__POS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V1x)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))))) = V1x)))))).
tff(conj_thm_2Etransc_2EROOT__POS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))))))))).
tff(conj_thm_2Etransc_2EROOT__POS__UNIQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y: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(V1x))) & (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(V2y))) & (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V2y)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = V1x))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))) = V2y))))))).
tff(conj_thm_2Etransc_2EROOT__MUL,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y: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(V1x))) & 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(V2y)))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1x)),inj__ty_2Erealax_2Ereal(V2y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V2y))))))))))).
tff(conj_thm_2Etransc_2EROOT__INV,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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(V1x))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Erealax_2Einv,inj__ty_2Erealax_2Ereal(V1x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Einv,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x)))))))))).
tff(conj_thm_2Etransc_2EROOT__DIV,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y: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(V1x))) & 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(V2y)))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V1x)),inj__ty_2Erealax_2Ereal(V2y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V2y))))))))))).
tff(conj_thm_2Etransc_2EROOT__MONO__LE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Erealax_2Ereal] : ( ! [V2y: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(V1x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1x)),inj__ty_2Erealax_2Ereal(V2y)))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V1x))),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(V2y)))))))))).
tff(conj_thm_2Etransc_2ESQRT__0,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ESQRT__1,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Etransc_2ESQRT__POS__LT,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESQRT__POS__LE,lemma,(( ! [V0x: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,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESQRT__POW2,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0x) <=> 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))))))).
tff(conj_thm_2Etransc_2ESQRT__POW__2,lemma,(( ! [V0x: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))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0x))))).
tff(conj_thm_2Etransc_2EPOW__2__SQRT,lemma,(( ! [V0x: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))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = V0x))))).
tff(conj_thm_2Etransc_2ESQRT__POS__UNIQ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y: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,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y))) & (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V1y)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0x))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))) = V1y)))))).
tff(conj_thm_2Etransc_2ESQRT__MUL,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y: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,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Etransc_2ESQRT__INV,lemma,(( ! [V0x: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))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(c_2Erealax_2Einv,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Einv,ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))))))))).
tff(conj_thm_2Etransc_2ESQRT__DIV,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y: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,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V1y)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Etransc_2ESQRT__MONO__LE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y: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(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2ESQRT__EVEN__POW2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,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(V0n)))) = surj__ty_2Erealax_2Ereal(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))))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Etransc_2EREAL__DIV__SQRT,lemma,(( ! [V0x: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))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESQRT__EQ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = 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(V0x)))) => (V0x = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,inj__ty_2Erealax_2Ereal(V1y))))))))).
tff(conj_thm_2Etransc_2ESIN__0,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ECOS__0,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Etransc_2ESIN__CIRCLE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2ESIN__BOUND,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2ESIN__BOUNDS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2ECOS__BOUND,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2ECOS__BOUNDS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2ESIN__COS__ADD,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V1y)))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V1y)))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Etransc_2ESIN__COS__NEG,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(ap(c_2Erealax_2Ereal__add,ap(c_2Etransc_2Esin,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Ecos,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Etransc_2ESIN__ADD,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Etransc_2ECOS__ADD,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Etransc_2ESIN__NEG,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__NEG,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ESIN__DOUBLE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))))))))).
tff(conj_thm_2Etransc_2ECOS__DOUBLE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2ESIN__PAIRED,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Eseq_2Esums,f2982(V0x)),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ESIN__POS,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__PAIRED,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Eseq_2Esums,f2983(V0x)),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ECOS__2,lemma,(p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Ecos,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ECOS__ISZERO,lemma,(p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2984)))).
tff(ax_thm_2Etransc_2Epi,axiom,(fo__c_2Etransc_2Epi = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2984))))).
tff(conj_thm_2Etransc_2EPI2,lemma,((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2984))))).
tff(conj_thm_2Etransc_2ECOS__PI2,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2EPI2__BOUNDS,lemma,((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2EPI__POS,lemma,(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(fo__c_2Etransc_2Epi))))).
tff(conj_thm_2Etransc_2ESIN__PI2,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Etransc_2ECOS__PI,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Etransc_2ESIN__PI,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ESIN__COS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__SIN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESIN__PERIODIC__PI,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__PERIODIC__PI,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESIN__PERIODIC,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ECOS__PERIODIC,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ECOS__NPI,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Etransc_2ESIN__NPI,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Etransc_2ESIN__POS__PI2,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__POS__PI2,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__POS__PI,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESIN__POS__PI,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__POS__PI2__LE,lemma,(( ! [V0x: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(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__POS__PI__LE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESIN__POS__PI2__LE,lemma,(( ! [V0x: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(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ESIN__POS__PI__LE,lemma,(( ! [V0x: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(V0x)),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ECOS__TOTAL,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2985(V0y))))))).
tff(conj_thm_2Etransc_2ESIN__TOTAL,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2986(V0y))))))).
tff(conj_thm_2Etransc_2ECOS__ZERO__LEMMA,lemma,(( ! [V0x: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))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (? [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1n)))) & (V0x = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))).
tff(conj_thm_2Etransc_2ESIN__ZERO__LEMMA,lemma,(( ! [V0x: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))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => (? [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1n))) & (V0x = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))).
tff(conj_thm_2Etransc_2ECOS__ZERO,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> ((? [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1n)))) & (V0x = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) | (? [V2n:tp__ty_2Enum_2Enum] : ((~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V2n)))) & (V0x = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))).
tff(conj_thm_2Etransc_2ESIN__ZERO,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> ((? [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1n))) & (V0x = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) | (? [V2n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V2n))) & (V0x = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))).
tff(ax_thm_2Etransc_2Etan,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ETAN__0,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ETAN__PI,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2ETAN__NPI,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Etransc_2ETAN__NEG,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2ETAN__PERIODIC,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ETAN__ADD,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (((~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & ((~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V1y))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Erealax_2Ereal__add,ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V1y)))))))))))).
tff(conj_thm_2Etransc_2ETAN__DOUBLE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (((~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x)))),ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2ETAN__POS__PI2,lemma,(( ! [V0x: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_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Etransc_2EDIFF__TAN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Etan),ap(c_2Erealax_2Einv,ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2ETAN__TOTAL__LEMMA,lemma,(( ! [V0y: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(V0y))) => (? [V1x: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(V1x))) & (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V1x))))))))))).
tff(conj_thm_2Etransc_2ETAN__TOTAL__POS,lemma,(( ! [V0y: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(V0y))) => (? [V1x: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(V1x))) & (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V1x))) = V0y)))))))).
tff(conj_thm_2Etransc_2ETAN__TOTAL,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2987(V0y)))))).
tff(ax_thm_2Etransc_2Easn,axiom,( ! [V0y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y))) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2986(V0y)))))).
tff(ax_thm_2Etransc_2Eacs,axiom,( ! [V0y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y))) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2985(V0y)))))).
tff(ax_thm_2Etransc_2Eatn,axiom,( ! [V0y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y))) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2987(V0y)))))).
tff(conj_thm_2Etransc_2EASN,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y)))) & (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y)))) = V0y))))))).
tff(conj_thm_2Etransc_2EASN__SIN,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y)))) = V0y))))).
tff(conj_thm_2Etransc_2EASN__BOUNDS,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2EASN__BOUNDS__LT,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y)))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0y))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2ESIN__ASN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Easn,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))) = V0x))))).
tff(conj_thm_2Etransc_2EACS,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y)))) & (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y)))) = V0y))))))).
tff(conj_thm_2Etransc_2EACS__COS,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y)))) = V0y))))).
tff(conj_thm_2Etransc_2EACS__BOUNDS,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))))))).
tff(conj_thm_2Etransc_2EACS__BOUNDS__LT,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0y))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0y)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y)))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0y))),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))))))).
tff(conj_thm_2Etransc_2ECOS__ACS,lemma,(( ! [V0x: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(V0x)),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eacs,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))) = V0x))))).
tff(conj_thm_2Etransc_2EATN,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y)))) & (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y)))) = V0y)))))).
tff(conj_thm_2Etransc_2EATN__TAN,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Etan,ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y)))) = V0y)))).
tff(conj_thm_2Etransc_2EATN__BOUNDS,lemma,(( ! [V0y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y)))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0y))),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Etransc_2ETAN__ATN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eatn,ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x)))) = V0x))))).
tff(conj_thm_2Etransc_2ETAN__SEC,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = 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_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_2Ereal_2Epow,ap(c_2Etransc_2Etan,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Erealax_2Einv,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2ESIN__COS__SQ,lemma,(( ! [V0x: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(V0x)),inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2ECOS__SIN__SQ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(fo__c_2Etransc_2Epi)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2ECOS__ATN__NZ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eatn,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Etransc_2ECOS__ASN__NZ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Etransc_2ESIN__ACS__NZ,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (~~ (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0x)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Etransc_2ECOS__SIN__SQRT,lemma,(( ! [V0x: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))),ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2ESIN__COS__SQRT,lemma,(( ! [V0x: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))),ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x)))) => (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esin,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Etransc_2EDIFF__LN,lemma,(( ! [V0x: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(ap(c_2Elim_2Ediffl,c_2Etransc_2Eln),ap(c_2Erealax_2Einv,inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EDIFF__ASN__LEMMA,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Easn),ap(c_2Erealax_2Einv,ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Easn,inj__ty_2Erealax_2Ereal(V0x))))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EDIFF__ASN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Easn),ap(c_2Erealax_2Einv,ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EDIFF__ACS__LEMMA,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Eacs),ap(c_2Erealax_2Einv,ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,ap(c_2Etransc_2Eacs,inj__ty_2Erealax_2Ereal(V0x)))))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EDIFF__ACS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Erealax_2Ereal(V0x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Eacs),ap(c_2Erealax_2Ereal__neg,ap(c_2Erealax_2Einv,ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Etransc_2EDIFF__ATN,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Eatn),ap(c_2Erealax_2Einv,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_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))),inj__ty_2Erealax_2Ereal(V0x)))))).
tff(ax_thm_2Etransc_2Edivision,axiom,( ! [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(V2D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0a) & (? [V3N:tp__ty_2Enum_2Enum] : (( ! [V4n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4n)),inj__ty_2Enum_2Enum(V3N))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V2D,inj__ty_2Enum_2Enum(V4n))),ap(V2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V4n))))))) & ( ! [V5n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V5n)),inj__ty_2Enum_2Enum(V3N))) => (surj__ty_2Erealax_2Ereal(ap(V2D,inj__ty_2Enum_2Enum(V5n))) = V1b)))))))))))).
tff(ax_thm_2Etransc_2Edsize,axiom,( ! [V0D:$i] : (mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => (surj__ty_2Enum_2Enum(ap(c_2Etransc_2Edsize,V0D)) = surj__ty_2Enum_2Enum(ap(c_2Emin_2E_40(ty_2Enum_2Enum),f2990(V0D))))))).
tff(ax_thm_2Etransc_2Etdiv,axiom,( ! [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)) => (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))) <=> (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)) & ( ! [V4n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(V2D,inj__ty_2Enum_2Enum(V4n))),ap(V3p,inj__ty_2Enum_2Enum(V4n)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(V3p,inj__ty_2Enum_2Enum(V4n))),ap(V2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V4n)))))))))))))))).
tff(ax_thm_2Etransc_2Egauge,axiom,( ! [V0E:$i] : (mem(V0E,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1g:$i] : (mem(V1g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => (p(ap(ap(c_2Etransc_2Egauge,V0E),V1g)) <=> ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(V0E,inj__ty_2Erealax_2Ereal(V2x))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V1g,inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(ax_thm_2Etransc_2Efine,axiom,( ! [V0g:$i] : (mem(V0g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1D:$i] : (mem(V1D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V2p:$i] : (mem(V2p,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => (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)),V1D),V2p))) <=> ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),ap(c_2Etransc_2Edsize,V1D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Ereal_2Ereal__sub,ap(V1D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n)))),ap(V1D,inj__ty_2Enum_2Enum(V3n)))),ap(V0g,ap(V2p,inj__ty_2Enum_2Enum(V3n))))))))))))))).
tff(ax_thm_2Etransc_2Ersum,axiom,( ! [V0D:$i] : (mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V1p:$i] : (mem(V1p,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V2f:$i] : (mem(V2f,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)),V0D),V1p)),V2f)) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Etransc_2Edsize,V0D))),f2991(V1p,V2f,V0D))))))))))).
tff(ax_thm_2Etransc_2EDint,axiom,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : (mem(V2f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V3k: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(V3k))) <=> ( ! [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))) => (? [V5g:$i] : (mem(V5g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) & (p(ap(ap(c_2Etransc_2Egauge,f2992(V0a,V1b)),V5g)) & ( ! [V7D:$i] : (mem(V7D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V8p:$i] : (mem(V8p,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)),V7D),V8p))) & p(ap(ap(c_2Etransc_2Efine,V5g),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V7D),V8p)))) => 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)),V7D),V8p)),V2f)),inj__ty_2Erealax_2Ereal(V3k)))),inj__ty_2Erealax_2Ereal(V4e)))))))))))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__0,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ((V0a = V1b) => (surj__ty_2Enum_2Enum(ap(c_2Etransc_2Edsize,f2993(V0a,V1b))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Etransc_2EDIVISION__1,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))) => (surj__ty_2Enum_2Enum(ap(c_2Etransc_2Edsize,f2993(V0a,V1b))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2EDIVISION__SINGLE,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))) => 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))),f2993(V0a,V1b)))))))).
tff(conj_thm_2Etransc_2EDIVISION__LHS,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)) => (surj__ty_2Erealax_2Ereal(ap(V0D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V1a)))))))).
tff(conj_thm_2Etransc_2EDIVISION__THM,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)) <=> ((surj__ty_2Erealax_2Ereal(ap(V0D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V1a) & (( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),ap(c_2Etransc_2Edsize,V0D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,inj__ty_2Enum_2Enum(V3n))),ap(V0D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n))))))) & ( ! [V4n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V4n)),ap(c_2Etransc_2Edsize,V0D))) => (surj__ty_2Erealax_2Ereal(ap(V0D,inj__ty_2Enum_2Enum(V4n))) = V2b)))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__RHS,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)) => (surj__ty_2Erealax_2Ereal(ap(V0D,ap(c_2Etransc_2Edsize,V0D))) = V2b)))))))).
tff(conj_thm_2Etransc_2EDIVISION__LT__GEN,lemma,(( ! [V0D:$i] : (mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4n: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(V1a)),inj__ty_2Erealax_2Ereal(V2b))),V0D)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3m)),inj__ty_2Enum_2Enum(V4n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V4n)),ap(c_2Etransc_2Edsize,V0D))))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,inj__ty_2Enum_2Enum(V3m))),ap(V0D,inj__ty_2Enum_2Enum(V4n))))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__LT,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_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),ap(c_2Etransc_2Edsize,V0D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V0D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n)))))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__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)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V2b)))))))))).
tff(conj_thm_2Etransc_2EDIVISION__GT,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_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),ap(c_2Etransc_2Edsize,V0D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,inj__ty_2Enum_2Enum(V3n))),ap(V0D,ap(c_2Etransc_2Edsize,V0D))))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__EQ,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)) => ((V1a = V2b) <=> (surj__ty_2Enum_2Enum(ap(c_2Etransc_2Edsize,V0D)) = fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Etransc_2EDIVISION__LBOUND,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)) => ( ! [V3r:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),ap(V0D,inj__ty_2Enum_2Enum(V3r)))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__LBOUND__LT,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)) & (~~ (surj__ty_2Enum_2Enum(ap(c_2Etransc_2Edsize,V0D)) = fo__c_2Enum_2E0))) => ( ! [V3n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1a)),ap(V0D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n))))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__UBOUND,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)) => ( ! [V3r:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0D,inj__ty_2Enum_2Enum(V3r))),inj__ty_2Erealax_2Ereal(V2b))))))))))).
tff(conj_thm_2Etransc_2EDIVISION__UBOUND__LT,lemma,(( ! [V0D:$i] : (mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__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(V1a)),inj__ty_2Erealax_2Ereal(V2b))),V0D)) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),ap(c_2Etransc_2Edsize,V0D)))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,inj__ty_2Enum_2Enum(V3n))),inj__ty_2Erealax_2Ereal(V2b))))))))))).
tff(conj_thm_2Etransc_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(conj_thm_2Etransc_2EDIVISION__EXISTS,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2g:$i] : (mem(V2g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ((p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))) & p(ap(ap(c_2Etransc_2Egauge,f2994(V0a,V1b)),V2g))) => (? [V4D:$i] : (mem(V4D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & (? [V5p:$i] : (mem(V5p,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)),V4D),V5p))) & p(ap(ap(c_2Etransc_2Efine,V2g),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V4D),V5p))))))))))))))).
tff(conj_thm_2Etransc_2EGAUGE__MIN,lemma,(( ! [V0E:$i] : (mem(V0E,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1g1:$i] : (mem(V1g1,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V2g2:$i] : (mem(V2g2,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ((p(ap(ap(c_2Etransc_2Egauge,V0E),V1g1)) & p(ap(ap(c_2Etransc_2Egauge,V0E),V2g2))) => p(ap(ap(c_2Etransc_2Egauge,V0E),f2995(V1g1,V2g2)))))))))))).
tff(conj_thm_2Etransc_2EFINE__MIN,lemma,(( ! [V0g1:$i] : (mem(V0g1,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1g2:$i] : (mem(V1g2,arr(ty_2Erealax_2Ereal,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)) => (p(ap(ap(c_2Etransc_2Efine,f2996(V0g1,V1g2)),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V2D),V3p))) => (p(ap(ap(c_2Etransc_2Efine,V0g1),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V2D),V3p))) & p(ap(ap(c_2Etransc_2Efine,V1g2),ap(ap(c_2Epair_2E_2C(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)),V2D),V3p))))))))))))))).
tff(conj_thm_2Etransc_2EDINT__UNIQ,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : (mem(V2f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V3k1:tp__ty_2Erealax_2Ereal] : ( ! [V4k2:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))) & (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(V3k1))) & 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(V4k2))))) => (V3k1 = V4k2)))))))))).
tff(conj_thm_2Etransc_2EINTEGRAL__NULL,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1a: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(V1a))),V0f),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Etransc_2EFTC1,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1f_27:$i] : (mem(V1f_27,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))) & ( ! [V4x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2a)),inj__ty_2Erealax_2Ereal(V4x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V3b)))) => p(ap(ap(ap(c_2Elim_2Ediffl,V0f),ap(V1f_27,inj__ty_2Erealax_2Ereal(V4x))),inj__ty_2Erealax_2Ereal(V4x)))))) => 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))),V1f_27),ap(ap(c_2Ereal_2Ereal__sub,ap(V0f,inj__ty_2Erealax_2Ereal(V3b))),ap(V0f,inj__ty_2Erealax_2Ereal(V2a)))))))))))))).
tff(conj_thm_2Etransc_2EMCLAURIN,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1diff:$i] : (mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ( ! [V2h:tp__ty_2Erealax_2Ereal] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V2h))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3n))) & ((ap(V1diff,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = V0f) & ( ! [V4m:tp__ty_2Enum_2Enum] : ( ! [V5t:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4m)),inj__ty_2Enum_2Enum(V3n))) & (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(V5t))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V5t)),inj__ty_2Erealax_2Ereal(V2h))))) => p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,inj__ty_2Enum_2Enum(V4m))),ap(ap(V1diff,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V4m))),inj__ty_2Erealax_2Ereal(V5t))),inj__ty_2Erealax_2Ereal(V5t))))))))) => (? [V6t: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(V6t))) & (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V6t)),inj__ty_2Erealax_2Ereal(V2h))) & (surj__ty_2Erealax_2Ereal(ap(V0f,inj__ty_2Erealax_2Ereal(V2h))) = 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(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3n))),f2997(V1diff,V2h))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,inj__ty_2Enum_2Enum(V3n)),inj__ty_2Erealax_2Ereal(V6t))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V3n))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V2h)),inj__ty_2Enum_2Enum(V3n)))))))))))))))))).
tff(conj_thm_2Etransc_2EMCLAURIN__NEG,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1diff:$i] : (mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ( ! [V2h:tp__ty_2Erealax_2Ereal] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V2h)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3n))) & ((ap(V1diff,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = V0f) & ( ! [V4m:tp__ty_2Enum_2Enum] : ( ! [V5t:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4m)),inj__ty_2Enum_2Enum(V3n))) & (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2h)),inj__ty_2Erealax_2Ereal(V5t))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V5t)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))) => p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,inj__ty_2Enum_2Enum(V4m))),ap(ap(V1diff,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V4m))),inj__ty_2Erealax_2Ereal(V5t))),inj__ty_2Erealax_2Ereal(V5t))))))))) => (? [V6t:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V2h)),inj__ty_2Erealax_2Ereal(V6t))) & (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V6t)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & (surj__ty_2Erealax_2Ereal(ap(V0f,inj__ty_2Erealax_2Ereal(V2h))) = 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(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3n))),f2997(V1diff,V2h))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,inj__ty_2Enum_2Enum(V3n)),inj__ty_2Erealax_2Ereal(V6t))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V3n))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V2h)),inj__ty_2Enum_2Enum(V3n)))))))))))))))))).
tff(conj_thm_2Etransc_2EMCLAURIN__ALL__LT,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1diff:$i] : (mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => (((ap(V1diff,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = V0f) & ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,inj__ty_2Enum_2Enum(V2m))),ap(ap(V1diff,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2m))),inj__ty_2Erealax_2Ereal(V3x))),inj__ty_2Erealax_2Ereal(V3x)))))) => ( ! [V4x:tp__ty_2Erealax_2Ereal] : ( ! [V5n:tp__ty_2Enum_2Enum] : (((~~ (V4x = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V5n)))) => (? [V6t: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))),ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V6t)))) & (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V6t))),ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V4x)))) & (surj__ty_2Erealax_2Ereal(ap(V0f,inj__ty_2Erealax_2Ereal(V4x))) = 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(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V5n))),f2998(V1diff,V4x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,inj__ty_2Enum_2Enum(V5n)),inj__ty_2Erealax_2Ereal(V6t))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V5n))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Enum_2Enum(V5n))))))))))))))))))).
tff(conj_thm_2Etransc_2EMCLAURIN__ZERO,lemma,(( ! [V0diff:$i] : (mem(V0diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : (((V2x = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))),f2999(V0diff,V2x))) = surj__ty_2Erealax_2Ereal(ap(ap(V0diff,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_2Etransc_2EMCLAURIN__ALL__LE,lemma,(( ! [V0f:$i] : (mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1diff:$i] : (mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => (((ap(V1diff,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = V0f) & ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,inj__ty_2Enum_2Enum(V2m))),ap(ap(V1diff,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2m))),inj__ty_2Erealax_2Ereal(V3x))),inj__ty_2Erealax_2Ereal(V3x)))))) => ( ! [V4x:tp__ty_2Erealax_2Ereal] : ( ! [V5n:tp__ty_2Enum_2Enum] : (? [V6t:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V6t))),ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V4x)))) & (surj__ty_2Erealax_2Ereal(ap(V0f,inj__ty_2Erealax_2Ereal(V4x))) = 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(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V5n))),f2998(V1diff,V4x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,inj__ty_2Enum_2Enum(V5n)),inj__ty_2Erealax_2Ereal(V6t))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V5n))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Enum_2Enum(V5n))))))))))))))))).
tff(conj_thm_2Etransc_2EMCLAURIN__EXP__LT,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((~~ (V0x = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))) => (? [V2t: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))),ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V2t)))) & (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V2t))),ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V0x)))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))) = 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(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))),f3000(V0x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V2t))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V1n))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Enum_2Enum(V1n)))))))))))))).
tff(conj_thm_2Etransc_2EMCLAURIN__EXP__LE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (? [V2t:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V2t))),ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V0x)))) & (surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V0x))) = 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(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))),f3000(V0x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eexp,inj__ty_2Erealax_2Ereal(V2t))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V1n))))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Enum_2Enum(V1n)))))))))))).
tff(conj_thm_2Etransc_2EDIFF__LN__COMPOSITE,lemma,(( ! [V0g:$i] : (mem(V0g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ! [V1m:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(ap(c_2Elim_2Ediffl,V0g),inj__ty_2Erealax_2Ereal(V1m)),inj__ty_2Erealax_2Ereal(V2x))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V0g,inj__ty_2Erealax_2Ereal(V2x))))) => p(ap(ap(ap(c_2Elim_2Ediffl,f3001(V0g)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Einv,ap(V0g,inj__ty_2Erealax_2Ereal(V2x)))),inj__ty_2Erealax_2Ereal(V1m))),inj__ty_2Erealax_2Ereal(V2x)))))))))).
tff(ax_thm_2Etransc_2Erpow__def,axiom,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Erpow,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))) = surj__ty_2Erealax_2Ereal(ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V1b)),ap(c_2Etransc_2Eln,inj__ty_2Erealax_2Ereal(V0a))))))))).
tff(conj_thm_2Etransc_2EGEN__RPOW,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V0a))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Erpow,inj__ty_2Erealax_2Ereal(V0a)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Etransc_2ERPOW__SUC__N,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V0a))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Erpow,inj__ty_2Erealax_2Ereal(V0a)),ap(ap(c_2Erealax_2Ereal__add,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0a)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Etransc_2ERPOW__0,lemma,(( ! [V0a: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(V0a))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Erpow,inj__ty_2Erealax_2Ereal(V0a)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2ERPOW__1,lemma,(( ! [V0a: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(V0a))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Erpow,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)))))) = V0a))))).
tff(conj_thm_2Etransc_2EONE__RPOW,lemma,(( ! [V0a: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(V0a))) => (surj__ty_2Erealax_2Ereal(ap(ap(c_2Etransc_2Erpow,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(V0a))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Etransc_2ERPOW__POS__LT,conjecture,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b: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(V0a))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Etransc_2Erpow,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))))))))).
