include('Axioms/powser+2.ax').
fof(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)))) )).
fof(mem_c_2Etransc_2Eacs,axiom,( mem(c_2Etransc_2Eacs,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Etransc_2Easn,axiom,( mem(c_2Etransc_2Easn,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Etransc_2Eatn,axiom,( mem(c_2Etransc_2Eatn,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Etransc_2Ecos,axiom,( mem(c_2Etransc_2Ecos,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(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))) )).
fof(mem_c_2Etransc_2Edsize,axiom,( mem(c_2Etransc_2Edsize,arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),ty_2Enum_2Enum)) )).
fof(mem_c_2Etransc_2Eexp,axiom,( mem(c_2Etransc_2Eexp,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(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))) )).
fof(mem_c_2Etransc_2Egauge,axiom,( mem(c_2Etransc_2Egauge,arr(arr(ty_2Erealax_2Ereal,bool),arr(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),bool))) )).
fof(mem_c_2Etransc_2Eln,axiom,( mem(c_2Etransc_2Eln,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Etransc_2Epi,axiom,( mem(c_2Etransc_2Epi,ty_2Erealax_2Ereal) )).
fof(mem_c_2Etransc_2Eroot,axiom,( mem(c_2Etransc_2Eroot,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Etransc_2Erpow,axiom,( mem(c_2Etransc_2Erpow,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(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))) )).
fof(mem_c_2Etransc_2Esin,axiom,( mem(c_2Etransc_2Esin,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Etransc_2Esqrt,axiom,( mem(c_2Etransc_2Esqrt,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Etransc_2Etan,axiom,( mem(c_2Etransc_2Etan,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(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))) )).
fof(ax_thm_2Etransc_2Eexp,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eexp,V0x) = ap(c_2Eseq_2Esuminf,f2958(V0x)) ) )).
fof(ax_thm_2Etransc_2Ecos,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Eseq_2Esuminf,f2960(V0x)) ) )).
fof(ax_thm_2Etransc_2Esin,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esin,V0x) = ap(c_2Eseq_2Esuminf,f2962(V0x)) ) )).
fof(conj_thm_2Etransc_2EEXP__CONVERGES,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Eseq_2Esums,f2958(V0x)),ap(c_2Etransc_2Eexp,V0x))) ))).
fof(conj_thm_2Etransc_2ESIN__CONVERGES,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Eseq_2Esums,f2962(V0x)),ap(c_2Etransc_2Esin,V0x))) ))).
fof(conj_thm_2Etransc_2ECOS__CONVERGES,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Eseq_2Esums,f2960(V0x)),ap(c_2Etransc_2Ecos,V0x))) ))).
fof(conj_thm_2Etransc_2EEXP__FDIFF,lemma,(( ap(c_2Epowser_2Ediffs,f2963) = f2964 ))).
fof(conj_thm_2Etransc_2ESIN__FDIFF,lemma,(( ap(c_2Epowser_2Ediffs,f2965) = f2966 ))).
fof(conj_thm_2Etransc_2ECOS__FDIFF,lemma,(( ap(c_2Epowser_2Ediffs,f2967) = f2968 ))).
fof(conj_thm_2Etransc_2ESIN__NEGLEMMA,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,V0x)) = ap(c_2Eseq_2Esuminf,f2969(V0x)) ) ))).
fof(conj_thm_2Etransc_2EDIFF__EXP,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Eexp),ap(c_2Etransc_2Eexp,V0x)),V0x)) ))).
fof(conj_thm_2Etransc_2EDIFF__SIN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Esin),ap(c_2Etransc_2Ecos,V0x)),V0x)) ))).
fof(conj_thm_2Etransc_2EDIFF__COS,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Ecos),ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,V0x))),V0x)) ))).
fof(conj_thm_2Etransc_2EDIFF__COMPOSITE,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3g] : ( mem(V3g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V4m] : ( mem(V4m,ty_2Erealax_2Ereal) => ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ( ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V0f),V1l),V2x)) & ( ~~ ( ap(V0f,V2x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) => p(ap(ap(ap(c_2Elim_2Ediffl,f2970(V0f)),ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,V1l),ap(ap(c_2Ereal_2Epow,ap(V0f,V2x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V2x)) ) & ( ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V0f),V1l),V2x)) & ( p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),V2x)) & ( ~~ ( ap(V3g,V2x) = ap(c_2Ereal_2Ereal__of__num,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,V1l),ap(V3g,V2x))),ap(ap(c_2Erealax_2Ereal__mul,V4m),ap(V0f,V2x)))),ap(ap(c_2Ereal_2Epow,ap(V3g,V2x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),V2x)) ) & ( ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V0f),V1l),V2x)) & p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),V2x)) ) => p(ap(ap(ap(c_2Elim_2Ediffl,f2972(V0f,V3g)),ap(ap(c_2Erealax_2Ereal__add,V1l),V4m)),V2x)) ) & ( ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V0f),V1l),V2x)) & p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),V2x)) ) => p(ap(ap(ap(c_2Elim_2Ediffl,f2973(V0f,V3g)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1l),ap(V3g,V2x))),ap(ap(c_2Erealax_2Ereal__mul,V4m),ap(V0f,V2x)))),V2x)) ) & ( ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V0f),V1l),V2x)) & p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),V2x)) ) => p(ap(ap(ap(c_2Elim_2Ediffl,f2974(V0f,V3g)),ap(ap(c_2Ereal_2Ereal__sub,V1l),V4m)),V2x)) ) & ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V0f),V1l),V2x)) => p(ap(ap(ap(c_2Elim_2Ediffl,f2975(V0f)),ap(c_2Erealax_2Ereal__neg,V1l)),V2x)) ) & ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),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,V5n)),ap(ap(c_2Ereal_2Epow,ap(V3g,V2x)),ap(ap(c_2Earithmetic_2E_2D,V5n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),V4m)),V2x)) ) & ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),V2x)) => p(ap(ap(ap(c_2Elim_2Ediffl,f2977(V3g)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,ap(V3g,V2x))),V4m)),V2x)) ) & ( ( p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),V2x)) => p(ap(ap(ap(c_2Elim_2Ediffl,f2978(V3g)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,ap(V3g,V2x))),V4m)),V2x)) ) & ( p(ap(ap(ap(c_2Elim_2Ediffl,V3g),V4m),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,V2x)))),V4m)),V2x)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__0,lemma,(( ap(c_2Etransc_2Eexp,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Etransc_2EEXP__LE__X,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),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,c_2Earithmetic_2EZERO)))),V0x)),ap(c_2Etransc_2Eexp,V0x))) ) ))).
fof(conj_thm_2Etransc_2EEXP__LT__1,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Etransc_2Eexp,V0x))) ) ))).
fof(conj_thm_2Etransc_2EEXP__ADD__MUL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y))),ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,V0x))) = ap(c_2Etransc_2Eexp,V1y) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__NEG__MUL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,V0x)),ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,V0x))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Etransc_2EEXP__NEG__MUL2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,V0x))),ap(c_2Etransc_2Eexp,V0x)) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Etransc_2EEXP__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eexp,ap(c_2Erealax_2Ereal__neg,V0x)) = ap(c_2Erealax_2Einv,ap(c_2Etransc_2Eexp,V0x)) ) ))).
fof(conj_thm_2Etransc_2EEXP__ADD,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Eexp,V0x)),ap(c_2Etransc_2Eexp,V1y)) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__POS__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eexp,V0x))) ))).
fof(conj_thm_2Etransc_2EEXP__NZ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ~~ ( ap(c_2Etransc_2Eexp,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__POS__LT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eexp,V0x))) ))).
fof(conj_thm_2Etransc_2EEXP__N,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eexp,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V0n)),V1x)) = ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Eexp,V1x)),V0n) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__SUB,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eexp,ap(ap(c_2Ereal_2Ereal__sub,V0x),V1y)) = ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eexp,V0x)),ap(c_2Etransc_2Eexp,V1y)) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__MONO__IMP,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V0x),V1y)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eexp,V0x)),ap(c_2Etransc_2Eexp,V1y))) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__MONO__LT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eexp,V0x)),ap(c_2Etransc_2Eexp,V1y))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,V0x),V1y)) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__MONO__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eexp,V0x)),ap(c_2Etransc_2Eexp,V1y))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__INJ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( ap(c_2Etransc_2Eexp,V0x) = ap(c_2Etransc_2Eexp,V1y) ) <=> ( V0x = V1y ) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__TOTAL__LEMMA,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0y)) => ? [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & ( p(ap(ap(c_2Ereal_2Ereal__lte,V1x),ap(ap(c_2Ereal_2Ereal__sub,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) & ( ap(c_2Etransc_2Eexp,V1x) = V0y ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EEXP__TOTAL,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0y)) => ? [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) & ( ap(c_2Etransc_2Eexp,V1x) = V0y ) ) ) ))).
fof(ax_thm_2Etransc_2Eln,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eln,V0x) = ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2980(V0x)) ) )).
fof(conj_thm_2Etransc_2ELN__EXP,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eln,ap(c_2Etransc_2Eexp,V0x)) = V0x ) ))).
fof(conj_thm_2Etransc_2EEXP__LN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ap(c_2Etransc_2Eexp,ap(c_2Etransc_2Eln,V0x)) = V0x ) <=> p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) ) ))).
fof(conj_thm_2Etransc_2ELN__MUL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( ap(c_2Etransc_2Eln,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)) = ap(ap(c_2Erealax_2Ereal__add,ap(c_2Etransc_2Eln,V0x)),ap(c_2Etransc_2Eln,V1y)) ) ) ) ))).
fof(conj_thm_2Etransc_2ELN__INJ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( ( ap(c_2Etransc_2Eln,V0x) = ap(c_2Etransc_2Eln,V1y) ) <=> ( V0x = V1y ) ) ) ) ))).
fof(conj_thm_2Etransc_2ELN__1,lemma,(( ap(c_2Etransc_2Eln,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2ELN__INV,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(c_2Etransc_2Eln,ap(c_2Erealax_2Einv,V0x)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Eln,V0x)) ) ) ))).
fof(conj_thm_2Etransc_2ELN__DIV,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( ap(c_2Etransc_2Eln,ap(ap(c_2Ereal_2E_2F,V0x),V1y)) = ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Eln,V0x)),ap(c_2Etransc_2Eln,V1y)) ) ) ) ))).
fof(conj_thm_2Etransc_2ELN__MONO__LT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eln,V0x)),ap(c_2Etransc_2Eln,V1y))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2Etransc_2ELN__MONO__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eln,V0x)),ap(c_2Etransc_2Eln,V1y))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2Etransc_2ELN__POW,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => ( ap(c_2Etransc_2Eln,ap(ap(c_2Ereal_2Epow,V1x),V0n)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V0n)),ap(c_2Etransc_2Eln,V1x)) ) ) ) ))).
fof(conj_thm_2Etransc_2ELN__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),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,c_2Earithmetic_2EZERO)))),V0x))),V0x)) ) ))).
fof(conj_thm_2Etransc_2ELN__LT__X,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eln,V0x)),V0x)) ) ))).
fof(conj_thm_2Etransc_2ELN__POS,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0x)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eln,V0x))) ) ))).
fof(ax_thm_2Etransc_2Eroot,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Etransc_2Eroot,V0n),V1x) = ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2981(V0n,V1x)) ) ) )).
fof(ax_thm_2Etransc_2Esqrt,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esqrt,V0x) = ap(ap(c_2Etransc_2Eroot,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V0x) ) )).
fof(conj_thm_2Etransc_2EROOT__LT__LEMMA,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => ( ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Eexp,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eln,V1x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Enum_2ESUC,V0n))))),ap(c_2Enum_2ESUC,V0n)) = V1x ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__LN,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x) = ap(c_2Etransc_2Eexp,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eln,V1x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Enum_2ESUC,V0n)))) ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__0,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Etransc_2EROOT__1,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Etransc_2EROOT__POS__LT,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x))) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__POW__POS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => ( ap(ap(c_2Ereal_2Epow,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x)),ap(c_2Enum_2ESUC,V0n)) = V1x ) ) ) ))).
fof(conj_thm_2Etransc_2EPOW__ROOT__POS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),ap(ap(c_2Ereal_2Epow,V1x),ap(c_2Enum_2ESUC,V0n))) = V1x ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__POS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x))) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__POS__UNIQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2y)) & ( ap(ap(c_2Ereal_2Epow,V2y),ap(c_2Enum_2ESUC,V0n)) = V1x ) ) ) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x) = V2y ) ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__MUL,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2y)) ) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),ap(ap(c_2Erealax_2Ereal__mul,V1x),V2y)) = ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x)),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V2y)) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__INV,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),ap(c_2Erealax_2Einv,V1x)) = ap(c_2Erealax_2Einv,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x)) ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__DIV,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2y)) ) => ( ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),ap(ap(c_2Ereal_2E_2F,V1x),V2y)) = ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x)),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V2y)) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EROOT__MONO__LE,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V1x),V2y)) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V1x)),ap(ap(c_2Etransc_2Eroot,ap(c_2Enum_2ESUC,V0n)),V2y))) ) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__0,lemma,(( ap(c_2Etransc_2Esqrt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2ESQRT__1,lemma,(( ap(c_2Etransc_2Esqrt,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Etransc_2ESQRT__POS__LT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esqrt,V0x))) ) ))).
fof(conj_thm_2Etransc_2ESQRT__POS__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esqrt,V0x))) ) ))).
fof(conj_thm_2Etransc_2ESQRT__POW2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esqrt,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = V0x ) <=> p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) ) ))).
fof(conj_thm_2Etransc_2ESQRT__POW__2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esqrt,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = V0x ) ) ))).
fof(conj_thm_2Etransc_2EPOW__2__SQRT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Epow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = V0x ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__POS__UNIQ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) & ( ap(ap(c_2Ereal_2Epow,V1y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = V0x ) ) ) => ( ap(c_2Etransc_2Esqrt,V0x) = V1y ) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__MUL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( ap(c_2Etransc_2Esqrt,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esqrt,V0x)),ap(c_2Etransc_2Esqrt,V1y)) ) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__INV,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(c_2Etransc_2Esqrt,ap(c_2Erealax_2Einv,V0x)) = ap(c_2Erealax_2Einv,ap(c_2Etransc_2Esqrt,V0x)) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__DIV,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => ( ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2E_2F,V0x),V1y)) = ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Esqrt,V0x)),ap(c_2Etransc_2Esqrt,V1y)) ) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__MONO__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Esqrt,V0x)),ap(c_2Etransc_2Esqrt,V1y))) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__EVEN__POW2,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,V0n)) => ( ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0n)) = ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2EDIV,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ) ))).
fof(conj_thm_2Etransc_2EREAL__DIV__SQRT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(ap(c_2Ereal_2E_2F,V0x),ap(c_2Etransc_2Esqrt,V0x)) = ap(c_2Etransc_2Esqrt,V0x) ) ) ))).
fof(conj_thm_2Etransc_2ESQRT__EQ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( ( ap(ap(c_2Ereal_2Epow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = V1y ) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) ) => ( V0x = ap(c_2Etransc_2Esqrt,V1y) ) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__0,lemma,(( ap(c_2Etransc_2Esin,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2ECOS__0,lemma,(( ap(c_2Etransc_2Ecos,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Etransc_2ESIN__CIRCLE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Etransc_2ESIN__BOUND,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Etransc_2Esin,V0x))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ))).
fof(conj_thm_2Etransc_2ESIN__BOUNDS,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),ap(c_2Etransc_2Esin,V0x))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Esin,V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ))).
fof(conj_thm_2Etransc_2ECOS__BOUND,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Etransc_2Ecos,V0x))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ))).
fof(conj_thm_2Etransc_2ECOS__BOUNDS,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),ap(c_2Etransc_2Ecos,V0x))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ))).
fof(conj_thm_2Etransc_2ESIN__COS__ADD,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,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,V0x),V1y))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,V0x)),ap(c_2Etransc_2Ecos,V1y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V1y))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y))),ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Ecos,V1y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,V0x)),ap(c_2Etransc_2Esin,V1y))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__COS__NEG,lemma,(! [V0x] : ( mem(V0x,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,V0x))),ap(c_2Etransc_2Esin,V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Etransc_2Ecos,ap(c_2Erealax_2Ereal__neg,V0x))),ap(c_2Etransc_2Ecos,V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Etransc_2ESIN__ADD,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,V0x)),ap(c_2Etransc_2Ecos,V1y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V1y))) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__ADD,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) = ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Ecos,V1y))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,V0x)),ap(c_2Etransc_2Esin,V1y))) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esin,ap(c_2Erealax_2Ereal__neg,V0x)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,V0x)) ) ))).
fof(conj_thm_2Etransc_2ECOS__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Ecos,ap(c_2Erealax_2Ereal__neg,V0x)) = ap(c_2Etransc_2Ecos,V0x) ) ))).
fof(conj_thm_2Etransc_2ESIN__DOUBLE,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO)))),V0x)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Esin,V0x)),ap(c_2Etransc_2Ecos,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__DOUBLE,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO)))),V0x)) = ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ))).
fof(conj_thm_2Etransc_2ESIN__PAIRED,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Eseq_2Esums,f2982(V0x)),ap(c_2Etransc_2Esin,V0x))) ))).
fof(conj_thm_2Etransc_2ESIN__POS,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esin,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__PAIRED,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => p(ap(ap(c_2Eseq_2Esums,f2983(V0x)),ap(c_2Etransc_2Ecos,V0x))) ))).
fof(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,c_2Earithmetic_2EZERO))))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))))).
fof(conj_thm_2Etransc_2ECOS__ISZERO,lemma,(p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2984)))).
fof(ax_thm_2Etransc_2Epi,axiom, ( c_2Etransc_2Epi = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2984)) )).
fof(conj_thm_2Etransc_2EPI2,lemma,(( ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2984) ))).
fof(conj_thm_2Etransc_2ECOS__PI2,lemma,(( ap(c_2Etransc_2Ecos,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2EPI2__BOUNDS,lemma,(( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ))).
fof(conj_thm_2Etransc_2EPI__POS,lemma,(p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),c_2Etransc_2Epi)))).
fof(conj_thm_2Etransc_2ESIN__PI2,lemma,(( ap(c_2Etransc_2Esin,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Etransc_2ECOS__PI,lemma,(( ap(c_2Etransc_2Ecos,c_2Etransc_2Epi) = ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ))).
fof(conj_thm_2Etransc_2ESIN__PI,lemma,(( ap(c_2Etransc_2Esin,c_2Etransc_2Epi) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2ESIN__COS,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esin,V0x) = ap(c_2Etransc_2Ecos,ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),V0x)) ) ))).
fof(conj_thm_2Etransc_2ECOS__SIN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Etransc_2Esin,ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),V0x)) ) ))).
fof(conj_thm_2Etransc_2ESIN__PERIODIC__PI,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,V0x),c_2Etransc_2Epi)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Esin,V0x)) ) ))).
fof(conj_thm_2Etransc_2ECOS__PERIODIC__PI,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,V0x),c_2Etransc_2Epi)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Ecos,V0x)) ) ))).
fof(conj_thm_2Etransc_2ESIN__PERIODIC,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),c_2Etransc_2Epi))) = ap(c_2Etransc_2Esin,V0x) ) ))).
fof(conj_thm_2Etransc_2ECOS__PERIODIC,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),c_2Etransc_2Epi))) = ap(c_2Etransc_2Ecos,V0x) ) ))).
fof(conj_thm_2Etransc_2ECOS__NPI,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V0n)),c_2Etransc_2Epi)) = ap(ap(c_2Ereal_2Epow,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0n) ) ))).
fof(conj_thm_2Etransc_2ESIN__NPI,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V0n)),c_2Etransc_2Epi)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Etransc_2ESIN__POS__PI2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esin,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__POS__PI2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Ecos,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__POS__PI,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Ecos,V0x))) ) ))).
fof(conj_thm_2Etransc_2ESIN__POS__PI,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),c_2Etransc_2Epi)) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esin,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__POS__PI2__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Ecos,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__POS__PI__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Ecos,V0x))) ) ))).
fof(conj_thm_2Etransc_2ESIN__POS__PI2__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esin,V0x))) ) ))).
fof(conj_thm_2Etransc_2ESIN__POS__PI__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),c_2Etransc_2Epi)) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esin,V0x))) ) ))).
fof(conj_thm_2Etransc_2ECOS__TOTAL,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2985(V0y))) ) ))).
fof(conj_thm_2Etransc_2ESIN__TOTAL,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2986(V0y))) ) ))).
fof(conj_thm_2Etransc_2ECOS__ZERO__LEMMA,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( ( ~~ p(ap(c_2Earithmetic_2EEVEN,V1n)) ) & ( V0x = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__ZERO__LEMMA,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & ( ap(c_2Etransc_2Esin,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( p(ap(c_2Earithmetic_2EEVEN,V1n)) & ( V0x = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__ZERO,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) <=> ( ( ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( ( ~~ p(ap(c_2Earithmetic_2EEVEN,V1n)) ) & ( V0x = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ) ) | ? [V2n] : ( mem(V2n,ty_2Enum_2Enum) & ( ( ~~ p(ap(c_2Earithmetic_2EEVEN,V2n)) ) & ( V0x = ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V2n)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__ZERO,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ap(c_2Etransc_2Esin,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) <=> ( ( ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( p(ap(c_2Earithmetic_2EEVEN,V1n)) & ( V0x = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ) ) | ? [V2n] : ( mem(V2n,ty_2Enum_2Enum) & ( p(ap(c_2Earithmetic_2EEVEN,V2n)) & ( V0x = ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V2n)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ) ) ) ) ))).
fof(ax_thm_2Etransc_2Etan,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Etan,V0x) = ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Esin,V0x)),ap(c_2Etransc_2Ecos,V0x)) ) )).
fof(conj_thm_2Etransc_2ETAN__0,lemma,(( ap(c_2Etransc_2Etan,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2ETAN__PI,lemma,(( ap(c_2Etransc_2Etan,c_2Etransc_2Epi) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Etransc_2ETAN__NPI,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V0n)),c_2Etransc_2Epi)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Etransc_2ETAN__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Etan,ap(c_2Erealax_2Ereal__neg,V0x)) = ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Etan,V0x)) ) ))).
fof(conj_thm_2Etransc_2ETAN__PERIODIC,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),c_2Etransc_2Epi))) = ap(c_2Etransc_2Etan,V0x) ) ))).
fof(conj_thm_2Etransc_2ETAN__ADD,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( ( ~~ ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & ( ( ~~ ( ap(c_2Etransc_2Ecos,V1y) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & ( ~~ ( ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) => ( ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) = ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Erealax_2Ereal__add,ap(c_2Etransc_2Etan,V0x)),ap(c_2Etransc_2Etan,V1y))),ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Etransc_2Etan,V0x)),ap(c_2Etransc_2Etan,V1y)))) ) ) ) ))).
fof(conj_thm_2Etransc_2ETAN__DOUBLE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ( ~~ ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & ( ~~ ( ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0x)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) => ( ap(c_2Etransc_2Etan,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0x)) = 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,c_2Earithmetic_2EZERO)))),ap(c_2Etransc_2Etan,V0x))),ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Etan,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Etransc_2ETAN__POS__PI2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Etan,V0x))) ) ))).
fof(conj_thm_2Etransc_2EDIFF__TAN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ~~ ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Ereal_2Ereal__of__num,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,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),V0x)) ) ))).
fof(conj_thm_2Etransc_2ETAN__TOTAL__LEMMA,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0y)) => ? [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & ( p(ap(ap(c_2Erealax_2Ereal__lt,V1x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Erealax_2Ereal__lt,V0y),ap(c_2Etransc_2Etan,V1x))) ) ) ) ) ))).
fof(conj_thm_2Etransc_2ETAN__TOTAL__POS,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0y)) => ? [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1x)) & ( p(ap(ap(c_2Erealax_2Ereal__lt,V1x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & ( ap(c_2Etransc_2Etan,V1x) = V0y ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2ETAN__TOTAL,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => p(ap(c_2Ebool_2E_3F_21(ty_2Erealax_2Ereal),f2987(V0y))) ))).
fof(ax_thm_2Etransc_2Easn,axiom, ! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Easn,V0y) = ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2986(V0y)) ) )).
fof(ax_thm_2Etransc_2Eacs,axiom, ! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eacs,V0y) = ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2985(V0y)) ) )).
fof(ax_thm_2Etransc_2Eatn,axiom, ! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Eatn,V0y) = ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f2987(V0y)) ) )).
fof(conj_thm_2Etransc_2EASN,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Easn,V0y))) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Easn,V0y)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & ( ap(c_2Etransc_2Esin,ap(c_2Etransc_2Easn,V0y)) = V0y ) ) ) ) ))).
fof(conj_thm_2Etransc_2EASN__SIN,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( ap(c_2Etransc_2Esin,ap(c_2Etransc_2Easn,V0y)) = V0y ) ) ))).
fof(conj_thm_2Etransc_2EASN__BOUNDS,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Easn,V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Easn,V0y)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ) ))).
fof(conj_thm_2Etransc_2EASN__BOUNDS__LT,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Easn,V0y))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Easn,V0y)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__ASN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => ( ap(c_2Etransc_2Easn,ap(c_2Etransc_2Esin,V0x)) = V0x ) ) ))).
fof(conj_thm_2Etransc_2EACS,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eacs,V0y))) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eacs,V0y)),c_2Etransc_2Epi)) & ( ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eacs,V0y)) = V0y ) ) ) ) ))).
fof(conj_thm_2Etransc_2EACS__COS,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eacs,V0y)) = V0y ) ) ))).
fof(conj_thm_2Etransc_2EACS__BOUNDS,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eacs,V0y))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eacs,V0y)),c_2Etransc_2Epi)) ) ) ))).
fof(conj_thm_2Etransc_2EACS__BOUNDS__LT,lemma,(! [V0y] : ( mem(V0y,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,c_2Earithmetic_2EZERO))))),V0y)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0y),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eacs,V0y))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eacs,V0y)),c_2Etransc_2Epi)) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__ACS,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),c_2Etransc_2Epi)) ) => ( ap(c_2Etransc_2Eacs,ap(c_2Etransc_2Ecos,V0x)) = V0x ) ) ))).
fof(conj_thm_2Etransc_2EATN,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Eatn,V0y))) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eatn,V0y)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & ( ap(c_2Etransc_2Etan,ap(c_2Etransc_2Eatn,V0y)) = V0y ) ) ) ))).
fof(conj_thm_2Etransc_2EATN__TAN,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( ap(c_2Etransc_2Etan,ap(c_2Etransc_2Eatn,V0y)) = V0y ) ))).
fof(conj_thm_2Etransc_2EATN__BOUNDS,lemma,(! [V0y] : ( mem(V0y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Eatn,V0y))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Etransc_2Eatn,V0y)),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ))).
fof(conj_thm_2Etransc_2ETAN__ATN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => ( ap(c_2Etransc_2Eatn,ap(c_2Etransc_2Etan,V0x)) = V0x ) ) ))).
fof(conj_thm_2Etransc_2ETAN__SEC,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ~~ ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Erealax_2Ereal__add,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Etan,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(ap(c_2Ereal_2Epow,ap(c_2Erealax_2Einv,ap(c_2Etransc_2Ecos,V0x))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__COS__SQ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),c_2Etransc_2Epi)) ) => ( ap(c_2Etransc_2Esin,V0x) = ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__SIN__SQ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V0x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) => ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__ATN__NZ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ~~ ( ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eatn,V0x)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__ASN__NZ,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( ~~ ( ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Easn,V0x)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__ACS__NZ,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => ( ~~ ( ap(c_2Etransc_2Esin,ap(c_2Etransc_2Eacs,V0x)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Etransc_2ECOS__SIN__SQRT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Ecos,V0x))) => ( ap(c_2Etransc_2Ecos,V0x) = ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Esin,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Etransc_2ESIN__COS__SQRT,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Esin,V0x))) => ( ap(c_2Etransc_2Esin,V0x) = ap(c_2Etransc_2Esqrt,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Etransc_2Ecos,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Etransc_2EDIFF__LN,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(ap(c_2Elim_2Ediffl,c_2Etransc_2Eln),ap(c_2Erealax_2Einv,V0x)),V0x)) ) ))).
fof(conj_thm_2Etransc_2EDIFF__ASN__LEMMA,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,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,V0x)))),V0x)) ) ))).
fof(conj_thm_2Etransc_2EDIFF__ASN,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,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,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))))),V0x)) ) ))).
fof(conj_thm_2Etransc_2EDIFF__ACS__LEMMA,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,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,V0x))))),V0x)) ) ))).
fof(conj_thm_2Etransc_2EDIFF__ACS,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO))))),V0x)) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,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,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))))),V0x)) ) ))).
fof(conj_thm_2Etransc_2EDIFF__ATN,lemma,(! [V0x] : ( mem(V0x,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,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),V0x)) ))).
fof(ax_thm_2Etransc_2Edivision,axiom, ! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ! [V2D] : ( 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),V0a),V1b)),V2D)) <=> ( ( ap(V2D,c_2Enum_2E0) = V0a ) & ? [V3N] : ( mem(V3N,ty_2Enum_2Enum) & ( ( ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V4n),V3N)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V2D,V4n)),ap(V2D,ap(c_2Enum_2ESUC,V4n)))) ) ) ) & ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E_3D,V5n),V3N)) => ( ap(V2D,V5n) = V1b ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Etransc_2Edsize,axiom, ! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ap(c_2Etransc_2Edsize,V0D) = ap(c_2Emin_2E_40(ty_2Enum_2Enum),f2990(V0D)) ) )).
fof(ax_thm_2Etransc_2Etdiv,axiom, ! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ! [V2D] : ( mem(V2D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V3p] : ( 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),V0a),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),V0a),V1b)),V2D)) & ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(V2D,V4n)),ap(V3p,V4n))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(V3p,V4n)),ap(V2D,ap(c_2Enum_2ESUC,V4n)))) ) ) ) ) ) ) ) )).
fof(ax_thm_2Etransc_2Egauge,axiom, ! [V0E] : ( mem(V0E,arr(ty_2Erealax_2Ereal,bool)) => ! [V1g] : ( mem(V1g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( p(ap(ap(c_2Etransc_2Egauge,V0E),V1g)) <=> ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ( p(ap(V0E,V2x)) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(V1g,V2x))) ) ) ) ) )).
fof(ax_thm_2Etransc_2Efine,axiom, ! [V0g] : ( mem(V0g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1D] : ( mem(V1D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V2p] : ( 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] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,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,V3n))),ap(V1D,V3n))),ap(V0g,ap(V2p,V3n)))) ) ) ) ) ) )).
fof(ax_thm_2Etransc_2Ersum,axiom, ! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1p] : ( mem(V1p,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V2f] : ( mem(V2f,arr(ty_2Erealax_2Ereal,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) = ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),ap(c_2Etransc_2Edsize,V0D))),f2991(V1p,V2f,V0D)) ) ) ) )).
fof(ax_thm_2Etransc_2EDint,axiom, ! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ! [V2f] : ( mem(V2f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3k] : ( mem(V3k,ty_2Erealax_2Ereal) => ( p(ap(ap(ap(c_2Etransc_2EDint,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0a),V1b)),V2f),V3k)) <=> ! [V4e] : ( mem(V4e,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V4e)) => ? [V5g] : ( mem(V5g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) & ( p(ap(ap(c_2Etransc_2Egauge,f2992(V0a,V1b)),V5g)) & ! [V7D] : ( mem(V7D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V8p] : ( 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),V0a),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)),V3k))),V4e)) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Etransc_2EDIVISION__0,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ( ( V0a = V1b ) => ( ap(c_2Etransc_2Edsize,f2993(V0a,V1b)) = c_2Enum_2E0 ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__1,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V0a),V1b)) => ( ap(c_2Etransc_2Edsize,f2993(V0a,V1b)) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__SINGLE,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,V0a),V1b)) => p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0a),V1b)),f2993(V0a,V1b))) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__LHS,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ( ap(V0D,c_2Enum_2E0) = V1a ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__THM,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) <=> ( ( ap(V0D,c_2Enum_2E0) = V1a ) & ( ( ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(c_2Etransc_2Edsize,V0D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,V3n)),ap(V0D,ap(c_2Enum_2ESUC,V3n)))) ) ) ) & ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E_3D,V4n),ap(c_2Etransc_2Edsize,V0D))) => ( ap(V0D,V4n) = V2b ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__RHS,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ( ap(V0D,ap(c_2Etransc_2Edsize,V0D)) = V2b ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__LT__GEN,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) & ( p(ap(ap(c_2Eprim__rec_2E_3C,V3m),V4n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V4n),ap(c_2Etransc_2Edsize,V0D))) ) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,V3m)),ap(V0D,V4n))) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__LT,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(c_2Etransc_2Edsize,V0D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,c_2Enum_2E0)),ap(V0D,ap(c_2Enum_2ESUC,V3n)))) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__LE,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => p(ap(ap(c_2Ereal_2Ereal__lte,V1a),V2b)) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__GT,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(c_2Etransc_2Edsize,V0D))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,V3n)),ap(V0D,ap(c_2Etransc_2Edsize,V0D)))) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__EQ,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ( ( V1a = V2b ) <=> ( ap(c_2Etransc_2Edsize,V0D) = c_2Enum_2E0 ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__LBOUND,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ! [V3r] : ( mem(V3r,ty_2Enum_2Enum) => p(ap(ap(c_2Ereal_2Ereal__lte,V1a),ap(V0D,V3r))) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__LBOUND__LT,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) & ( ~~ ( ap(c_2Etransc_2Edsize,V0D) = c_2Enum_2E0 ) ) ) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => p(ap(ap(c_2Erealax_2Ereal__lt,V1a),ap(V0D,ap(c_2Enum_2ESUC,V3n)))) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__UBOUND,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) => ! [V3r] : ( mem(V3r,ty_2Enum_2Enum) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0D,V3r)),V2b)) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__UBOUND__LT,lemma,(! [V0D] : ( mem(V0D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Etransc_2Edivision,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V2b)),V0D)) & p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(c_2Etransc_2Edsize,V0D))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(V0D,V3n)),V2b)) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__APPEND,lemma,(! [V0g] : ( mem(V0g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ! [V3c] : ( mem(V3c,ty_2Erealax_2Ereal) => ( ( ( ? [V4D1] : ( mem(V4D1,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V5p1] : ( 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),V1a),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] : ( mem(V6D2,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V7p2] : ( 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),V2b),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] : ( mem(V8D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V9p] : ( 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),V1a),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))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDIVISION__EXISTS,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ! [V2g] : ( mem(V2g,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,V0a),V1b)) & p(ap(ap(c_2Etransc_2Egauge,f2994(V0a,V1b)),V2g)) ) => ? [V4D] : ( mem(V4D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) & ? [V5p] : ( 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),V0a),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))) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EGAUGE__MIN,lemma,(! [V0E] : ( mem(V0E,arr(ty_2Erealax_2Ereal,bool)) => ! [V1g1] : ( mem(V1g1,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2g2] : ( 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))) ) ) ) ))).
fof(conj_thm_2Etransc_2EFINE__MIN,lemma,(! [V0g1] : ( mem(V0g1,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1g2] : ( mem(V1g2,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2D] : ( mem(V2D,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V3p] : ( 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))) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EDINT__UNIQ,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ! [V2f] : ( mem(V2f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3k1] : ( mem(V3k1,ty_2Erealax_2Ereal) => ! [V4k2] : ( mem(V4k2,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,V0a),V1b)) & ( p(ap(ap(ap(c_2Etransc_2EDint,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0a),V1b)),V2f),V3k1)) & p(ap(ap(ap(c_2Etransc_2EDint,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0a),V1b)),V2f),V4k2)) ) ) => ( V3k1 = V4k2 ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EINTEGRAL__NULL,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => p(ap(ap(ap(c_2Etransc_2EDint,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V1a),V1a)),V0f),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2Etransc_2EFTC1,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1f_27] : ( mem(V1f_27,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2a] : ( mem(V2a,ty_2Erealax_2Ereal) => ! [V3b] : ( mem(V3b,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,V2a),V3b)) & ! [V4x] : ( mem(V4x,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,V2a),V4x)) & p(ap(ap(c_2Ereal_2Ereal__lte,V4x),V3b)) ) => p(ap(ap(ap(c_2Elim_2Ediffl,V0f),ap(V1f_27,V4x)),V4x)) ) ) ) => p(ap(ap(ap(c_2Etransc_2EDint,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V2a),V3b)),V1f_27),ap(ap(c_2Ereal_2Ereal__sub,ap(V0f,V3b)),ap(V0f,V2a)))) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EMCLAURIN,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1diff] : ( mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ! [V2h] : ( mem(V2h,ty_2Erealax_2Ereal) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2h)) & ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V3n)) & ( ( ap(V1diff,c_2Enum_2E0) = V0f ) & ! [V4m] : ( mem(V4m,ty_2Enum_2Enum) => ! [V5t] : ( mem(V5t,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V4m),V3n)) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V5t)) & p(ap(ap(c_2Ereal_2Ereal__lte,V5t),V2h)) ) ) => p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,V4m)),ap(ap(V1diff,ap(c_2Enum_2ESUC,V4m)),V5t)),V5t)) ) ) ) ) ) ) => ? [V6t] : ( mem(V6t,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V6t)) & ( p(ap(ap(c_2Erealax_2Ereal__lt,V6t),V2h)) & ( ap(V0f,V2h) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),V3n)),f2997(V1diff,V2h))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,V3n),V6t)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,V3n)))),ap(ap(c_2Ereal_2Epow,V2h),V3n))) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EMCLAURIN__NEG,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1diff] : ( mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ! [V2h] : ( mem(V2h,ty_2Erealax_2Ereal) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,V2h),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V3n)) & ( ( ap(V1diff,c_2Enum_2E0) = V0f ) & ! [V4m] : ( mem(V4m,ty_2Enum_2Enum) => ! [V5t] : ( mem(V5t,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V4m),V3n)) & ( p(ap(ap(c_2Ereal_2Ereal__lte,V2h),V5t)) & p(ap(ap(c_2Ereal_2Ereal__lte,V5t),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) => p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,V4m)),ap(ap(V1diff,ap(c_2Enum_2ESUC,V4m)),V5t)),V5t)) ) ) ) ) ) ) => ? [V6t] : ( mem(V6t,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Erealax_2Ereal__lt,V2h),V6t)) & ( p(ap(ap(c_2Erealax_2Ereal__lt,V6t),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & ( ap(V0f,V2h) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),V3n)),f2997(V1diff,V2h))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,V3n),V6t)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,V3n)))),ap(ap(c_2Ereal_2Epow,V2h),V3n))) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EMCLAURIN__ALL__LT,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1diff] : ( mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ( ( ( ap(V1diff,c_2Enum_2E0) = V0f ) & ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,ty_2Erealax_2Ereal) => p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,V2m)),ap(ap(V1diff,ap(c_2Enum_2ESUC,V2m)),V3x)),V3x)) ) ) ) => ! [V4x] : ( mem(V4x,ty_2Erealax_2Ereal) => ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ( ( ( ~~ ( V4x = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V5n)) ) => ? [V6t] : ( mem(V6t,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ereal_2Eabs,V6t))) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,V6t)),ap(c_2Ereal_2Eabs,V4x))) & ( ap(V0f,V4x) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),V5n)),f2998(V1diff,V4x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,V5n),V6t)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,V5n)))),ap(ap(c_2Ereal_2Epow,V4x),V5n))) ) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EMCLAURIN__ZERO,lemma,(! [V0diff] : ( mem(V0diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ( ( ( V2x = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) => ( ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),V1n)),f2999(V0diff,V2x)) = ap(ap(V0diff,c_2Enum_2E0),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EMCLAURIN__ALL__LE,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1diff] : ( mem(V1diff,arr(ty_2Enum_2Enum,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) => ( ( ( ap(V1diff,c_2Enum_2E0) = V0f ) & ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,ty_2Erealax_2Ereal) => p(ap(ap(ap(c_2Elim_2Ediffl,ap(V1diff,V2m)),ap(ap(V1diff,ap(c_2Enum_2ESUC,V2m)),V3x)),V3x)) ) ) ) => ! [V4x] : ( mem(V4x,ty_2Erealax_2Ereal) => ! [V5n] : ( mem(V5n,ty_2Enum_2Enum) => ? [V6t] : ( mem(V6t,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,V6t)),ap(c_2Ereal_2Eabs,V4x))) & ( ap(V0f,V4x) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),V5n)),f2998(V1diff,V4x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(ap(V1diff,V5n),V6t)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,V5n)))),ap(ap(c_2Ereal_2Epow,V4x),V5n))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Etransc_2EMCLAURIN__EXP__LT,conjecture,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ( ~~ ( V0x = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) => ? [V2t] : ( mem(V2t,ty_2Erealax_2Ereal) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ereal_2Eabs,V2t))) & ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,V2t)),ap(c_2Ereal_2Eabs,V0x))) & ( ap(c_2Etransc_2Eexp,V0x) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Esum,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2E0),V1n)),f3000(V0x))),ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Ereal_2E_2F,ap(c_2Etransc_2Eexp,V2t)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2EFACT,V1n)))),ap(ap(c_2Ereal_2Epow,V0x),V1n))) ) ) ) ) ) ) ))).
