include('Axioms/iterate+2.ax').
fof(ne_ty_2Eextreal_2Eextreal,axiom,( ne(ty_2Eextreal_2Eextreal) )).
fof(mem_c_2Eextreal_2EEXTREAL__SUM__IMAGE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),arr(arr(A_27a,ty_2Eextreal_2Eextreal),arr(arr(A_27a,bool),ty_2Eextreal_2Eextreal))) ) )).
fof(mem_c_2Eextreal_2ENegInf,axiom,( mem(c_2Eextreal_2ENegInf,ty_2Eextreal_2Eextreal) )).
fof(mem_c_2Eextreal_2ENormal,axiom,( mem(c_2Eextreal_2ENormal,arr(ty_2Erealax_2Ereal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2EPosInf,axiom,( mem(c_2Eextreal_2EPosInf,ty_2Eextreal_2Eextreal) )).
fof(mem_c_2Eextreal_2EQ__set,axiom,( mem(c_2Eextreal_2EQ__set,arr(ty_2Eextreal_2Eextreal,bool)) )).
fof(mem_c_2Eextreal_2Eceiling,axiom,( mem(c_2Eextreal_2Eceiling,arr(ty_2Eextreal_2Eextreal,ty_2Enum_2Enum)) )).
fof(mem_c_2Eextreal_2Eext__mono__decreasing,axiom,( mem(c_2Eextreal_2Eext__mono__decreasing,arr(arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),bool)) )).
fof(mem_c_2Eextreal_2Eext__mono__increasing,axiom,( mem(c_2Eextreal_2Eext__mono__increasing,arr(arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),bool)) )).
fof(mem_c_2Eextreal_2Eext__suminf,axiom,( mem(c_2Eextreal_2Eext__suminf,arr(arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eextreal_2Eextreal__CASE(A_27a),arr(ty_2Eextreal_2Eextreal,arr(A_27a,arr(A_27a,arr(arr(ty_2Erealax_2Ereal,A_27a),A_27a))))) ) )).
fof(mem_c_2Eextreal_2Eextreal__abs,axiom,( mem(c_2Eextreal_2Eextreal__abs,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__add,axiom,( mem(c_2Eextreal_2Eextreal__add,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__ainv,axiom,( mem(c_2Eextreal_2Eextreal__ainv,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__div,axiom,( mem(c_2Eextreal_2Eextreal__div,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__exp,axiom,( mem(c_2Eextreal_2Eextreal__exp,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__inf,axiom,( mem(c_2Eextreal_2Eextreal__inf,arr(arr(ty_2Eextreal_2Eextreal,bool),ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__inv,axiom,( mem(c_2Eextreal_2Eextreal__inv,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__le,axiom,( mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))) )).
fof(mem_c_2Eextreal_2Eextreal__lg,axiom,( mem(c_2Eextreal_2Eextreal__lg,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__logr,axiom,( mem(c_2Eextreal_2Eextreal__logr,arr(ty_2Erealax_2Ereal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__lt,axiom,( mem(c_2Eextreal_2Eextreal__lt,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))) )).
fof(mem_c_2Eextreal_2Eextreal__max,axiom,( mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__min,axiom,( mem(c_2Eextreal_2Eextreal__min,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__mul,axiom,( mem(c_2Eextreal_2Eextreal__mul,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__of__num,axiom,( mem(c_2Eextreal_2Eextreal__of__num,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__pow,axiom,( mem(c_2Eextreal_2Eextreal__pow,arr(ty_2Eextreal_2Eextreal,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__size,axiom,( mem(c_2Eextreal_2Eextreal__size,arr(ty_2Eextreal_2Eextreal,ty_2Enum_2Enum)) )).
fof(mem_c_2Eextreal_2Eextreal__sqrt,axiom,( mem(c_2Eextreal_2Eextreal__sqrt,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Eextreal__sub,axiom,( mem(c_2Eextreal_2Eextreal__sub,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))) )).
fof(mem_c_2Eextreal_2Eextreal__sup,axiom,( mem(c_2Eextreal_2Eextreal__sup,arr(arr(ty_2Eextreal_2Eextreal,bool),ty_2Eextreal_2Eextreal)) )).
fof(mem_c_2Eextreal_2Emono__decreasing,axiom,( mem(c_2Eextreal_2Emono__decreasing,arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),bool)) )).
fof(mem_c_2Eextreal_2Emono__increasing,axiom,( mem(c_2Eextreal_2Emono__increasing,arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),bool)) )).
fof(mem_c_2Eextreal_2Eopen__interval,axiom,( mem(c_2Eextreal_2Eopen__interval,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool)))) )).
fof(mem_c_2Eextreal_2Eopen__intervals__set,axiom,( mem(c_2Eextreal_2Eopen__intervals__set,arr(arr(ty_2Eextreal_2Eextreal,bool),bool)) )).
fof(mem_c_2Eextreal_2Erational__intervals,axiom,( mem(c_2Eextreal_2Erational__intervals,arr(arr(ty_2Eextreal_2Eextreal,bool),bool)) )).
fof(mem_c_2Eextreal_2Ereal,axiom,( mem(c_2Eextreal_2Ereal,arr(ty_2Eextreal_2Eextreal,ty_2Erealax_2Ereal)) )).
fof(ax_thm_2Eextreal_2Eextreal__TY__DEF,axiom, ? [V0rep] : ( mem(V0rep,arr(ty_2Eextreal_2Eextreal,ty_2Eind__type_2Erecspace(ty_2Erealax_2Ereal))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(ty_2Erealax_2Ereal),ty_2Eextreal_2Eextreal),f3432),V0rep)) )).
fof(ax_thm_2Eextreal_2Eextreal__case__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0v] : ( mem(V0v,A_27a) => ! [V1v1] : ( mem(V1v1,A_27a) => ! [V2f] : ( mem(V2f,arr(ty_2Erealax_2Ereal,A_27a)) => ( ap(ap(ap(ap(c_2Eextreal_2Eextreal__CASE(A_27a),c_2Eextreal_2ENegInf),V0v),V1v1),V2f) = V0v ) ) ) ) ) & ( ( ! [V3v] : ( mem(V3v,A_27a) => ! [V4v1] : ( mem(V4v1,A_27a) => ! [V5f] : ( mem(V5f,arr(ty_2Erealax_2Ereal,A_27a)) => ( ap(ap(ap(ap(c_2Eextreal_2Eextreal__CASE(A_27a),c_2Eextreal_2EPosInf),V3v),V4v1),V5f) = V4v1 ) ) ) ) ) & ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ! [V7v] : ( mem(V7v,A_27a) => ! [V8v1] : ( mem(V8v1,A_27a) => ! [V9f] : ( mem(V9f,arr(ty_2Erealax_2Ereal,A_27a)) => ( ap(ap(ap(ap(c_2Eextreal_2Eextreal__CASE(A_27a),ap(c_2Eextreal_2ENormal,V6a)),V7v),V8v1),V9f) = ap(V9f,V6a) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__size__def,axiom, ( ( ap(c_2Eextreal_2Eextreal__size,c_2Eextreal_2ENegInf) = c_2Enum_2E0 ) & ( ( ap(c_2Eextreal_2Eextreal__size,c_2Eextreal_2EPosInf) = c_2Enum_2E0 ) & ! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ( ap(c_2Eextreal_2Eextreal__size,ap(c_2Eextreal_2ENormal,V0a)) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) )).
fof(conj_thm_2Eextreal_2Edatatype__extreal,lemma,(! [V0extreal] : ( mem(V0extreal,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,arr(arr(ty_2Erealax_2Ereal,ty_2Eextreal_2Eextreal),bool)))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(V0extreal,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf),c_2Eextreal_2ENormal))) ))).
fof(conj_thm_2Eextreal_2Eextreal__distinct,lemma,(( ( ~~ ( c_2Eextreal_2ENegInf = c_2Eextreal_2EPosInf ) ) & ( ( ! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ( ~~ ( c_2Eextreal_2ENegInf = ap(c_2Eextreal_2ENormal,V0a) ) ) ) ) & ! [V1a] : ( mem(V1a,ty_2Erealax_2Ereal) => ( ~~ ( c_2Eextreal_2EPosInf = ap(c_2Eextreal_2ENormal,V1a) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__nchotomy,lemma,(! [V0ee] : ( mem(V0ee,ty_2Eextreal_2Eextreal) => ( ( V0ee = c_2Eextreal_2ENegInf ) | ( ( V0ee = c_2Eextreal_2EPosInf ) | ? [V1r] : ( mem(V1r,ty_2Erealax_2Ereal) & ( V0ee = ap(c_2Eextreal_2ENormal,V1r) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f0] : ( mem(V0f0,A_27a) => ! [V1f1] : ( mem(V1f1,A_27a) => ! [V2f2] : ( mem(V2f2,arr(ty_2Erealax_2Ereal,A_27a)) => ? [V3fn] : ( mem(V3fn,arr(ty_2Eextreal_2Eextreal,A_27a)) & ( ( ap(V3fn,c_2Eextreal_2ENegInf) = V0f0 ) & ( ( ap(V3fn,c_2Eextreal_2EPosInf) = V1f1 ) & ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( ap(V3fn,ap(c_2Eextreal_2ENormal,V4a)) = ap(V2f2,V4a) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2Eextreal__induction,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eextreal_2Eextreal,bool)) => ( ( p(ap(V0P,c_2Eextreal_2ENegInf)) & ( p(ap(V0P,c_2Eextreal_2EPosInf)) & ! [V1r] : ( mem(V1r,ty_2Erealax_2Ereal) => p(ap(V0P,ap(c_2Eextreal_2ENormal,V1r))) ) ) ) => ! [V2e] : ( mem(V2e,ty_2Eextreal_2Eextreal) => p(ap(V0P,V2e)) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__case__cong,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0v_27] : ( mem(V0v_27,A_27a) => ! [V1v1_27] : ( mem(V1v1_27,A_27a) => ! [V2f_27] : ( mem(V2f_27,arr(ty_2Erealax_2Ereal,A_27a)) => ! [V3M] : ( mem(V3M,ty_2Eextreal_2Eextreal) => ! [V4M_27] : ( mem(V4M_27,ty_2Eextreal_2Eextreal) => ! [V5v] : ( mem(V5v,A_27a) => ! [V6v1] : ( mem(V6v1,A_27a) => ! [V7f] : ( mem(V7f,arr(ty_2Erealax_2Ereal,A_27a)) => ( ( ( V3M = V4M_27 ) & ( ( ( V4M_27 = c_2Eextreal_2ENegInf ) => ( V5v = V0v_27 ) ) & ( ( ( V4M_27 = c_2Eextreal_2EPosInf ) => ( V6v1 = V1v1_27 ) ) & ! [V8a] : ( mem(V8a,ty_2Erealax_2Ereal) => ( ( V4M_27 = ap(c_2Eextreal_2ENormal,V8a) ) => ( ap(V7f,V8a) = ap(V2f_27,V8a) ) ) ) ) ) ) => ( ap(ap(ap(ap(c_2Eextreal_2Eextreal__CASE(A_27a),V3M),V5v),V6v1),V7f) = ap(ap(ap(ap(c_2Eextreal_2Eextreal__CASE(A_27a),V4M_27),V0v_27),V1v1_27),V2f_27) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2Eextreal__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1v] : ( mem(V1v,A_27a) => ! [V2v1] : ( mem(V2v1,A_27a) => ! [V3f] : ( mem(V3f,arr(ty_2Erealax_2Ereal,A_27a)) => ! [V4v_27] : ( mem(V4v_27,A_27a) => ( ( ap(ap(ap(ap(c_2Eextreal_2Eextreal__CASE(A_27a),V0x),V1v),V2v1),V3f) = V4v_27 ) <=> ( ( ( V0x = c_2Eextreal_2ENegInf ) & ( V1v = V4v_27 ) ) | ( ( ( V0x = c_2Eextreal_2EPosInf ) & ( V2v1 = V4v_27 ) ) | ? [V5r] : ( mem(V5r,ty_2Erealax_2Ereal) & ( ( V0x = ap(c_2Eextreal_2ENormal,V5r) ) & ( ap(V3f,V5r) = V4v_27 ) ) ) ) ) ) ) ) ) ) )))).
fof(ax_thm_2Eextreal_2Eextreal__of__num__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Eextreal_2Eextreal__of__num,V0n) = ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,V0n)) ) )).
fof(ax_thm_2Eextreal_2Ereal__def,axiom, ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(c_2Eextreal_2Ereal,V0x) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Emin_2E_3D(ty_2Eextreal_2Eextreal),V0x),c_2Eextreal_2ENegInf)),ap(ap(c_2Emin_2E_3D(ty_2Eextreal_2Eextreal),V0x),c_2Eextreal_2EPosInf))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f3433(V0x))) ) )).
fof(conj_thm_2Eextreal_2Ereal__normal,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Eextreal_2Ereal,ap(c_2Eextreal_2ENormal,V0x)) = V0x ) ))).
fof(conj_thm_2Eextreal_2Enormal__real,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( ap(c_2Eextreal_2ENormal,ap(c_2Eextreal_2Ereal,V0x)) = V0x ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__add__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))) => ( ( ( ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V1x)),ap(c_2Eextreal_2ENormal,V2y))) ) ) ) & ( ( ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,c_2Eextreal_2EPosInf),V3a)) ) ) & ( p(ap(ap(V0P,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf)) & ( ( ! [V4v2] : ( mem(V4v2,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V4v2)),c_2Eextreal_2EPosInf)) ) ) & ( p(ap(ap(V0P,c_2Eextreal_2ENegInf),c_2Eextreal_2ENegInf)) & ( ( ! [V5v5] : ( mem(V5v5,ty_2Erealax_2Ereal) => p(ap(ap(V0P,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V5v5))) ) ) & ! [V6v3] : ( mem(V6v3,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V6v3)),c_2Eextreal_2ENegInf)) ) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Eextreal_2Eextreal) => ! [V8v1] : ( mem(V8v1,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__add__def,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ! [V3v2] : ( mem(V3v2,ty_2Erealax_2Ereal) => ! [V4v5] : ( mem(V4v5,ty_2Erealax_2Ereal) => ! [V5v3] : ( mem(V5v3,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2ENormal,V0x)),ap(c_2Eextreal_2ENormal,V1y)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) ) & ( ( ap(ap(c_2Eextreal_2Eextreal__add,c_2Eextreal_2EPosInf),V2a) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__add,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2ENormal,V3v2)),c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__add,c_2Eextreal_2ENegInf),c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__add,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V4v5)) = c_2Eextreal_2ENegInf ) & ( ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2ENormal,V5v3)),c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf ) ) ) ) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__sub__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))) => ( ( ( ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V1x)),ap(c_2Eextreal_2ENormal,V2y))) ) ) ) & ( ( ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,c_2Eextreal_2EPosInf),V3a)) ) ) & ( p(ap(ap(V0P,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf)) & ( ( ! [V4v2] : ( mem(V4v2,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V4v2)),c_2Eextreal_2EPosInf)) ) ) & ( p(ap(ap(V0P,c_2Eextreal_2ENegInf),c_2Eextreal_2ENegInf)) & ( ( ! [V5v5] : ( mem(V5v5,ty_2Erealax_2Ereal) => p(ap(ap(V0P,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V5v5))) ) ) & ! [V6v3] : ( mem(V6v3,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V6v3)),c_2Eextreal_2ENegInf)) ) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Eextreal_2Eextreal) => ! [V8v1] : ( mem(V8v1,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__sub__def,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ! [V3v2] : ( mem(V3v2,ty_2Erealax_2Ereal) => ! [V4v5] : ( mem(V4v5,ty_2Erealax_2Ereal) => ! [V5v3] : ( mem(V5v3,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2ENormal,V0x)),ap(c_2Eextreal_2ENormal,V1y)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal_2Ereal__sub,V0x),V1y)) ) & ( ( ap(ap(c_2Eextreal_2Eextreal__sub,c_2Eextreal_2EPosInf),V2a) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__sub,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf) = c_2Eextreal_2ENegInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2ENormal,V3v2)),c_2Eextreal_2EPosInf) = c_2Eextreal_2ENegInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__sub,c_2Eextreal_2ENegInf),c_2Eextreal_2ENegInf) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__sub,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V4v5)) = c_2Eextreal_2ENegInf ) & ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2ENormal,V5v3)),c_2Eextreal_2ENegInf) = c_2Eextreal_2EPosInf ) ) ) ) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__le__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))) => ( ( ( ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V1x)),ap(c_2Eextreal_2ENormal,V2y))) ) ) ) & ( ( ! [V3a] : ( mem(V3a,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,c_2Eextreal_2ENegInf),V3a)) ) ) & ( p(ap(ap(V0P,c_2Eextreal_2EPosInf),c_2Eextreal_2EPosInf)) & ( ( ! [V4v2] : ( mem(V4v2,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V4v2)),c_2Eextreal_2EPosInf)) ) ) & ( p(ap(ap(V0P,c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf)) & ( ( ! [V5v3] : ( mem(V5v3,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V5v3)),c_2Eextreal_2ENegInf)) ) ) & ! [V6v5] : ( mem(V6v5,ty_2Erealax_2Ereal) => p(ap(ap(V0P,c_2Eextreal_2EPosInf),ap(c_2Eextreal_2ENormal,V6v5))) ) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Eextreal_2Eextreal) => ! [V8v1] : ( mem(V8v1,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__le__def,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Eextreal_2Eextreal) => ! [V3v2] : ( mem(V3v2,ty_2Erealax_2Ereal) => ! [V4v3] : ( mem(V4v3,ty_2Erealax_2Ereal) => ! [V5v5] : ( mem(V5v5,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,V0x)),ap(c_2Eextreal_2ENormal,V1y))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) ) & ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,c_2Eextreal_2ENegInf),V2a)) <=> $true ) & ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,c_2Eextreal_2EPosInf),c_2Eextreal_2EPosInf)) <=> $true ) & ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,V3v2)),c_2Eextreal_2EPosInf)) <=> $true ) & ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf)) <=> $false ) & ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,V4v3)),c_2Eextreal_2ENegInf)) <=> $false ) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,c_2Eextreal_2EPosInf),ap(c_2Eextreal_2ENormal,V5v5))) <=> $false ) ) ) ) ) ) ) ) ) ) ) ) ))).
fof(ax_thm_2Eextreal_2Eextreal__lt__def,axiom, ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x)) ) ) ) )).
fof(conj_thm_2Eextreal_2Eextreal__mul__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))) => ( ( p(ap(ap(V0P,c_2Eextreal_2ENegInf),c_2Eextreal_2ENegInf)) & ( p(ap(ap(V0P,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf)) & ( p(ap(ap(V0P,c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf)) & ( p(ap(ap(V0P,c_2Eextreal_2EPosInf),c_2Eextreal_2EPosInf)) & ( ( ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V1x)),c_2Eextreal_2ENegInf)) ) ) & ( ( ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => p(ap(ap(V0P,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V2y))) ) ) & ( ( ! [V3x] : ( mem(V3x,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V3x)),c_2Eextreal_2EPosInf)) ) ) & ( ( ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => p(ap(ap(V0P,c_2Eextreal_2EPosInf),ap(c_2Eextreal_2ENormal,V4y))) ) ) & ! [V5x] : ( mem(V5x,ty_2Erealax_2Ereal) => ! [V6y] : ( mem(V6y,ty_2Erealax_2Ereal) => p(ap(ap(V0P,ap(c_2Eextreal_2ENormal,V5x)),ap(c_2Eextreal_2ENormal,V6y))) ) ) ) ) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Eextreal_2Eextreal) => ! [V8v1] : ( mem(V8v1,ty_2Eextreal_2Eextreal) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__mul__def,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2ENegInf),c_2Eextreal_2ENegInf) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf) = c_2Eextreal_2ENegInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2EPosInf),c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),c_2Eextreal_2ENegInf) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Emin_2E_3D(ty_2Erealax_2Ereal),V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)),c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf)) ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V1y)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Emin_2E_3D(ty_2Erealax_2Ereal),V1y),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)),c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf)) ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),c_2Eextreal_2EPosInf) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Emin_2E_3D(ty_2Erealax_2Ereal),V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)),c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf)) ) & ( ( ap(ap(c_2Eextreal_2Eextreal__mul,c_2Eextreal_2EPosInf),ap(c_2Eextreal_2ENormal,V1y)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Emin_2E_3D(ty_2Erealax_2Ereal),V1y),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)),c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf)) ) & ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),ap(c_2Eextreal_2ENormal,V1y)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)) ) ) ) ) ) ) ) ) ) ) ))).
fof(ax_thm_2Eextreal_2Eextreal__inv__def,axiom, ( ( ap(c_2Eextreal_2Eextreal__inv,c_2Eextreal_2ENegInf) = ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) ) & ( ( ap(c_2Eextreal_2Eextreal__inv,c_2Eextreal_2EPosInf) = ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) ) & ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Eextreal_2Eextreal__inv,ap(c_2Eextreal_2ENormal,V0x)) = ap(c_2Eextreal_2ENormal,ap(c_2Erealax_2Einv,V0x)) ) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__ainv__def,axiom, ( ( ap(c_2Eextreal_2Eextreal__ainv,c_2Eextreal_2ENegInf) = c_2Eextreal_2EPosInf ) & ( ( ap(c_2Eextreal_2Eextreal__ainv,c_2Eextreal_2EPosInf) = c_2Eextreal_2ENegInf ) & ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Eextreal_2Eextreal__ainv,ap(c_2Eextreal_2ENormal,V0x)) = ap(c_2Eextreal_2ENormal,ap(c_2Erealax_2Ereal__neg,V0x)) ) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__div__def,axiom, ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__div,V0x),V1y) = ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(c_2Eextreal_2Eextreal__inv,V1y)) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__abs__primitive__def,axiom, ( c_2Eextreal_2Eextreal__abs = ap(ap(c_2Erelation_2EWFREC(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal),ap(c_2Emin_2E_40(arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),f3434)),k(arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal),f3436)) )).
fof(conj_thm_2Eextreal_2Eextreal__abs__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Eextreal_2Eextreal,bool)) => ( ( ( ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => p(ap(V0P,ap(c_2Eextreal_2ENormal,V1x))) ) ) & ( p(ap(V0P,c_2Eextreal_2ENegInf)) & p(ap(V0P,c_2Eextreal_2EPosInf)) ) ) => ! [V2v] : ( mem(V2v,ty_2Eextreal_2Eextreal) => p(ap(V0P,V2v)) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__abs__def,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ap(c_2Eextreal_2Eextreal__abs,ap(c_2Eextreal_2ENormal,V0x)) = ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Eabs,V0x)) ) & ( ( ap(c_2Eextreal_2Eextreal__abs,c_2Eextreal_2ENegInf) = c_2Eextreal_2EPosInf ) & ( ap(c_2Eextreal_2Eextreal__abs,c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) ) ) ))).
fof(ax_thm_2Eextreal_2Eextreal__logr__def,axiom, ( ( ! [V0b] : ( mem(V0b,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Eextreal_2Eextreal__logr,V0b),ap(c_2Eextreal_2ENormal,V1x)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Eutil__prob_2Elogr,V0b),V1x)) ) ) ) ) & ( ( ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( ap(ap(c_2Eextreal_2Eextreal__logr,V2b),c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) ) ) & ! [V3b] : ( mem(V3b,ty_2Erealax_2Ereal) => ( ap(ap(c_2Eextreal_2Eextreal__logr,V3b),c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf ) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__lg__def,axiom, ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(c_2Eextreal_2Eextreal__lg,V0x) = ap(ap(c_2Eextreal_2Eextreal__logr,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0x) ) )).
fof(ax_thm_2Eextreal_2Eextreal__exp__def,axiom, ( ( ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Eextreal_2Eextreal__exp,ap(c_2Eextreal_2ENormal,V0x)) = ap(c_2Eextreal_2ENormal,ap(c_2Etransc_2Eexp,V0x)) ) ) ) & ( ( ap(c_2Eextreal_2Eextreal__exp,c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) & ( ap(c_2Eextreal_2Eextreal__exp,c_2Eextreal_2ENegInf) = ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__pow__def,axiom, ( ( ! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2ENormal,V0a)),V1n) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal_2Epow,V0a),V1n)) ) ) ) ) & ( ( ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Eextreal_2Eextreal__pow,c_2Eextreal_2EPosInf),V2n) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V2n),c_2Enum_2E0)),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2Eextreal_2EPosInf) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ap(ap(c_2Eextreal_2Eextreal__pow,c_2Eextreal_2ENegInf),V3n) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V3n),c_2Enum_2E0)),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(c_2Earithmetic_2EEVEN,V3n)),c_2Eextreal_2EPosInf),c_2Eextreal_2ENegInf)) ) ) ) )).
fof(ax_thm_2Eextreal_2Eextreal__sqrt__def,axiom, ( ( ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Eextreal_2Eextreal__sqrt,ap(c_2Eextreal_2ENormal,V0x)) = ap(c_2Eextreal_2ENormal,ap(c_2Etransc_2Esqrt,V0x)) ) ) ) & ( ap(c_2Eextreal_2Eextreal__sqrt,c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) )).
fof(conj_thm_2Eextreal_2EREAL__LT__LMUL__0__NEG,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)),ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y))) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,V1y),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LT__RMUL__0__NEG,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)),ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y))) & p(ap(ap(c_2Erealax_2Ereal__lt,V1y),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LT__LMUL__NEG__0,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) ) => p(ap(ap(c_2Erealax_2Ereal__lt,V1y),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LT__RMUL__NEG__0,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LT__LMUL__NEG__0__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LT__RMUL__NEG__0__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Erealax_2Ereal__lt,V1y),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LT__RDIV__EQ__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V2z),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Ereal_2E_2F,V1y),V2z)),V0x)) <=> p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,V0x),V2z)),V1y)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LE__RDIV__EQ__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V2z),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Ereal_2E_2F,V1y),V2z)),V0x)) <=> p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__mul,V0x),V2z)),V1y)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2EPOW__POS__EVEN,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V1x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(ap(c_2Ereal_2Epow,V1x),V0n))) <=> p(ap(c_2Earithmetic_2EEVEN,V0n)) ) ) ) ))).
fof(conj_thm_2Eextreal_2EPOW__NEG__ODD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V1x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Ereal_2Epow,V1x),V0n)),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(c_2Earithmetic_2EODD,V0n)) ) ) ) ))).
fof(conj_thm_2Eextreal_2ELOGR__MONO__LE,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,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_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2b)) ) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Eutil__prob_2Elogr,V2b),V0x)),ap(ap(c_2Eutil__prob_2Elogr,V2b),V1y))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2ELOGR__MONO__LE__IMP,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2b] : ( mem(V2b,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,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_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2b)) ) ) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Eutil__prob_2Elogr,V2b),V0x)),ap(ap(c_2Eutil__prob_2Elogr,V2b),V1y))) ) ) ) ))).
fof(ax_thm_2Eextreal_2Emono__increasing__def,axiom, ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( p(ap(c_2Eextreal_2Emono__increasing,V0f)) <=> ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V2n)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0f,V1m)),ap(V0f,V2n))) ) ) ) ) )).
fof(conj_thm_2Eextreal_2Emono__increasing__suc,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( p(ap(c_2Eextreal_2Emono__increasing,V0f)) <=> ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0f,V1n)),ap(V0f,ap(c_2Enum_2ESUC,V1n)))) ) ) ))).
fof(ax_thm_2Eextreal_2Emono__decreasing__def,axiom, ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( p(ap(c_2Eextreal_2Emono__decreasing,V0f)) <=> ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V2n)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0f,V2n)),ap(V0f,V1m))) ) ) ) ) )).
fof(conj_thm_2Eextreal_2Emono__decreasing__suc,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( p(ap(c_2Eextreal_2Emono__decreasing,V0f)) <=> ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0f,ap(c_2Enum_2ESUC,V1n))),ap(V0f,V1n))) ) ) ))).
fof(conj_thm_2Eextreal_2Emono__increasing__converges__to__sup,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ! [V1r] : ( mem(V1r,ty_2Erealax_2Ereal) => ( ( p(ap(c_2Eextreal_2Emono__increasing,V0f)) & p(ap(ap(c_2Eseq_2E_2D_2D_3E,V0f),V1r)) ) => ( V1r = ap(c_2Ereal_2Esup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Erealax_2Ereal),V0f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__cases,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( V0x = c_2Eextreal_2ENegInf ) | ( ( V0x = c_2Eextreal_2EPosInf ) | ? [V1r] : ( mem(V1r,ty_2Erealax_2Ereal) & ( V0x = ap(c_2Eextreal_2ENormal,V1r) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__eq__zero,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ap(c_2Eextreal_2ENormal,V0x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) <=> ( V0x = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__not__infty,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ( ~~ ( ap(c_2Eextreal_2ENormal,V0x) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(c_2Eextreal_2ENormal,V0x) = c_2Eextreal_2EPosInf ) ) ) ))).
fof(conj_thm_2Eextreal_2Enum__not__infty,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ( ~~ ( ap(c_2Eextreal_2Eextreal__of__num,V0n) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(c_2Eextreal_2Eextreal__of__num,V0n) = c_2Eextreal_2EPosInf ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__11,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1a_27] : ( mem(V1a_27,ty_2Erealax_2Ereal) => ( ( ap(c_2Eextreal_2ENormal,V0a) = ap(c_2Eextreal_2ENormal,V1a_27) ) <=> ( V0a = V1a_27 ) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__rzero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Eextreal_2Emul__lzero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Eextreal_2Emul__rone,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0x ) ))).
fof(conj_thm_2Eextreal_2Emul__lone,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0x) = V0x ) ))).
fof(conj_thm_2Eextreal_2Eentire,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) <=> ( ( V0x = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) | ( V1y = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__lt__eq,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2ENormal,V0x)),ap(c_2Eextreal_2ENormal,V1y))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__refl,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V0x)) ))).
fof(conj_thm_2Eextreal_2Elt__refl,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ~~ p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V0x)) ) ))).
fof(conj_thm_2Eextreal_2Ele__infty,lemma,(( ( ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,c_2Eextreal_2ENegInf),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),c_2Eextreal_2EPosInf)) ) ) ) & ( ( ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),c_2Eextreal_2ENegInf)) <=> ( V1x = c_2Eextreal_2ENegInf ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,c_2Eextreal_2EPosInf),V2x)) <=> ( V2x = c_2Eextreal_2EPosInf ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__infty,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,V1y))) & ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2ENormal,V1y)),c_2Eextreal_2EPosInf)) & ( p(ap(ap(c_2Eextreal_2Eextreal__lt,c_2Eextreal_2ENegInf),c_2Eextreal_2EPosInf)) & ( ( ~~ p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),c_2Eextreal_2ENegInf)) ) & ( ( ~~ p(ap(ap(c_2Eextreal_2Eextreal__lt,c_2Eextreal_2EPosInf),V0x)) ) & ( ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),c_2Eextreal_2EPosInf)) ) & ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,c_2Eextreal_2ENegInf),V0x)) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__imp__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__imp__ne,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) => ( ~~ ( V0x = V1y ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__trans,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__trans,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V2z)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elet__trans,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V2z)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__antisym,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x)) ) <=> ( V0x = V1y ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__antisym,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ~~ ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V0x)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elte__trans,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__total,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) | p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x)) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__total,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( V0x = V1y ) | ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) | p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V0x)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__01,lemma,(p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))).
fof(conj_thm_2Eextreal_2Elt__01,lemma,(p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))).
fof(conj_thm_2Eextreal_2Ene__01,lemma,(( ~~ ( ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Eextreal_2Ele__02,lemma,(p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))))).
fof(conj_thm_2Eextreal_2Elt__02,lemma,(p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))))).
fof(conj_thm_2Eextreal_2Ene__02,lemma,(( ~~ ( ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Eextreal_2Ele__num,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__of__num,V0n))) ))).
fof(conj_thm_2Eextreal_2Elt__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) <=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) & ( ~~ ( V0x = V1y ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__lt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) <=> ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) | ( V0x = V1y ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__ainv,V0x)),ap(c_2Eextreal_2Eextreal__ainv,V1y))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V0x)) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__ainv,V0x)),ap(c_2Eextreal_2Eextreal__ainv,V1y))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V0x)) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elet__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elte__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__add2,lemma,(! [V0w] : ( mem(V0w,ty_2Eextreal_2Eextreal) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ! [V3z] : ( mem(V3z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0w),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V3z)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V0w),V2y)),ap(ap(c_2Eextreal_2Eextreal__add,V1x),V3z))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__add2,lemma,(! [V0w] : ( mem(V0w,ty_2Eextreal_2Eextreal) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ! [V3z] : ( mem(V3z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0w),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V2y),V3z)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V0w),V2y)),ap(ap(c_2Eextreal_2Eextreal__add,V1x),V3z))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elet__add2,lemma,(! [V0w] : ( mem(V0w,ty_2Eextreal_2Eextreal) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ! [V3z] : ( mem(V3z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0w = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0w = c_2Eextreal_2EPosInf ) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0w),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V2y),V3z)) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V0w),V2y)),ap(ap(c_2Eextreal_2Eextreal__add,V1x),V3z))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elet__add2__alt,lemma,(! [V0w] : ( mem(V0w,ty_2Eextreal_2Eextreal) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ! [V3z] : ( mem(V3z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1x = c_2Eextreal_2EPosInf ) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0w),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V2y),V3z)) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V0w),V2y)),ap(ap(c_2Eextreal_2Eextreal__add,V1x),V3z))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__addr,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__addr__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__ladd,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V2z))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__radd,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__radd__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__ladd__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V2z))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__ladd,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V2z))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__radd,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__addl,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__lneg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__ainv,V0x)),V1y)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__mul,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elet__mul,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elte__mul,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__mul__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__mul,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__mul__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__lt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__let,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__lte,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__rmul__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)),ap(ap(c_2Eextreal_2Eextreal__mul,V1y),V2z))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__lmul__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V2z),V0x)),ap(ap(c_2Eextreal_2Eextreal__mul,V2z),V1y))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__rmul,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)),ap(ap(c_2Eextreal_2Eextreal__mul,V1y),V2z))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__lmul,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__mul2,lemma,(! [V0x1] : ( mem(V0x1,ty_2Eextreal_2Eextreal) => ! [V1x2] : ( mem(V1x2,ty_2Eextreal_2Eextreal) => ! [V2y1] : ( mem(V2y1,ty_2Eextreal_2Eextreal) => ! [V3y2] : ( mem(V3y2,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x1)) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2y1)) & ( ( ~~ ( V0x1 = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V2y1 = c_2Eextreal_2EPosInf ) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x1),V1x2)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V2y1),V3y2)) ) ) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__mul,V0x1),V2y1)),ap(ap(c_2Eextreal_2Eextreal__mul,V1x2),V3y2))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eabs__pos,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__abs,V0x))) ))).
fof(conj_thm_2Eextreal_2Eabs__refl,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ap(c_2Eextreal_2Eextreal__abs,V0x) = V0x ) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) ) ))).
fof(conj_thm_2Eextreal_2Eabs__bounds,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1k] : ( mem(V1k,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__abs,V0x)),V1k)) <=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__ainv,V1k)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1k)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eabs__bounds__lt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1k] : ( mem(V1k,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__abs,V0x)),V1k)) <=> ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__ainv,V1k)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1k)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__comm,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y) = ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__assoc,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),V2z) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__not__infty,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y) = c_2Eextreal_2ENegInf ) ) ) & ( ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y) = c_2Eextreal_2EPosInf ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__rzero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)) = V0x ) ))).
fof(conj_thm_2Eextreal_2Eadd__lzero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x) = V0x ) ))).
fof(conj_thm_2Eextreal_2Eadd__infty,lemma,(( ( ! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf ) & ( ap(ap(c_2Eextreal_2Eextreal__add,c_2Eextreal_2EPosInf),V0x) = c_2Eextreal_2EPosInf ) ) ) ) & ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( ( ~~ ( V1x = c_2Eextreal_2EPosInf ) ) => ( ( ap(ap(c_2Eextreal_2Eextreal__add,V1x),c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf ) & ( ap(ap(c_2Eextreal_2Eextreal__add,c_2Eextreal_2ENegInf),V1x) = c_2Eextreal_2ENegInf ) ) ) ) ))).
fof(conj_thm_2Eextreal_2EEXTREAL__EQ__LADD,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y) = ap(ap(c_2Eextreal_2Eextreal__add,V0x),V2z) ) <=> ( V1y = V2z ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__rzero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)) = V0x ) ))).
fof(conj_thm_2Eextreal_2Esub__lzero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x) = ap(c_2Eextreal_2Eextreal__ainv,V0x) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__imp2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__sub__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),V2z)) => p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__sub,V2z),V0x))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__sub__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),V2z)) => p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(ap(c_2Eextreal_2Eextreal__sub,V2z),V0x))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__lt__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__lt__imp2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__zero__lt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x))) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__zero__lt2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__lt__zero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__lt__zero2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__zero__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x))) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__zero,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__sub__eq,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__sub,V2z),V0x))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__sub__eq2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__sub,V2z),V0x))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__eq,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__eq2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__add,V2z),V0x))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__switch,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V2z)),V0x)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__le__switch2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)),V2z)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V2z)),V0x)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__sub,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),V2z)) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(ap(c_2Eextreal_2Eextreal__sub,V2z),V0x))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__add2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x)) = V1y ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__sub,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),V1y) = V0x ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__sub2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V0x)),V1y) = V0x ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y)),V1y) = V0x ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__sub__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y) = ap(ap(c_2Eextreal_2Eextreal__add,V0x),ap(c_2Eextreal_2Eextreal__ainv,V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__0,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) => ( V0x = V1y ) ) ) ))).
fof(conj_thm_2Eextreal_2Eneg__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(c_2Eextreal_2Eextreal__ainv,ap(c_2Eextreal_2Eextreal__ainv,V0x)) = V0x ) ))).
fof(conj_thm_2Eextreal_2Eneg__0,lemma,(( ap(c_2Eextreal_2Eextreal__ainv,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Eextreal_2Eneg__eq0,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ap(c_2Eextreal_2Eextreal__ainv,V0x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) <=> ( V0x = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Eextreal_2Eeq__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ap(c_2Eextreal_2Eextreal__ainv,V0x) = ap(c_2Eextreal_2Eextreal__ainv,V1y) ) <=> ( V0x = V1y ) ) ) ))).
fof(conj_thm_2Eextreal_2Eneg__minus1,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(c_2Eextreal_2Eextreal__ainv,V0x) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__ainv,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x) ) ))).
fof(conj_thm_2Eextreal_2Esub__rneg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),ap(c_2Eextreal_2Eextreal__ainv,V1y)) = ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__lneg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) ) | ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2Eextreal__ainv,V0x)),V1y) = ap(c_2Eextreal_2Eextreal__ainv,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eneg__sub,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) | ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) ) => ( ap(c_2Eextreal_2Eextreal__ainv,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y)) = ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V0x) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__not__infty,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y) = c_2Eextreal_2ENegInf ) ) ) & ( ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y) = c_2Eextreal_2EPosInf ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__lsub__imp,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),V2z)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V2z)),ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eeq__sub__ladd__normal,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ( V0x = ap(ap(c_2Eextreal_2Eextreal__sub,V1y),ap(c_2Eextreal_2ENormal,V2z)) ) <=> ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),ap(c_2Eextreal_2ENormal,V2z)) = V1y ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eeq__sub__radd,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) => ( ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y) = V2z ) <=> ( V0x = ap(ap(c_2Eextreal_2Eextreal__add,V2z),V1y) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eeq__sub__ladd,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) => ( ( V0x = ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V2z) ) <=> ( ap(ap(c_2Eextreal_2Eextreal__add,V0x),V2z) = V1y ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eeq__sub__switch,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ( V0x = ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2ENormal,V2z)),V1y) ) <=> ( V1y = ap(ap(c_2Eextreal_2Eextreal__sub,ap(c_2Eextreal_2ENormal,V2z)),V0x) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eeq__add__sub__switch,lemma,(! [V0a] : ( mem(V0a,ty_2Eextreal_2Eextreal) => ! [V1b] : ( mem(V1b,ty_2Eextreal_2Eextreal) => ! [V2c] : ( mem(V2c,ty_2Eextreal_2Eextreal) => ! [V3d] : ( mem(V3d,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1b = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1b = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V2c = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2c = c_2Eextreal_2EPosInf ) ) ) ) ) => ( ( ap(ap(c_2Eextreal_2Eextreal__add,V0a),V1b) = ap(ap(c_2Eextreal_2Eextreal__add,V2c),V3d) ) <=> ( ap(ap(c_2Eextreal_2Eextreal__sub,V0a),V2c) = ap(ap(c_2Eextreal_2Eextreal__sub,V3d),V1b) ) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__refl,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V0x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__comm,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) = ap(ap(c_2Eextreal_2Eextreal__mul,V1y),V0x) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__assoc,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(ap(c_2Eextreal_2Eextreal__mul,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),V2z) ) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__not__infty,lemma,(( ( ! [V0c] : ( mem(V0c,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0c)) & ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0c)),V1y) = c_2Eextreal_2ENegInf ) ) ) ) ) ) & ( ( ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2c)) & ( ~~ ( V3y = c_2Eextreal_2EPosInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V2c)),V3y) = c_2Eextreal_2EPosInf ) ) ) ) ) ) & ( ( ! [V4c] : ( mem(V4c,ty_2Erealax_2Ereal) => ! [V5y] : ( mem(V5y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,V4c),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & ( ~~ ( V5y = c_2Eextreal_2ENegInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V4c)),V5y) = c_2Eextreal_2EPosInf ) ) ) ) ) ) & ! [V6c] : ( mem(V6c,ty_2Erealax_2Ereal) => ! [V7y] : ( mem(V7y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,V6c),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) & ( ~~ ( V7y = c_2Eextreal_2EPosInf ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V6c)),V7y) = c_2Eextreal_2ENegInf ) ) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__not__infty2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) ) ) ) => ( ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) = c_2Eextreal_2EPosInf ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__ldistrib__pos,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__ldistrib__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Eextreal_2Eextreal__le,V2z),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__ldistrib__normal,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) | ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__ldistrib__normal2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V0x)),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__rdistrib__normal,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) | ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)),ap(c_2Eextreal_2ENormal,V0x)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,V1y),ap(c_2Eextreal_2ENormal,V0x))),ap(ap(c_2Eextreal_2Eextreal__mul,V2z),ap(c_2Eextreal_2ENormal,V0x))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__rdistrib__normal2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)),ap(c_2Eextreal_2ENormal,V0x)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,V1y),ap(c_2Eextreal_2ENormal,V0x))),ap(ap(c_2Eextreal_2Eextreal__mul,V2z),ap(c_2Eextreal_2ENormal,V0x))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__ldistrib,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) ) | ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Eextreal_2Eextreal__le,V2z),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__rdistrib,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1y)) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) ) | ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Eextreal_2Eextreal__le,V2z),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2z)),V0x) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__mul,V1y),V0x)),ap(ap(c_2Eextreal_2Eextreal__mul,V2z),V0x)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__lneg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__ainv,V0x)),V1y) = ap(c_2Eextreal_2Eextreal__ainv,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Emul__rneg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(c_2Eextreal_2Eextreal__ainv,V1y)) = ap(c_2Eextreal_2Eextreal__ainv,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Eneg__mul2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__ainv,V0x)),ap(c_2Eextreal_2Eextreal__ainv,V1y)) = ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd2__sub2,lemma,(! [V0a] : ( mem(V0a,ty_2Eextreal_2Eextreal) => ! [V1b] : ( mem(V1b,ty_2Eextreal_2Eextreal) => ! [V2c] : ( mem(V2c,ty_2Eextreal_2Eextreal) => ! [V3d] : ( mem(V3d,ty_2Eextreal_2Eextreal) => ( ( ( ( ~~ ( V1b = c_2Eextreal_2EPosInf ) ) & ( ~~ ( V3d = c_2Eextreal_2EPosInf ) ) ) | ( ( ~~ ( V1b = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V3d = c_2Eextreal_2ENegInf ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__sub,V0a),V1b)),ap(ap(c_2Eextreal_2Eextreal__sub,V2c),V3d)) = ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Eextreal_2Eextreal__add,V0a),V2c)),ap(ap(c_2Eextreal_2Eextreal__add,V1b),V3d)) ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__ldistrib,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(ap(c_2Eextreal_2Eextreal__sub,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y)),ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esub__rdistrib,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) & ( ( ~~ ( V2z = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = c_2Eextreal_2EPosInf ) ) ) ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__sub,V0x),V1y)),V2z) = ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V2z)),ap(ap(c_2Eextreal_2Eextreal__mul,V1y),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eextreal__div__eq,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2ENormal,V0x)),ap(c_2Eextreal_2ENormal,V1y)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal_2E_2F,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Einv__one,lemma,(( ap(c_2Eextreal_2Eextreal__inv,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Eextreal_2Einv__1over,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(c_2Eextreal_2Eextreal__inv,V0x) = ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0x) ) ))).
fof(conj_thm_2Eextreal_2Ediv__one,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__div,V0x),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0x ) ))).
fof(conj_thm_2Eextreal_2Einv__pos,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0x))) ) ))).
fof(conj_thm_2Eextreal_2Erinv__uniq,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) => ( V1y = ap(c_2Eextreal_2Eextreal__inv,V0x) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elinv__uniq,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V1y) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) => ( V0x = ap(c_2Eextreal_2Eextreal__inv,V1y) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__rdiv,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V1y),ap(c_2Eextreal_2ENormal,V0x))),V2z)) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__div,V2z),ap(c_2Eextreal_2ENormal,V0x)))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__ldiv,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x)) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,V1y),ap(ap(c_2Eextreal_2Eextreal__mul,V2z),ap(c_2Eextreal_2ENormal,V0x)))) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__div,V1y),ap(c_2Eextreal_2ENormal,V0x))),V2z)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__rdiv,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2z)) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),ap(ap(c_2Eextreal_2Eextreal__div,V1y),ap(c_2Eextreal_2ENormal,V2z)))) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(c_2Eextreal_2ENormal,V2z))),V1y)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__ldiv,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2z)) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__div,V0x),ap(c_2Eextreal_2ENormal,V2z))),V1y)) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),ap(ap(c_2Eextreal_2Eextreal__mul,V1y),ap(c_2Eextreal_2ENormal,V2z)))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Elt__rdiv__neg,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V2z),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__div,V1y),ap(c_2Eextreal_2ENormal,V2z))),V0x)) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__mul,V0x),ap(c_2Eextreal_2ENormal,V2z))),V1y)) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ediv__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ( ~~ ( V1y = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V2z = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) => ( ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__div,V0x),V2z)),ap(ap(c_2Eextreal_2Eextreal__div,V1y),V2z)) = ap(ap(c_2Eextreal_2Eextreal__div,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),V2z) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__inv,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__inv,V0x))) ) ))).
fof(conj_thm_2Eextreal_2Epow__0,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__pow,V0x),c_2Enum_2E0) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Eextreal_2Epow__1,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__pow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = V0x ) ))).
fof(conj_thm_2Eextreal_2Epow__2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__pow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = ap(ap(c_2Eextreal_2Eextreal__mul,V0x),V0x) ) ))).
fof(conj_thm_2Eextreal_2Epow__zero,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__pow,V1x),ap(c_2Enum_2ESUC,V0n)) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) <=> ( V1x = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__zero__imp,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) => ( V1x = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__pow2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__pow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ))).
fof(conj_thm_2Eextreal_2Epow__pos__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__pow,V0x),V1n))) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__pos__lt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__pow,V0x),V1n))) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__le,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),V2y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n)),ap(ap(c_2Eextreal_2Eextreal__pow,V2y),V0n))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__lt,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1x),V2y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__pow,V1x),ap(c_2Enum_2ESUC,V0n))),ap(ap(c_2Eextreal_2Eextreal__pow,V2y),ap(c_2Enum_2ESUC,V0n)))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__lt2,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V0n = c_2Enum_2E0 ) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V1x)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1x),V2y)) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n)),ap(ap(c_2Eextreal_2Eextreal__pow,V2y),V0n))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__le__mono,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0x)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2m)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__pow,V0x),V1n)),ap(ap(c_2Eextreal_2Eextreal__pow,V0x),V2m))) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__pos__even,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V1x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n))) <=> p(ap(c_2Earithmetic_2EEVEN,V0n)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__neg__odd,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,V1x),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n)),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))) <=> p(ap(c_2Earithmetic_2EODD,V0n)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Eadd__pow2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__pow,ap(ap(c_2Eextreal_2Eextreal__add,V0x),V1y)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__pow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Eextreal_2Eextreal__pow,V1y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0x)),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__add,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( ap(ap(c_2Eextreal_2Eextreal__pow,V0x),ap(ap(c_2Earithmetic_2E_2B,V1n),V2m)) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__pow,V0x),V1n)),ap(ap(c_2Eextreal_2Eextreal__pow,V0x),V2m)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__mul,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ( ap(ap(c_2Eextreal_2Eextreal__pow,ap(ap(c_2Eextreal_2Eextreal__mul,V1x),V2y)),V0n) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n)),ap(ap(c_2Eextreal_2Eextreal__pow,V2y),V0n)) ) ) ) ))).
fof(conj_thm_2Eextreal_2Epow__minus1,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__ainv,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V0n)) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Eextreal_2Epow__not__infty,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( ( ( ~~ ( V1x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V1x = c_2Eextreal_2EPosInf ) ) ) => ( ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__pow,V1x),V0n) = c_2Eextreal_2EPosInf ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Esqrt__pos__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__sqrt,V0x))) ) ))).
fof(conj_thm_2Eextreal_2Esqrt__pos__lt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(c_2Eextreal_2Eextreal__sqrt,V0x))) ) ))).
fof(conj_thm_2Eextreal_2Epow2__sqrt,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => ( ap(c_2Eextreal_2Eextreal__sqrt,ap(ap(c_2Eextreal_2Eextreal__pow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = V0x ) ) ))).
fof(conj_thm_2Eextreal_2Esqrt__pow2,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__sqrt,V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = V0x ) <=> p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) ) ))).
fof(conj_thm_2Eextreal_2Esqrt__mono__le,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) & p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__sqrt,V0x)),ap(c_2Eextreal_2Eextreal__sqrt,V1y))) ) ) ))).
fof(conj_thm_2Eextreal_2Elogr__not__infty,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ( ( ( ~~ ( V0x = c_2Eextreal_2ENegInf ) ) & ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) ) => ( ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__logr,V1b),V0x) = c_2Eextreal_2ENegInf ) ) & ( ~~ ( ap(ap(c_2Eextreal_2Eextreal__logr,V1b),V0x) = c_2Eextreal_2EPosInf ) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2Ehalf__between,lemma,(( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ))).
fof(conj_thm_2Eextreal_2Ethirds__between,lemma,(( ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) & ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) & ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Eextreal_2Ehalf__cancel,lemma,(( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Eextreal_2Ethird__cancel,lemma,(( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Eextreal_2Efourth__cancel,lemma,(( ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Eextreal_2Equotient__normal,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Eextreal_2Eextreal__div,ap(c_2Eextreal_2Eextreal__of__num,V0n)),ap(c_2Eextreal_2Eextreal__of__num,V1m)) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,V0n)),ap(c_2Ereal_2Ereal__of__num,V1m))) ) ) ))).
fof(ax_thm_2Eextreal_2Eext__mono__increasing__def,axiom, ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) => ( p(ap(c_2Eextreal_2Eext__mono__increasing,V0f)) <=> ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V2n)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V0f,V1m)),ap(V0f,V2n))) ) ) ) ) )).
fof(conj_thm_2Eextreal_2Eext__mono__increasing__suc,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) => ( p(ap(c_2Eextreal_2Eext__mono__increasing,V0f)) <=> ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V0f,V1n)),ap(V0f,ap(c_2Enum_2ESUC,V1n)))) ) ) ))).
fof(ax_thm_2Eextreal_2Eext__mono__decreasing__def,axiom, ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) => ( p(ap(c_2Eextreal_2Eext__mono__decreasing,V0f)) <=> ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V2n)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V0f,V2n)),ap(V0f,V1m))) ) ) ) ) )).
fof(conj_thm_2Eextreal_2Eext__mono__decreasing__suc,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) => ( p(ap(c_2Eextreal_2Eext__mono__decreasing,V0f)) <=> ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V0f,ap(c_2Enum_2ESUC,V1n))),ap(V0f,V1n))) ) ) ))).
fof(conj_thm_2Eextreal_2EEXTREAL__ARCH,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0x)) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ~~ ( V1y = c_2Eextreal_2EPosInf ) ) => ? [V2n] : ( mem(V2n,ty_2Enum_2Enum) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V1y),ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,V2n)),V0x))) ) ) ) ) ))).
fof(conj_thm_2Eextreal_2ESIMP__REAL__ARCH,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(c_2Ereal_2Ereal__of__num,V1n))) ) ))).
fof(conj_thm_2Eextreal_2ESIMP__REAL__ARCH__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,V1n))),V0x)) ) ))).
fof(conj_thm_2Eextreal_2ESIMP__EXTREAL__ARCH,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(c_2Eextreal_2Eextreal__of__num,V1n))) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__ARCH__POW,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(ap(c_2Erealax_2Ereal__lt,V0x),ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V1n))) ) ))).
fof(conj_thm_2Eextreal_2EEXTREAL__ARCH__POW,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ( ( ~~ ( V0x = c_2Eextreal_2EPosInf ) ) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V0x),ap(ap(c_2Eextreal_2Eextreal__pow,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V1n))) ) ) ))).
fof(conj_thm_2Eextreal_2EEXTREAL__ARCH__POW__INV,lemma,(! [V0e] : ( mem(V0e,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V0e)) => ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2E_2F,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_2EBIT2,c_2Earithmetic_2EZERO))))),V1n))),V0e)) ) ) ))).
fof(conj_thm_2Eextreal_2EREAL__LE__MUL__EPSILON,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2z)) & p(ap(ap(c_2Erealax_2Ereal__lt,V2z),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(ap(c_2Erealax_2Ereal__mul,V2z),V0x)),V1y)) ) ) ) => p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__epsilon,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ! [V2e] : ( mem(V2e,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2e)) & ( ~~ ( V2e = c_2Eextreal_2EPosInf ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),ap(ap(c_2Eextreal_2Eextreal__add,V1y),V2e))) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) ) ))).
fof(conj_thm_2Eextreal_2Ele__mul__epsilon,lemma,(! [V0x] : ( mem(V0x,ty_2Eextreal_2Eextreal) => ! [V1y] : ( mem(V1y,ty_2Eextreal_2Eextreal) => ( ( ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),V2z)) & p(ap(ap(c_2Eextreal_2Eextreal__lt,V2z),ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__mul,V2z),V0x)),V1y)) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,V0x),V1y)) ) ) ))).
fof(ax_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s) = ap(ap(ap(c_2Epred__set_2EITSET(A_27a,ty_2Eextreal_2Eextreal),f3438(A_27a,V0f)),V1s),ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)) ) ) ) ) )).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__THM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),c_2Epred__set_2EEMPTY(A_27a)) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) & ! [V1e] : ( mem(V1e,A_27a) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V2s)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),ap(ap(c_2Epred__set_2EINSERT(A_27a),V1e),V2s)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(V0f,V1e)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),ap(ap(c_2Epred__set_2EDELETE(A_27a),V2s),V1e))) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__NOT__NEG__INF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => ( ~~ ( ap(V0f,V2x) = c_2Eextreal_2ENegInf ) ) ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s) = c_2Eextreal_2ENegInf ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__NOT__POS__INF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => ( ~~ ( ap(V0f,V2x) = c_2Eextreal_2EPosInf ) ) ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s) = c_2Eextreal_2EPosInf ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__NOT__INFTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => ( ~~ ( ap(V0f,V2x) = c_2Eextreal_2ENegInf ) ) ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s) = c_2Eextreal_2ENegInf ) ) ) & ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) => ( ~~ ( ap(V0f,V3x) = c_2Eextreal_2EPosInf ) ) ) ) ) => ( ~~ ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s) = c_2Eextreal_2EPosInf ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__SING,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1e] : ( mem(V1e,A_27a) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),ap(ap(c_2Epred__set_2EINSERT(A_27a),V1e),c_2Epred__set_2EEMPTY(A_27a))) = ap(V0f,V1e) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__POS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V0f,V2x))) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s))) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__SPOS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ( ( ~~ ( V1s = c_2Epred__set_2EEMPTY(A_27a) ) ) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V0f,V2x))) ) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s))) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__IF__ELIM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V0s)) => p(ap(V1P,V3x)) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3439(A_27a,V2f,V1P)),V0s) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f),V0s) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__FINITE__SAME,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2p] : ( mem(V2p,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2p),V0s)) & ! [V3q] : ( mem(V3q,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3q),V0s)) => ( ap(V1f,V2p) = ap(V1f,V3q) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Epred__set_2ECARD(A_27a),V0s))),ap(V1f,V2p)) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__FINITE__CONST,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0P)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2x] : ( mem(V2x,ty_2Eextreal_2Eextreal) => ( ( ! [V3y] : ( mem(V3y,A_27a) => ( ap(V1f,V3y) = V2x ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0P) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Epred__set_2ECARD(A_27a),V0P))),V2x) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__ZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),k(A_27a,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0))),V0s) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => ( ap(V0f,V2x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__IN__IF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3440(A_27a,V1f,V0s)),V0s) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__CMUL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ( ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V2c)) | ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V0s)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V1f,V3x))) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3441(A_27a,V1f,V2c)),V0s) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V2c)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s)) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__CMUL2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V0s)) => ( ~~ ( ap(V1f,V3x) = c_2Eextreal_2ENegInf ) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3441(A_27a,V1f,V2c)),V0s) = ap(ap(c_2Eextreal_2Eextreal__mul,ap(c_2Eextreal_2ENormal,V2c)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s)) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__IMAGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f_27] : ( mem(V1f_27,arr(A_27a,A_27b)) => ( p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V1f_27),V0s),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V1f_27),V0s))) => ! [V2f] : ( mem(V2f,arr(A_27b,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27b),V2f),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V1f_27),V0s)) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),ap(ap(c_2Ecombin_2Eo(A_27a,ty_2Eextreal_2Eextreal,A_27b),V2f),V1f_27)),V0s) ) ) ) ) ) ))))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__DISJOINT__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1s_27] : ( mem(V1s_27,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s_27)) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),V0s),V1s_27)) ) ) => ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f),ap(ap(c_2Epred__set_2EUNION(A_27a),V0s),V1s_27)) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f),V0s)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f),V1s_27)) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__EQ__CARD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3442(A_27a,V0s)),V0s) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Epred__set_2ECARD(A_27a),V0s)) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__INV__CARD__EQ__1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( ( ( ~~ ( V0s = c_2Epred__set_2EEMPTY(A_27a) ) ) & p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3443(A_27a,V0s)),V0s) = ap(c_2Eextreal_2Eextreal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__INTER__NONZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),ap(ap(c_2Epred__set_2EINTER(A_27a),V0s),f3444(A_27a,V1f))) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__INTER__ELIM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27a,bool)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V2s_27)) ) => ( ap(V1f,V3x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),ap(ap(c_2Epred__set_2EINTER(A_27a),V0s),V2s_27)) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__ZERO__DIFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2t] : ( mem(V2t,arr(A_27a,bool)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V2t)) => ( ap(V1f,V3x) = ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),ap(ap(c_2Epred__set_2EDIFF(A_27a),V0s),V2t)) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__MONO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f_27] : ( mem(V2f_27,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V0s)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V1f,V3x)),ap(V2f_27,V3x))) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f_27),V0s))) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__MONO__SET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2t] : ( mem(V2t,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ( p(ap(c_2Epred__set_2EFINITE(A_27a),V2t)) & ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1s),V2t)) & ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V2t)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V0f,V3x))) ) ) ) ) ) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V2t))) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f_27] : ( mem(V2f_27,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V0s)) => ( ap(V1f,V3x) = ap(V2f_27,V3x) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f_27),V0s) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__POS__MEM__LE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__of__num,c_2Enum_2E0)),ap(V0f,V2x))) ) ) ) => ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) => p(ap(ap(c_2Eextreal_2Eextreal__le,ap(V0f,V3x)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V0f),V1s))) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f_27] : ( mem(V2f_27,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3445(A_27a,V1f,V2f_27)),V0s) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f_27),V0s)) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__SUB,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2f_27] : ( mem(V2f_27,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V0s)) => ( ~~ ( ap(V2f_27,V3x) = c_2Eextreal_2ENegInf ) ) ) ) ) | ! [V4x] : ( mem(V4x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V0s)) => ( ~~ ( ap(V2f_27,V4x) = c_2Eextreal_2EPosInf ) ) ) ) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3446(A_27a,V1f,V2f_27)),V0s) = ap(ap(c_2Eextreal_2Eextreal__sub,ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s)),ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V2f_27),V0s)) ) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__EXTREAL__SUM__IMAGE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1s_27] : ( mem(V1s_27,arr(A_27b,bool)) => ! [V2f] : ( mem(V2f,arr(A_27a,arr(A_27b,ty_2Eextreal_2Eextreal))) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & p(ap(c_2Epred__set_2EFINITE(A_27b),V1s_27)) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3447(A_27a,A_27b,V2f,V1s_27)),V0s) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Epair_2Eprod(A_27a,A_27b)),f3179(A_27a,A_27b,V2f)),ap(ap(c_2Epred__set_2ECROSS(A_27a,A_27b),V0s),V1s_27)) ) ) ) ) ))))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__NORMAL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Erealax_2Ereal)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3448(A_27a,V0f)),V1s) = ap(c_2Eextreal_2ENormal,ap(ap(c_2Ereal__sigma_2EREAL__SUM__IMAGE(A_27a),V0f),V1s)) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__IN__IF__ALT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ! [V2z] : ( mem(V2z,ty_2Eextreal_2Eextreal) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),V1f),V0s) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(A_27a),f3449(A_27a,V1f,V0s,V2z)),V0s) ) ) ) ) )))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__CROSS__SYM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Eextreal_2Eextreal)) => ! [V1s1] : ( mem(V1s1,arr(A_27a,bool)) => ! [V2s2] : ( mem(V2s2,arr(A_27b,bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V1s1)) & p(ap(c_2Epred__set_2EFINITE(A_27b),V2s2)) ) => ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Eextreal_2Eextreal),f3190(A_27a,A_27b,V0f))),ap(ap(c_2Epred__set_2ECROSS(A_27a,A_27b),V1s1),V2s2)) = ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2EUNCURRY(A_27b,A_27a,ty_2Eextreal_2Eextreal),f3192(A_27a,A_27b,V0f))),ap(ap(c_2Epred__set_2ECROSS(A_27b,A_27a),V2s2),V1s1)) ) ) ) ) ))))).
fof(conj_thm_2Eextreal_2EEXTREAL__SUM__IMAGE__COUNT,lemma,(! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal)) => ( ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),V0f),ap(c_2Epred__set_2Ecount,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(ap(c_2Eextreal_2Eextreal__add,ap(V0f,c_2Enum_2E0)),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) & ( ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),V0f),ap(c_2Epred__set_2Ecount,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(V0f,c_2Enum_2E0)),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) & ( ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),V0f),ap(c_2Epred__set_2Ecount,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(V0f,c_2Enum_2E0)),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) & ( ap(ap(c_2Eextreal_2EEXTREAL__SUM__IMAGE(ty_2Enum_2Enum),V0f),ap(c_2Epred__set_2Ecount,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) = ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(ap(c_2Eextreal_2Eextreal__add,ap(V0f,c_2Enum_2E0)),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(V0f,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ) ) ))).
fof(ax_thm_2Eextreal_2Eextreal__sup__def,axiom, ! [V0p] : ( mem(V0p,arr(ty_2Eextreal_2Eextreal,bool)) => ( ap(c_2Eextreal_2Eextreal__sup,V0p) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(c_2Ebool_2E_21(ty_2Eextreal_2Eextreal),f3451(V0p))),c_2Eextreal_2EPosInf),ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(c_2Ebool_2E_21(ty_2Eextreal_2Eextreal),f3452(V0p))),c_2Eextreal_2ENegInf),ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Esup,f3453(V0p))))) ) )).
fof(ax_thm_2Eextreal_2Eextreal__inf__def,axiom, ! [V0p] : ( mem(V0p,arr(ty_2Eextreal_2Eextreal,bool)) => ( ap(c_2Eextreal_2Eextreal__inf,V0p) = ap(c_2Eextreal_2Eextreal__ainv,ap(c_2Eextreal_2Eextreal__sup,ap(ap(c_2Epred__set_2EIMAGE(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal),c_2Eextreal_2Eextreal__ainv),V0p))) ) )).
fof(conj_thm_2Eextreal_2Ele__sup__imp,lemma,(! [V0p] : ( mem(V0p,arr(ty_2Eextreal_2Eextreal,bool)) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( p(ap(V0p,V1x)) => p(ap(ap(c_2Eextreal_2Eextreal__le,V1x),ap(c_2Eextreal_2Eextreal__sup,V0p))) ) ) ))).
fof(conj_thm_2Eextreal_2Esup__le,conjecture,(! [V0p] : ( mem(V0p,arr(ty_2Eextreal_2Eextreal,bool)) => ! [V1x] : ( mem(V1x,ty_2Eextreal_2Eextreal) => ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2Eextreal__sup,V0p)),V1x)) <=> ! [V2y] : ( mem(V2y,ty_2Eextreal_2Eextreal) => ( p(ap(V0p,V2y)) => p(ap(ap(c_2Eextreal_2Eextreal__le,V2y),V1x)) ) ) ) ) ))).
