include('Axioms/binary_ieee+2.ax').
fof(mem_c_2EHolSmt_2Earray__ext,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2EHolSmt_2Earray__ext(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27a,A_27b),A_27a))) ) ) )).
fof(mem_c_2EHolSmt_2Exor,axiom,( mem(c_2EHolSmt_2Exor,arr(bool,arr(bool,bool))) )).
fof(ax_thm_2EHolSmt_2Exor__def,axiom, ! [V0x] : ( mem(V0x,bool) => ! [V1y] : ( mem(V1y,bool) => ( p(ap(ap(c_2EHolSmt_2Exor,V0x),V1y)) <=> ( ~~ ( p(V0x) <=> p(V1y) ) ) ) ) )).
fof(ax_thm_2EHolSmt_2Earray__ext__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0A] : ( mem(V0A,arr(A_27a,A_27b)) => ! [V1B] : ( mem(V1B,arr(A_27a,A_27b)) => ( ap(ap(c_2EHolSmt_2Earray__ext(A_27a,A_27b),V0A),V1B) = ap(c_2Emin_2E_40(A_27a),f3148(A_27a,A_27b,V1B,V0A)) ) ) ) ) ) )).
fof(conj_thm_2EHolSmt_2EALL__DISTINCT__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),c_2Elist_2ENIL(A_27a))) <=> $true )))).
fof(conj_thm_2EHolSmt_2EALL__DISTINCT__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) <=> ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0h),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1t))) ) & p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1t)) ) ) ) )))).
fof(conj_thm_2EHolSmt_2ENOT__MEM__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),c_2Elist_2ENIL(A_27a)))) ) <=> $true ) )))).
fof(conj_thm_2EHolSmt_2ENOT__MEM__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1h] : ( mem(V1h,A_27a) => ! [V2t] : ( mem(V2t,ty_2Elist_2Elist(A_27a)) => ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t)))) ) <=> ( ( ~~ ( V0x = V1h ) ) & ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2t))) ) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2EAND__T,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) & $true ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2ET__AND,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( $true & p(V0p) ) <=> ( $true & p(V1q) ) ) => ( p(V0p) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EF__OR,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( $false | p(V0p) ) <=> ( $false | p(V1q) ) ) => ( p(V0p) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ECONJ__CONG,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ! [V3s] : ( mem(V3s,bool) => ( ( p(V0p) <=> p(V1q) ) => ( ( p(V2r) <=> p(V3s) ) => ( ( p(V0p) & p(V2r) ) <=> ( p(V1q) & p(V3s) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENOT__NOT__ELIM,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( ~~ ( ~~ p(V0p) ) ) => p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2ENOT__FALSE,lemma,(! [V0p] : ( mem(V0p,bool) => ( p(V0p) => ( ( ~~ p(V0p) ) => $false ) ) ))).
fof(conj_thm_2EHolSmt_2ENNF__CONJ,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ! [V3s] : ( mem(V3s,bool) => ( ( ( ~~ p(V0p) ) <=> p(V2r) ) => ( ( ( ~~ p(V1q) ) <=> p(V3s) ) => ( ( ~~ ( p(V0p) & p(V1q) ) ) <=> ( p(V2r) | p(V3s) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENNF__DISJ,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ! [V3s] : ( mem(V3s,bool) => ( ( ( ~~ p(V0p) ) <=> p(V2r) ) => ( ( ( ~~ p(V1q) ) <=> p(V3s) ) => ( ( ~~ ( p(V0p) | p(V1q) ) ) <=> ( p(V2r) & p(V3s) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENNF__NOT__NOT,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) <=> p(V1q) ) => ( ( ~~ ( ~~ p(V0p) ) ) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENEG__IFF__1__1,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V1q) <=> p(V0p) ) => ( ~~ ( p(V0p) <=> ( ~~ p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENEG__IFF__1__2,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( p(V0p) <=> ( ~~ p(V1q) ) ) ) => ( p(V1q) <=> p(V0p) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENEG__IFF__2__1,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) <=> ( ~~ p(V1q) ) ) => ( ~~ ( p(V0p) <=> p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2ENEG__IFF__2__2,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( p(V0p) <=> p(V1q) ) ) => ( p(V0p) <=> ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EDISJ__ELIM__1,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ( p(V0p) | p(V1q) ) => p(V2r) ) => ( p(V0p) => p(V2r) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EDISJ__ELIM__2,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ( p(V0p) | p(V1q) ) => p(V2r) ) => ( p(V1q) => p(V2r) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EIMP__DISJ__1,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) => p(V1q) ) => ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EIMP__DISJ__2,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) => p(V1q) ) => ( p(V0p) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EIMP__FALSE,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( ( ~~ p(V0p) ) => $false ) => p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2EAND__IMP__INTRO__SYM,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ( p(V0p) & p(V1q) ) => p(V2r) ) <=> ( p(V0p) => ( p(V1q) => p(V2r) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2EVALID__IFF__TRUE,lemma,(! [V0p] : ( mem(V0p,bool) => ( p(V0p) => ( p(V0p) <=> $true ) ) ))).
fof(conj_thm_2EHolSmt_2Ed001,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( p(V0p) <=> p(V1q) ) ) | ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed002,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( p(V0p) <=> p(V1q) ) ) | ( p(V0p) | ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed003,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) <=> ( ~~ p(V1q) ) ) | ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed004,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) <=> p(V1q) ) | ( p(V0p) | ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed005,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) <=> p(V1q) ) | ( ( ~~ p(V0p) ) | ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed006,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) <=> p(V1q) ) | ( p(V0p) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed007,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( ( ~~ p(V0p) ) <=> p(V1q) ) ) | ( p(V0p) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed008,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( p(V0p) <=> ( ~~ p(V1q) ) ) ) | ( p(V0p) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed009,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ p(V0p) ) | ( p(V1q) | ( ~~ ( p(V0p) <=> p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed010,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(V0p) | ( ( ~~ p(V1q) ) | ( ~~ ( p(V0p) <=> p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed011,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(V0p) | ( p(V1q) | ( ~~ ( ( ~~ p(V0p) ) <=> p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed012,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(V0p) | ( p(V1q) | ( ~~ ( p(V0p) <=> ( ~~ p(V1q) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed013,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) & ( ~~ p(V1q) ) ) | ( p(V0p) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed014,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) & p(V1q) ) | ( p(V0p) | ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed015,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & ( ~~ p(V1q) ) ) | ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed016,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & p(V1q) ) | ( ( ~~ p(V0p) ) | ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed017,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2x] : ( mem(V2x,A_27a) => ( p(V0p) | ( V1y = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V2x),V1y) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Ed018,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( ( ~~ p(V0p) ) | ( V1x = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),V2y) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Ed019,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(V0p) | ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),V2y) = V2y ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Ed020,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( ( ~~ p(V0p) ) | ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),V2y) = V1x ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Ed021,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( p(V0p) | ( p(V1q) | ( ~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V2r),V1q)) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed022,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ~~ p(V0p) ) | ( p(V1q) | ( ~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),V2r)) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed023,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),V2r)) | ( ( ~~ p(V0p) ) | ( ~~ p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed024,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),V2r)) | ( p(V0p) | ( ~~ p(V2r) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed025,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),ap(c_2Ebool_2E_7E,V1q)),V2r)) | ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed026,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),ap(c_2Ebool_2E_7E,V2r))) | ( p(V0p) | p(V2r) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed027,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),V2r)) ) | ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Ed028,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ~~ p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),V2r)) ) | ( p(V0p) | p(V2r) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er001,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( ( V0x = V1y ) <=> ( V1y = V0x ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er002,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ( ( V0x = V0x ) <=> $true ) )))).
fof(conj_thm_2EHolSmt_2Er003,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) <=> $true ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er004,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $true <=> p(V0p) ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er005,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) <=> $false ) <=> ( ~~ p(V0p) ) ) ))).
fof(conj_thm_2EHolSmt_2Er006,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $false <=> p(V0p) ) <=> ( ~~ p(V0p) ) ) ))).
fof(conj_thm_2EHolSmt_2Er007,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) <=> ( ~~ p(V1q) ) ) <=> ( p(V0p) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er008,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( p(V0p) <=> ( ~~ p(V1q) ) ) ) <=> ( p(V0p) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er009,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ~~ ( ( ~~ p(V0p) ) <=> p(V1q) ) ) <=> ( p(V0p) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er010,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),c_2Ebool_2ET),V0x),V1y) = V0x ) ) )))).
fof(conj_thm_2EHolSmt_2Er011,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),c_2Ebool_2EF),V0x),V1y) = V1y ) ) )))).
fof(conj_thm_2EHolSmt_2Er012,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),c_2Ebool_2ET)) <=> ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er013,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),c_2Ebool_2ET)) <=> ( p(V1q) | ( ~~ p(V0p) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er014,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),ap(c_2Ebool_2E_7E,V1q))) <=> ( p(V0p) <=> p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er015,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),V1q),ap(c_2Ebool_2E_7E,V1q))) <=> ( p(V1q) <=> p(V0p) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er016,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),ap(c_2Ebool_2E_7E,V1q)),V1q)) <=> ( p(V0p) <=> ( ~~ p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er017,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),ap(c_2Ebool_2E_7E,V1q)),V1q)) <=> ( ( ~~ p(V1q) ) <=> p(V0p) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er018,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(c_2Ebool_2E_7E,V0p)),V1x),V2y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V2y),V1x) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er019,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V1q),V2x),V3y)),V2x) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,V0p),ap(c_2Ebool_2E_7E,V1q))),V3y),V2x) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er020,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V1q),V2x),V3y)),V2x) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,ap(c_2Ebool_2E_7E,V1q)),V0p)),V3y),V2x) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er021,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V1q),V2x),V3y)),V3y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,V0p),V1q)),V2x),V3y) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er022,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V1q),V2x),V3y)),V3y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_2F_5C,V1q),V0p)),V2x),V3y) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er023,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ! [V3z] : ( mem(V3z,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V2y),V3z)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),V3z) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er024,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2q] : ( mem(V2q,bool) => ! [V3y] : ( mem(V3y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V2q),V1x),V3y)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_5C_2F,V0p),V2q)),V1x),V3y) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er025,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2q] : ( mem(V2q,bool) => ! [V3y] : ( mem(V3y,A_27a) => ( ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),ap(ap(ap(c_2Ebool_2ECOND(A_27a),V2q),V1x),V3y)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2E_5C_2F,V2q),V0p)),V1x),V3y) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er026,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ! [V3z] : ( mem(V3z,A_27a) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V3z))) <=> ( V1x = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V2y),V3z) ) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er027,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ! [V3z] : ( mem(V3z,A_27a) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),ap(ap(c_2Emin_2E_3D(A_27a),V2y),V3z))) <=> ( V2y = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),V3z) ) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er028,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0p] : ( mem(V0p,bool) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ! [V3z] : ( mem(V3z,A_27a) => ( p(ap(ap(ap(c_2Ebool_2ECOND(bool),V0p),ap(ap(c_2Emin_2E_3D(A_27a),V1x),V2y)),ap(ap(c_2Emin_2E_3D(A_27a),V3z),V2y))) <=> ( V2y = ap(ap(ap(c_2Ebool_2ECOND(A_27a),V0p),V1x),V3z) ) ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er029,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) => p(V1q) ) <=> ( p(V0p) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er030,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) => p(V1q) ) <=> ( p(V1q) | p(V0p) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er031,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) => p(V1q) ) <=> ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er032,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) => p(V1q) ) <=> ( p(V1q) | ( ~~ p(V0p) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er033,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $true => p(V0p) ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er034,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) => $true ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er035,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $false => p(V0p) ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er036,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) => p(V0p) ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er037,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ! [V2r] : ( mem(V2r,bool) => ( ( ( p(V0p) <=> p(V1q) ) => p(V2r) ) <=> ( p(V2r) | ( p(V1q) <=> ( ~~ p(V0p) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er038,lemma,(( (~~ ($true)) <=> $false ))).
fof(conj_thm_2EHolSmt_2Er039,lemma,(( (~~ ($false)) <=> $true ))).
fof(conj_thm_2EHolSmt_2Er040,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( ~~ ( ~~ p(V0p) ) ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er041,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) | p(V1q) ) <=> ( p(V1q) | p(V0p) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er042,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) | $true ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er043,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) | ( ~~ p(V0p) ) ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er044,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( ( ~~ p(V0p) ) | p(V0p) ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er045,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $true | p(V0p) ) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er046,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) | $false ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er047,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $false | p(V0p) ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er048,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & p(V1q) ) <=> ( p(V1q) & p(V0p) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er049,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) & $true ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er050,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $true & p(V0p) ) <=> p(V0p) ) ))).
fof(conj_thm_2EHolSmt_2Er051,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( p(V0p) & $false ) <=> $false ) ))).
fof(conj_thm_2EHolSmt_2Er052,lemma,(! [V0p] : ( mem(V0p,bool) => ( ( $false & p(V0p) ) <=> $false ) ))).
fof(conj_thm_2EHolSmt_2Er053,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & p(V1q) ) <=> ( ~~ ( ( ~~ p(V0p) ) | ( ~~ p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er054,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) & p(V1q) ) <=> ( ~~ ( p(V0p) | ( ~~ p(V1q) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er055,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & ( ~~ p(V1q) ) ) <=> ( ~~ ( ( ~~ p(V0p) ) | p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er056,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) & ( ~~ p(V1q) ) ) <=> ( ~~ ( p(V0p) | p(V1q) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er057,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & p(V1q) ) <=> ( ~~ ( ( ~~ p(V1q) ) | ( ~~ p(V0p) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er058,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) & p(V1q) ) <=> ( ~~ ( ( ~~ p(V1q) ) | p(V0p) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er059,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( p(V0p) & ( ~~ p(V1q) ) ) <=> ( ~~ ( p(V1q) | ( ~~ p(V0p) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er060,lemma,(! [V0p] : ( mem(V0p,bool) => ! [V1q] : ( mem(V1q,bool) => ( ( ( ~~ p(V0p) ) & ( ~~ p(V1q) ) ) <=> ( ~~ ( p(V1q) | p(V0p) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er061,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ( ap(ap(ap(c_2Ecombin_2EUPDATE(A_27a,A_27b),V0x),ap(V1f,V0x)),V1f) = V1f ) ) ))))).
fof(conj_thm_2EHolSmt_2Er062,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),ap(ap(c_2Elist_2ECONS(A_27a),V0x),c_2Elist_2ENIL(A_27a))))) <=> $false ) )))).
fof(conj_thm_2EHolSmt_2Er063,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),ap(ap(c_2Elist_2ECONS(A_27a),V1y),c_2Elist_2ENIL(A_27a))))) <=> ( ~~ ( V0x = V1y ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er064,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),ap(ap(c_2Elist_2ECONS(A_27a),V1y),c_2Elist_2ENIL(A_27a))))) <=> ( ~~ ( V1y = V0x ) ) ) ) )))).
fof(conj_thm_2EHolSmt_2Er065,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ( V0x = V1y ) <=> ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er066,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,V1y),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)) = V1y ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er067,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),V2z)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er068,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)),V0x)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er069,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,V1y),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z))) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er070,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,V1y),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er071,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,V1y),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),V2z)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er072,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,V1y),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)) = ap(c_2Einteger_2Eint__neg,V1y) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er073,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( V0x = ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V1y)),V2z) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)) = V1y ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er074,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ( ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x) = ap(c_2Einteger_2Eint__neg,V1y) ) <=> ( V0x = V1y ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er075,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),V1y) = V2z ) <=> ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)) = ap(c_2Einteger_2Eint__neg,V2z) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er076,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ( ap(ap(c_2Einteger_2Eint__add,V0x),V1y) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) <=> ( V1y = ap(c_2Einteger_2Eint__neg,V0x) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er077,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ( ap(ap(c_2Einteger_2Eint__add,V0x),V1y) = V2z ) <=> ( ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)) = ap(c_2Einteger_2Eint__neg,V0x) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er078,lemma,(! [V0a] : ( mem(V0a,ty_2Einteger_2Eint) => ! [V1x] : ( mem(V1x,ty_2Einteger_2Eint) => ! [V2v] : ( mem(V2v,ty_2Einteger_2Eint) => ! [V3y] : ( mem(V3y,ty_2Einteger_2Eint) => ! [V4w] : ( mem(V4w,ty_2Einteger_2Eint) => ! [V5z] : ( mem(V5z,ty_2Einteger_2Eint) => ( ( ap(ap(c_2Einteger_2Eint__add,V0a),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1x)),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,V2v),V3y)),ap(ap(c_2Einteger_2Eint__mul,V4w),V5z)))) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) <=> ( ap(ap(c_2Einteger_2Eint__add,V1x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,V2v)),V3y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,V4w)),V5z))) = V0a ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er079,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),V0x) = V0x ) ))).
fof(conj_thm_2EHolSmt_2Er080,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = V0x ) ))).
fof(conj_thm_2EHolSmt_2Er081,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,V0x),V1y) = ap(ap(c_2Einteger_2Eint__add,V1y),V0x) ) ) ))).
fof(conj_thm_2EHolSmt_2Er082,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,V0x),V0x) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0x) ) ))).
fof(conj_thm_2EHolSmt_2Er083,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,V0x),V1y)),V2z) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er084,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,V0x),V1y)),V2z) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,V2z),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er085,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z)) = ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,V2z),V0x)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er086,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z)) = ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,V0x),V2z)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er087,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ! [V3u] : ( mem(V3u,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,V2z),V3u))) = ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__add,V3u),V0x))) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er088,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,V0x),V0x)) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er089,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,V0x),V1y)) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er090,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,V0x),V1y)) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er091,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er092,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__le,V0x),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2EHolSmt_2Er093,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(c_2Einteger_2Eint__neg,V1y))) <=> p(ap(ap(c_2Einteger_2Eint__le,V0x),V1y)) ) ) ))).
fof(conj_thm_2EHolSmt_2Er094,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),V1y)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er095,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__le,V1y),V0x)) ) ) ))).
fof(conj_thm_2EHolSmt_2Er096,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__gt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,V1y),V0x)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er097,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__gt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er098,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__gt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er099,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__gt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er100,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__gt,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),ap(c_2Einteger_2Eint__neg,V1y))) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er101,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),V0x)) <=> $true ) ))).
fof(conj_thm_2EHolSmt_2Er102,lemma,(( p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) <=> $true ))).
fof(conj_thm_2EHolSmt_2Er103,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),V1y)) <=> p(ap(ap(c_2Einteger_2Eint__ge,V1y),V0x)) ) ) ))).
fof(conj_thm_2EHolSmt_2Er104,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V0x)),V1y))) <=> p(ap(ap(c_2Einteger_2Eint__ge,V1y),V0x)) ) ) ))).
fof(conj_thm_2EHolSmt_2Er105,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__ge,V0x),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2EHolSmt_2Er106,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),V1y)) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er107,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),V1y)) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er108,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),V1y)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er109,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),V1y)),ap(c_2Einteger_2Eint__neg,V2z))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),V2z)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er110,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V0x)),V1y)),V2z)) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z))),V0x)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er111,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),V2z)) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er112,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z))),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er113,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z))) <=> p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),ap(c_2Einteger_2Eint__neg,V1y))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er114,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__le,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),V2z))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er115,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,V1y),V0x)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er116,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er117,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er118,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er119,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),V2z)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er120,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),V2z))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er121,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V1y)),V2z))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))),V1y)) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er122,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ! [V3u] : ( mem(V3u,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V1y)),ap(ap(c_2Einteger_2Eint__add,V2z),V3u)))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__add,V3u),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)))),V1y)) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er123,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ! [V3u] : ( mem(V3u,ty_2Einteger_2Eint) => ! [V4v] : ( mem(V4v,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,V0x),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V1y)),ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__add,V3u),V4v))))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__add,V3u),ap(ap(c_2Einteger_2Eint__add,V4v),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x))))),V1y)) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er124,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V0x)),V1y)),V2z)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__ge,ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z))),V0x)) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er125,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,V0x),V1y)),V2z)) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,V2z),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),V0x)) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er126,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V0x)),V1y))) <=> ( ~~ p(ap(ap(c_2Einteger_2Eint__le,V1y),V0x)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er127,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,V0x),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = V0x ) ))).
fof(conj_thm_2EHolSmt_2Er128,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),V0x) = ap(c_2Einteger_2Eint__neg,V0x) ) ))).
fof(conj_thm_2EHolSmt_2Er129,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),V0x) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x) ) ))).
fof(conj_thm_2EHolSmt_2Er130,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,V0x),V1y) = ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,V1y)),V0x) ) ) ))).
fof(conj_thm_2EHolSmt_2Er131,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,V0x),V1y) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)) ) ) ))).
fof(conj_thm_2EHolSmt_2Er132,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,V0x),V1y) = ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y)),V0x) ) ) ))).
fof(conj_thm_2EHolSmt_2Er133,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,V0x),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x) ) ))).
fof(conj_thm_2EHolSmt_2Er134,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__add,V0x),V1y)),V2z) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,V1y),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er135,lemma,(! [V0x] : ( mem(V0x,ty_2Einteger_2Eint) => ! [V1y] : ( mem(V1y,ty_2Einteger_2Eint) => ! [V2z] : ( mem(V2z,ty_2Einteger_2Eint) => ( ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__add,V0x),V1y)),V2z) = ap(ap(c_2Einteger_2Eint__add,V0x),ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z)),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er136,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ( ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x) ) <=> ( ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er137,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x) ) <=> ( ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er138,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3z] : ( mem(V3z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,V1x),ap(ap(c_2Erealax_2Ereal__add,V2y),V3z)) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,V1x),ap(ap(c_2Erealax_2Ereal__add,V2y),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0a)),V3z))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er139,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3z] : ( mem(V3z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,V1x),ap(ap(c_2Erealax_2Ereal__add,V2y),V3z)) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,V1x),ap(ap(c_2Erealax_2Ereal__add,V2y),ap(ap(c_2Erealax_2Ereal__add,V3z),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0a)))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er140,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3v),V4z)) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2y)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4z)),V0a)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er141,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4z)) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2y)),ap(ap(c_2Erealax_2Ereal__add,V0a),ap(ap(c_2Erealax_2Ereal__mul,V3v),V4z))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er142,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ( ( ap(c_2Erealax_2Ereal__neg,V0a) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)) = V0a ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er143,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z)),V0a))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er144,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er145,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er146,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er147,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er148,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( ap(c_2Erealax_2Ereal__neg,V0a) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) = V0a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er149,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( ap(c_2Erealax_2Ereal__neg,V0a) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) = V0a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er150,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( ap(c_2Erealax_2Ereal__neg,V0a) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) = V0a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er151,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3v] : ( mem(V3v,ty_2Erealax_2Ereal) => ! [V4y] : ( mem(V4y,ty_2Erealax_2Ereal) => ! [V5w] : ( mem(V5w,ty_2Erealax_2Ereal) => ! [V6z] : ( mem(V6z,ty_2Erealax_2Ereal) => ( ( ap(c_2Erealax_2Ereal__neg,V0a) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3v)),V4y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V5w)),V6z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V3v),V4y)),ap(ap(c_2Erealax_2Ereal__mul,V5w),V6z))) = V0a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er152,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,V3y),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z))) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er153,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1u] : ( mem(V1u,ty_2Erealax_2Ereal) => ! [V2x] : ( mem(V2x,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( ( V0a = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1u)),V2x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z))) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1u),V2x)),ap(ap(c_2Erealax_2Ereal__add,V3y),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z))) = ap(c_2Erealax_2Ereal__neg,V0a) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er154,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)) = ap(c_2Erealax_2Ereal__neg,V4a) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)) = V4a ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er155,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z))) = ap(c_2Erealax_2Ereal__neg,V5a) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z))) = V5a ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er156,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z))) = ap(c_2Erealax_2Ereal__neg,V6a) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z))) = V6a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er157,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z))) = ap(c_2Erealax_2Ereal__neg,V6a) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z))) = V6a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er158,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z))) = ap(c_2Erealax_2Ereal__neg,V6a) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z))) = V6a ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er159,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,V1y),V0x)) ) ) ))).
fof(conj_thm_2EHolSmt_2Er160,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__ge,V0x),V1y)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er161,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__gt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er162,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,V0x),V1y)) <=> p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V1y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ))).
fof(conj_thm_2EHolSmt_2Er163,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,V0x),ap(ap(c_2Erealax_2Ereal__add,V1y),V2z))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2z))),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er164,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),V2a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(c_2Erealax_2Ereal__neg,V2a))) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er165,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(c_2Erealax_2Ereal__neg,V2a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),V2a)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er166,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er167,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),V4a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er168,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),V4a)) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er169,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),V4a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er170,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),V4a)) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er171,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er172,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er173,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er174,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er175,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er176,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er177,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er178,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er179,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er180,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er181,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er182,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er183,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> p(ap(ap(c_2Ereal_2Ereal__ge,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),V5a)) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er184,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,V0x),V1y)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__ge,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er185,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),V2a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(c_2Erealax_2Ereal__neg,V2a))) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er186,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2a] : ( mem(V2a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(c_2Erealax_2Ereal__neg,V2a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),V2a)) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er187,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er188,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er189,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),V4a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er190,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),V4a)) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er191,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),V4a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er192,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4a] : ( mem(V4a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y))),ap(c_2Erealax_2Ereal__neg,V4a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y))),V4a)) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er193,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er194,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er195,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er196,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er197,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er198,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er199,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),V6a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er200,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ! [V6a] : ( mem(V6a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Erealax_2Ereal__neg,V6a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),V6a)) ) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er201,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er202,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4w] : ( mem(V4w,ty_2Erealax_2Ereal) => ! [V5z] : ( mem(V5z,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V4w)),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,V4w),V5z)))),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er203,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),V5a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er204,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),V5a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er205,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),V5a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er206,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),V5a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er207,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),V5a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er208,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),V5a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er209,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),V5a)) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er210,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1v] : ( mem(V1v,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V1v)),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V1v),V2y)),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),V5a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er211,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2y] : ( mem(V2y,ty_2Erealax_2Ereal) => ! [V3w] : ( mem(V3w,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V2y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V3w)),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,V2y),ap(ap(c_2Erealax_2Ereal__mul,V3w),V4z)))),V5a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er212,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ! [V2v] : ( mem(V2v,ty_2Erealax_2Ereal) => ! [V3y] : ( mem(V3y,ty_2Erealax_2Ereal) => ! [V4z] : ( mem(V4z,ty_2Erealax_2Ereal) => ! [V5a] : ( mem(V5a,ty_2Erealax_2Ereal) => ( p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V2v),V3y)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V4z)))),ap(c_2Erealax_2Ereal__neg,V5a))) <=> ( ~~ p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V2v)),V3y)),V4z))),V5a)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er213,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x) = V0x ) ))).
fof(conj_thm_2EHolSmt_2Er214,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = V0x ) ))).
fof(conj_thm_2EHolSmt_2Er215,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,V0x),V1y) = ap(ap(c_2Erealax_2Ereal__add,V1y),V0x) ) ) ))).
fof(conj_thm_2EHolSmt_2Er216,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,V0x),V0x) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0x) ) ))).
fof(conj_thm_2EHolSmt_2Er217,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)),V2z) = ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,V1y),V2z)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er218,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)),V2z) = ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,V2z),V1y)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er219,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,V1y),V2z)) = ap(ap(c_2Erealax_2Ereal__add,V1y),ap(ap(c_2Erealax_2Ereal__add,V2z),V0x)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er220,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,V0x),ap(ap(c_2Erealax_2Ereal__add,V1y),V2z)) = ap(ap(c_2Erealax_2Ereal__add,V1y),ap(ap(c_2Erealax_2Ereal__add,V0x),V2z)) ) ) ) ))).
fof(conj_thm_2EHolSmt_2Er221,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0x) = ap(c_2Erealax_2Ereal__neg,V0x) ) ))).
fof(conj_thm_2EHolSmt_2Er222,lemma,(! [V0u] : ( mem(V0u,ty_2Erealax_2Ereal) => ! [V1x] : ( mem(V1x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(ap(c_2Erealax_2Ereal__mul,V0u),V1x)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Erealax_2Ereal__neg,V0u)),V1x) ) ) ))).
fof(conj_thm_2EHolSmt_2Er223,conjecture,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ereal_2Ereal__sub,V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = V0x ) ))).
