include('Axioms/powser^2.ax').
thf(tp_c_2Etransc_2EDint,type,(c_2Etransc_2EDint:$i)).
thf(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))))).
thf(tp_c_2Etransc_2Eacs,type,(c_2Etransc_2Eacs:$i)).
thf(mem_c_2Etransc_2Eacs,axiom,(mem@c_2Etransc_2Eacs@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Eacs,type,(fo__c_2Etransc_2Eacs:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Easn,type,(c_2Etransc_2Easn:$i)).
thf(mem_c_2Etransc_2Easn,axiom,(mem@c_2Etransc_2Easn@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Easn,type,(fo__c_2Etransc_2Easn:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Eatn,type,(c_2Etransc_2Eatn:$i)).
thf(mem_c_2Etransc_2Eatn,axiom,(mem@c_2Etransc_2Eatn@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Eatn,type,(fo__c_2Etransc_2Eatn:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Ecos,type,(c_2Etransc_2Ecos:$i)).
thf(mem_c_2Etransc_2Ecos,axiom,(mem@c_2Etransc_2Ecos@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Ecos,type,(fo__c_2Etransc_2Ecos:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Edivision,type,(c_2Etransc_2Edivision:$i)).
thf(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)))).
thf(tp_c_2Etransc_2Edsize,type,(c_2Etransc_2Edsize:$i)).
thf(mem_c_2Etransc_2Edsize,axiom,(mem@c_2Etransc_2Edsize@(arr@(arr@ty_2Enum_2Enum@ty_2Erealax_2Ereal)@ty_2Enum_2Enum))).
thf(tp_c_2Etransc_2Eexp,type,(c_2Etransc_2Eexp:$i)).
thf(mem_c_2Etransc_2Eexp,axiom,(mem@c_2Etransc_2Eexp@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Eexp,type,(fo__c_2Etransc_2Eexp:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Efine,type,(c_2Etransc_2Efine:$i)).
thf(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)))).
thf(tp_c_2Etransc_2Egauge,type,(c_2Etransc_2Egauge:$i)).
thf(mem_c_2Etransc_2Egauge,axiom,(mem@c_2Etransc_2Egauge@(arr@(arr@ty_2Erealax_2Ereal@bool)@(arr@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@bool)))).
thf(tp_c_2Etransc_2Eln,type,(c_2Etransc_2Eln:$i)).
thf(mem_c_2Etransc_2Eln,axiom,(mem@c_2Etransc_2Eln@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Eln,type,(fo__c_2Etransc_2Eln:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Epi,type,(c_2Etransc_2Epi:$i)).
thf(mem_c_2Etransc_2Epi,axiom,(mem@c_2Etransc_2Epi@ty_2Erealax_2Ereal)).
thf(stp_fo_c_2Etransc_2Epi,type,(fo__c_2Etransc_2Epi:tp__ty_2Erealax_2Ereal)).
thf(stp_eq_fo_c_2Etransc_2Epi,axiom,((inj__ty_2Erealax_2Ereal @ fo__c_2Etransc_2Epi) = c_2Etransc_2Epi)).
thf(tp_c_2Etransc_2Eroot,type,(c_2Etransc_2Eroot:$i)).
thf(mem_c_2Etransc_2Eroot,axiom,(mem@c_2Etransc_2Eroot@(arr@ty_2Enum_2Enum@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Etransc_2Eroot,type,(fo__c_2Etransc_2Eroot:(tp__ty_2Enum_2Enum > (tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal)))).
thf(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)))))).
thf(tp_c_2Etransc_2Erpow,type,(c_2Etransc_2Erpow:$i)).
thf(mem_c_2Etransc_2Erpow,axiom,(mem@c_2Etransc_2Erpow@(arr@ty_2Erealax_2Ereal@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(stp_fo_c_2Etransc_2Erpow,type,(fo__c_2Etransc_2Erpow:(tp__ty_2Erealax_2Ereal > (tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal)))).
thf(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)))))).
thf(tp_c_2Etransc_2Ersum,type,(c_2Etransc_2Ersum:$i)).
thf(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)))).
thf(tp_c_2Etransc_2Esin,type,(c_2Etransc_2Esin:$i)).
thf(mem_c_2Etransc_2Esin,axiom,(mem@c_2Etransc_2Esin@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Esin,type,(fo__c_2Etransc_2Esin:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Esqrt,type,(c_2Etransc_2Esqrt:$i)).
thf(mem_c_2Etransc_2Esqrt,axiom,(mem@c_2Etransc_2Esqrt@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Esqrt,type,(fo__c_2Etransc_2Esqrt:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Etan,type,(c_2Etransc_2Etan:$i)).
thf(mem_c_2Etransc_2Etan,axiom,(mem@c_2Etransc_2Etan@(arr@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Etransc_2Etan,type,(fo__c_2Etransc_2Etan:(tp__ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(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))))).
thf(tp_c_2Etransc_2Etdiv,type,(c_2Etransc_2Etdiv:$i)).
thf(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)))).
thf(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@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Erealax_2Einv@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2EFACT@V2n)))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n))))))))).
thf(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@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V2n))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@V2n)@(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_2EFACT@V2n))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n))))))))).
thf(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@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V2n))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@(ap@(ap@c_2Earithmetic_2E_2D@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(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_2EFACT@V2n))))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n))))))))).
thf(conj_thm_2Etransc_2EEXP__CONVERGES,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@c_2Erealax_2Einv@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2EFACT@V2n)))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n)))))@(ap@c_2Etransc_2Eexp@(inj__ty_2Erealax_2Ereal @ V0x)))))).
thf(conj_thm_2Etransc_2ESIN__CONVERGES,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V2n))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@(ap@(ap@c_2Earithmetic_2E_2D@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(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_2EFACT@V2n))))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n)))))@(ap@c_2Etransc_2Esin@(inj__ty_2Erealax_2Ereal @ V0x)))))).
thf(conj_thm_2Etransc_2ECOS__CONVERGES,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V2n))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@V2n)@(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_2EFACT@V2n))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n)))))@(ap@c_2Etransc_2Ecos@(inj__ty_2Erealax_2Ereal @ V0x)))))).
thf(conj_thm_2Etransc_2EEXP__FDIFF,lemma,((ap@c_2Epowser_2Ediffs@(lam@ty_2Enum_2Enum@(^ [V0n:$i] : (ap@c_2Erealax_2Einv@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2EFACT@V0n)))))) = (lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Erealax_2Einv@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2EFACT@V1n))))))).
thf(conj_thm_2Etransc_2ESIN__FDIFF,lemma,((ap@c_2Epowser_2Ediffs@(lam@ty_2Enum_2Enum@(^ [V0n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V0n))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@(ap@(ap@c_2Earithmetic_2E_2D@V0n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(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_2EFACT@V0n))))))) = (lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V1n))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@V1n)@(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_2EFACT@V1n))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Etransc_2ECOS__FDIFF,lemma,((ap@c_2Epowser_2Ediffs@(lam@ty_2Enum_2Enum@(^ [V0n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V0n))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@V0n)@(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_2EFACT@V0n))))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) = (lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V2n))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@(ap@(ap@c_2Earithmetic_2E_2D@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(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_2EFACT@V2n))))))@V1n)))))).
thf(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@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@c_2Earithmetic_2EEVEN@V2n))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@c_2Ereal_2E_2F@(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))))))@(ap@(ap@c_2Earithmetic_2EDIV@(ap@(ap@c_2Earithmetic_2E_2D@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(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_2EFACT@V2n))))))@V1n))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@V1n)))))))))).
thf(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))))).
thf(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))))).
thf(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))))).
thf(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@(lam@ty_2Erealax_2Ereal@(^ [V6x:$i] : (ap@c_2Erealax_2Einv@(ap@V0f@V6x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V7x:$i] : (ap@(ap@c_2Ereal_2E_2F@(ap@V0f@V7x))@(ap@V3g@V7x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V8x:$i] : (ap@(ap@c_2Erealax_2Ereal__add@(ap@V0f@V8x))@(ap@V3g@V8x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V9x:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@V0f@V9x))@(ap@V3g@V9x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V10x:$i] : (ap@(ap@c_2Ereal_2Ereal__sub@(ap@V0f@V10x))@(ap@V3g@V10x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V11x:$i] : (ap@c_2Erealax_2Ereal__neg@(ap@V0f@V11x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V12x:$i] : (ap@(ap@c_2Ereal_2Epow@(ap@V3g@V12x))@(inj__ty_2Enum_2Enum @ 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@(lam@ty_2Erealax_2Ereal@(^ [V13x:$i] : (ap@c_2Etransc_2Eexp@(ap@V3g@V13x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V14x:$i] : (ap@c_2Etransc_2Esin@(ap@V3g@V14x)))))@(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@(lam@ty_2Erealax_2Ereal@(^ [V15x:$i] : (ap@c_2Etransc_2Ecos@(ap@V3g@V15x)))))@(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)))))))))))))))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))).
thf(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))))).
thf(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))))))).
thf(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))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V1u:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Etransc_2Eexp@V1u))@(inj__ty_2Erealax_2Ereal @ V0x))))))))).
thf(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))).
thf(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)))))).
thf(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))))))))).
thf(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)))))).
thf(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))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))).
thf(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))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V2u:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Emin_2E_3D_3D_3E@(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)))@(ap@(ap@c_2Erealax_2Ereal__lt@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V2u)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@(ap@c_2Ereal_2Epow@V2u)@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Erealax_2Ereal @ V1x))))))))))).
thf(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)))))).
thf(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))))).
thf(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))))))))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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)))))))).
thf(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)))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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)))).
thf(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)))).
thf(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))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))).
thf(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)))))).
thf(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)))))))).
thf(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))))))))).
thf(conj_thm_2Etransc_2ESIN__PAIRED,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2E_2F@(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))))))@V1n))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2EFACT@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V1n))@(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@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V1n))@(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)))))).
thf(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))))))).
thf(conj_thm_2Etransc_2ECOS__PAIRED,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Eseq_2Esums@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Ereal_2E_2F@(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))))))@V1n))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2EFACT@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V1n)))))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V1n))))))@(ap@c_2Etransc_2Ecos@(inj__ty_2Erealax_2Ereal @ V0x)))))).
thf(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))))).
thf(conj_thm_2Etransc_2ECOS__ISZERO,lemma,(p@(ap@(c_2Ebool_2E_3F_21@ty_2Erealax_2Ereal)@(lam@ty_2Erealax_2Ereal@(^ [V0x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V0x))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@V0x)@(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_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Etransc_2Ecos@V0x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V0x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V0x))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@V0x)@(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_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Etransc_2Ecos@V0x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))))).
thf(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)@(lam@ty_2Erealax_2Ereal@(^ [V0x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V0x))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Ereal_2Ereal__lte@V0x)@(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_2Emin_2E_3D@ty_2Erealax_2Ereal)@(ap@c_2Etransc_2Ecos@V0x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))).
thf(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))))).
thf(conj_thm_2Etransc_2EPI2__BOUNDS,conjecture,((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)))))))).
