include('Axioms/nets+2.ax').
fof(ne_ty_2Erat_2Erat,axiom,( ne(ty_2Erat_2Erat) )).
fof(mem_c_2Erat_2ERATD,axiom,( mem(c_2Erat_2ERATD,arr(ty_2Erat_2Erat,ty_2Enum_2Enum)) )).
fof(mem_c_2Erat_2ERATN,axiom,( mem(c_2Erat_2ERATN,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint)) )).
fof(mem_c_2Erat_2Eabs__rat,axiom,( mem(c_2Erat_2Eabs__rat,arr(ty_2Efrac_2Efrac,ty_2Erat_2Erat)) )).
fof(mem_c_2Erat_2Eabs__rat__CLASS,axiom,( mem(c_2Erat_2Eabs__rat__CLASS,arr(arr(ty_2Efrac_2Efrac,bool),ty_2Erat_2Erat)) )).
fof(mem_c_2Erat_2Erat__0,axiom,( mem(c_2Erat_2Erat__0,ty_2Erat_2Erat) )).
fof(mem_c_2Erat_2Erat__1,axiom,( mem(c_2Erat_2Erat__1,ty_2Erat_2Erat) )).
fof(mem_c_2Erat_2Erat__add,axiom,( mem(c_2Erat_2Erat__add,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erat__ainv,axiom,( mem(c_2Erat_2Erat__ainv,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)) )).
fof(mem_c_2Erat_2Erat__cons,axiom,( mem(c_2Erat_2Erat__cons,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erat__div,axiom,( mem(c_2Erat_2Erat__div,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erat__dnm,axiom,( mem(c_2Erat_2Erat__dnm,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint)) )).
fof(mem_c_2Erat_2Erat__equiv,axiom,( mem(c_2Erat_2Erat__equiv,arr(ty_2Efrac_2Efrac,arr(ty_2Efrac_2Efrac,bool))) )).
fof(mem_c_2Erat_2Erat__geq,axiom,( mem(c_2Erat_2Erat__geq,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool))) )).
fof(mem_c_2Erat_2Erat__gre,axiom,( mem(c_2Erat_2Erat__gre,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool))) )).
fof(mem_c_2Erat_2Erat__leq,axiom,( mem(c_2Erat_2Erat__leq,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool))) )).
fof(mem_c_2Erat_2Erat__les,axiom,( mem(c_2Erat_2Erat__les,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,bool))) )).
fof(mem_c_2Erat_2Erat__max,axiom,( mem(c_2Erat_2Erat__max,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erat__min,axiom,( mem(c_2Erat_2Erat__min,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erat__minv,axiom,( mem(c_2Erat_2Erat__minv,arr(ty_2Erat_2Erat,ty_2Erat_2Erat)) )).
fof(mem_c_2Erat_2Erat__mul,axiom,( mem(c_2Erat_2Erat__mul,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erat__nmr,axiom,( mem(c_2Erat_2Erat__nmr,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint)) )).
fof(mem_c_2Erat_2Erat__of__int,axiom,( mem(c_2Erat_2Erat__of__int,arr(ty_2Einteger_2Eint,ty_2Erat_2Erat)) )).
fof(mem_c_2Erat_2Erat__of__num,axiom,( mem(c_2Erat_2Erat__of__num,arr(ty_2Enum_2Enum,ty_2Erat_2Erat)) )).
fof(mem_c_2Erat_2Erat__sgn,axiom,( mem(c_2Erat_2Erat__sgn,arr(ty_2Erat_2Erat,ty_2Einteger_2Eint)) )).
fof(mem_c_2Erat_2Erat__sub,axiom,( mem(c_2Erat_2Erat__sub,arr(ty_2Erat_2Erat,arr(ty_2Erat_2Erat,ty_2Erat_2Erat))) )).
fof(mem_c_2Erat_2Erep__rat,axiom,( mem(c_2Erat_2Erep__rat,arr(ty_2Erat_2Erat,ty_2Efrac_2Efrac)) )).
fof(mem_c_2Erat_2Erep__rat__CLASS,axiom,( mem(c_2Erat_2Erep__rat__CLASS,arr(ty_2Erat_2Erat,arr(ty_2Efrac_2Efrac,bool))) )).
fof(ax_thm_2Erat_2Erat__equiv__def,axiom, ! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0f1),V1f2)) <=> ( ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Efrac_2Efrac__dnm,V1f2)) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V1f2)),ap(c_2Efrac_2Efrac__dnm,V0f1)) ) ) ) )).
fof(conj_thm_2Erat_2ERAT__EQUIV__REF,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => p(ap(ap(c_2Erat_2Erat__equiv,V0a),V0a)) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV__SYM,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ! [V1b] : ( mem(V1b,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0a),V1b)) <=> p(ap(ap(c_2Erat_2Erat__equiv,V1b),V0a)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV__NMR__Z__IFF,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ! [V1b] : ( mem(V1b,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0a),V1b)) => ( ( ap(c_2Efrac_2Efrac__nmr,V0a) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) <=> ( ap(c_2Efrac_2Efrac__nmr,V1b) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV__NMR__GTZ__IFF,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ! [V1b] : ( mem(V1b,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0a),V1b)) => ( p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,V0a)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,V1b)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV__NMR__LTZ__IFF,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ! [V1b] : ( mem(V1b,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0a),V1b)) => ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,V0a)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,V1b)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NMR__Z__IFF__EQUIV,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ! [V1b] : ( mem(V1b,ty_2Efrac_2Efrac) => ( ( ap(c_2Efrac_2Efrac__nmr,V0a) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0a),V1b)) <=> ( ap(c_2Efrac_2Efrac__nmr,V1b) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV__TRANS,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ! [V1b] : ( mem(V1b,ty_2Efrac_2Efrac) => ! [V2c] : ( mem(V2c,ty_2Efrac_2Efrac) => ( ( p(ap(ap(c_2Erat_2Erat__equiv,V0a),V1b)) & p(ap(ap(c_2Erat_2Erat__equiv,V1b),V2c)) ) => p(ap(ap(c_2Erat_2Erat__equiv,V0a),V2c)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0f1),V1f2)) <=> ( ap(c_2Erat_2Erat__equiv,V0f1) = ap(c_2Erat_2Erat__equiv,V1f2) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQUIV__ALT,lemma,(! [V0a] : ( mem(V0a,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Erat__equiv,V0a) = f2853(V0a) ) ))).
fof(ax_thm_2Erat_2Erat__TY__DEF,axiom, ? [V0rep] : ( mem(V0rep,arr(ty_2Erat_2Erat,arr(ty_2Efrac_2Efrac,bool))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(arr(ty_2Efrac_2Efrac,bool),ty_2Erat_2Erat),f2855),V0rep)) )).
fof(ax_thm_2Erat_2Erat__bijections,axiom, ( ( ! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(c_2Erat_2Eabs__rat__CLASS,ap(c_2Erat_2Erep__rat__CLASS,V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,arr(ty_2Efrac_2Efrac,bool)) => ( p(ap(f2857,V1r)) <=> ( ap(c_2Erat_2Erep__rat__CLASS,ap(c_2Erat_2Eabs__rat__CLASS,V1r)) = V1r ) ) ) )).
fof(conj_thm_2Erat_2Erat__ABS__REP__CLASS,lemma,(( ( ! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(c_2Erat_2Eabs__rat__CLASS,ap(c_2Erat_2Erep__rat__CLASS,V0a)) = V0a ) ) ) & ! [V1c] : ( mem(V1c,arr(ty_2Efrac_2Efrac,bool)) => ( ( ? [V2r] : ( mem(V2r,ty_2Efrac_2Efrac) & ( p(ap(ap(c_2Erat_2Erat__equiv,V2r),V2r)) & ( V1c = ap(c_2Erat_2Erat__equiv,V2r) ) ) ) ) <=> ( ap(c_2Erat_2Erep__rat__CLASS,ap(c_2Erat_2Eabs__rat__CLASS,V1c)) = V1c ) ) ) ))).
fof(ax_thm_2Erat_2Erep__rat__def,axiom, ! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erep__rat,V0a) = ap(c_2Emin_2E_40(ty_2Efrac_2Efrac),ap(c_2Erat_2Erep__rat__CLASS,V0a)) ) )).
fof(ax_thm_2Erat_2Eabs__rat__def,axiom, ! [V0r] : ( mem(V0r,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,V0r) = ap(c_2Erat_2Eabs__rat__CLASS,ap(c_2Erat_2Erat__equiv,V0r)) ) )).
fof(conj_thm_2Erat_2Erat__QUOTIENT,lemma,(p(ap(ap(ap(c_2Equotient_2EQUOTIENT(ty_2Efrac_2Efrac,ty_2Erat_2Erat),c_2Erat_2Erat__equiv),c_2Erat_2Eabs__rat),c_2Erat_2Erep__rat)))).
fof(conj_thm_2Erat_2Erat__def,lemma,(p(ap(ap(ap(c_2Equotient_2EQUOTIENT(ty_2Efrac_2Efrac,ty_2Erat_2Erat),c_2Erat_2Erat__equiv),c_2Erat_2Eabs__rat),c_2Erat_2Erep__rat)))).
fof(conj_thm_2Erat_2Erat__type__thm,lemma,(( ( ! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(c_2Erat_2Eabs__rat,ap(c_2Erat_2Erep__rat,V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,ty_2Efrac_2Efrac) => ! [V2s] : ( mem(V2s,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V1r),V2s)) <=> ( ap(c_2Erat_2Eabs__rat,V1r) = ap(c_2Erat_2Eabs__rat,V2s) ) ) ) ) ))).
fof(conj_thm_2Erat_2Erat__equiv__reps,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__equiv,ap(c_2Erat_2Erep__rat,V0r1)),ap(c_2Erat_2Erep__rat,V1r2))) <=> ( V0r1 = V1r2 ) ) ) ))).
fof(conj_thm_2Erat_2Erat__equiv__rep__abs,lemma,(! [V0f] : ( mem(V0f,ty_2Efrac_2Efrac) => p(ap(ap(c_2Erat_2Erat__equiv,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0f))),V0f)) ))).
fof(ax_thm_2Erat_2Erat__nmr__def,axiom, ! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__nmr,V0r) = ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,V0r)) ) )).
fof(ax_thm_2Erat_2Erat__dnm__def,axiom, ! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__dnm,V0r) = ap(c_2Efrac_2Efrac__dnm,ap(c_2Erat_2Erep__rat,V0r)) ) )).
fof(ax_thm_2Erat_2Erat__sgn__def,axiom, ! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__sgn,V0r) = ap(c_2Efrac_2Efrac__sgn,ap(c_2Erat_2Erep__rat,V0r)) ) )).
fof(ax_thm_2Erat_2Erat__0__def,axiom, ( c_2Erat_2Erat__0 = ap(c_2Erat_2Eabs__rat,c_2Efrac_2Efrac__0) )).
fof(ax_thm_2Erat_2Erat__1__def,axiom, ( c_2Erat_2Erat__1 = ap(c_2Erat_2Eabs__rat,c_2Efrac_2Efrac__1) )).
fof(ax_thm_2Erat_2Erat__ainv__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__ainv,V0r1) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,ap(c_2Erat_2Erep__rat,V0r1))) ) )).
fof(ax_thm_2Erat_2Erat__minv__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__minv,V0r1) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,ap(c_2Erat_2Erep__rat,V0r1))) ) )).
fof(ax_thm_2Erat_2Erat__add__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,V0r1),V1r2) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,ap(c_2Erat_2Erep__rat,V0r1)),ap(c_2Erat_2Erep__rat,V1r2))) ) ) )).
fof(ax_thm_2Erat_2Erat__sub__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,ap(c_2Erat_2Erep__rat,V0r1)),ap(c_2Erat_2Erep__rat,V1r2))) ) ) )).
fof(ax_thm_2Erat_2Erat__mul__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,ap(c_2Erat_2Erep__rat,V0r1)),ap(c_2Erat_2Erep__rat,V1r2))) ) ) )).
fof(ax_thm_2Erat_2Erat__div__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__div,V0r1),V1r2) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,ap(c_2Erat_2Erep__rat,V0r1)),ap(c_2Erat_2Erep__rat,V1r2))) ) ) )).
fof(ax_thm_2Erat_2Erat__les__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) <=> ( ap(c_2Erat_2Erat__sgn,ap(ap(c_2Erat_2Erat__sub,V1r2),V0r1)) = ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) )).
fof(ax_thm_2Erat_2Erat__gre__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__gre,V0r1),V1r2)) <=> p(ap(ap(c_2Erat_2Erat__les,V1r2),V0r1)) ) ) )).
fof(ax_thm_2Erat_2Erat__leq__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) <=> ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) | ( V0r1 = V1r2 ) ) ) ) )).
fof(ax_thm_2Erat_2Erat__geq__def,axiom, ! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__geq,V0r1),V1r2)) <=> p(ap(ap(c_2Erat_2Erat__leq,V1r2),V0r1)) ) ) )).
fof(ax_thm_2Erat_2Erat__cons__def,axiom, ! [V0nmr] : ( mem(V0nmr,ty_2Einteger_2Eint) => ! [V1dnm] : ( mem(V1dnm,ty_2Einteger_2Eint) => ( ap(ap(c_2Erat_2Erat__cons,V0nmr),V1dnm) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Eabs__frac,ap(ap(c_2Epair_2E_2C(ty_2Einteger_2Eint,ty_2Einteger_2Eint),ap(ap(c_2Einteger_2Eint__mul,ap(ap(c_2Einteger_2Eint__mul,ap(c_2EintExtension_2ESGN,V0nmr)),ap(c_2EintExtension_2ESGN,V1dnm))),ap(c_2Einteger_2EABS,V0nmr))),ap(c_2Einteger_2EABS,V1dnm)))) ) ) )).
fof(ax_thm_2Erat_2Erat__of__num__primitive__def,axiom, ( c_2Erat_2Erat__of__num = ap(ap(c_2Erelation_2EWFREC(ty_2Enum_2Enum,ty_2Erat_2Erat),ap(c_2Emin_2E_40(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),f2859)),f2863) )).
fof(conj_thm_2Erat_2Erat__of__num__ind,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ( p(ap(V0P,c_2Enum_2E0)) & ( p(ap(V0P,ap(c_2Enum_2ESUC,c_2Enum_2E0))) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(V0P,ap(c_2Enum_2ESUC,V1n))) => p(ap(V0P,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,V1n)))) ) ) ) ) => ! [V2v] : ( mem(V2v,ty_2Enum_2Enum) => p(ap(V0P,V2v)) ) ) ))).
fof(conj_thm_2Erat_2Erat__of__num__def,lemma,(( ( ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) = c_2Erat_2Erat__0 ) & ( ( ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,c_2Enum_2E0)) = c_2Erat_2Erat__1 ) & ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,V0n))) = ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,V0n))),c_2Erat_2Erat__1) ) ) ) ))).
fof(conj_thm_2Erat_2Erat__of__num__def__compute,lemma,(( ( ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) = c_2Erat_2Erat__0 ) & ( ( ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,c_2Enum_2E0)) = c_2Erat_2Erat__1 ) & ( ( ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n)))) = ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n)))),c_2Erat_2Erat__1) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V1n)))) = ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V1n)))),c_2Erat_2Erat__1) ) ) ) ) ))).
fof(conj_thm_2Erat_2Erat__0,lemma,(( ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) = ap(c_2Erat_2Eabs__rat,c_2Efrac_2Efrac__0) ))).
fof(conj_thm_2Erat_2Erat__1,lemma,(( ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = ap(c_2Erat_2Eabs__rat,c_2Efrac_2Efrac__1) ))).
fof(conj_thm_2Erat_2ERAT,lemma,(! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(c_2Erat_2Eabs__rat,ap(c_2Erat_2Erep__rat,V0r)) = V0r ) ))).
fof(conj_thm_2Erat_2ERAT__ABS__EQUIV,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ( ap(c_2Erat_2Eabs__rat,V0f1) = ap(c_2Erat_2Eabs__rat,V1f2) ) <=> p(ap(ap(c_2Erat_2Erat__equiv,V0f1),V1f2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ( ap(c_2Erat_2Eabs__rat,V0f1) = ap(c_2Erat_2Eabs__rat,V1f2) ) <=> ( ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Efrac_2Efrac__dnm,V1f2)) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V1f2)),ap(c_2Efrac_2Efrac__dnm,V0f1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__ALT,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( V0r1 = V1r2 ) <=> ( ap(ap(c_2Einteger_2Eint__mul,ap(c_2Erat_2Erat__nmr,V0r1)),ap(c_2Erat_2Erat__dnm,V1r2)) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Erat_2Erat__nmr,V1r2)),ap(c_2Erat_2Erat__dnm,V0r1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NMREQ0__CONG,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( ( ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0f1))) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) <=> ( ap(c_2Efrac_2Efrac__nmr,V0f1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NMRLT0__CONG,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0f1)))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2Erat_2ERAT__NMRGT0__CONG,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0f1)))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__gt,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__CONG,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( ap(c_2Efrac_2Efrac__sgn,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0f1))) = ap(c_2Efrac_2Efrac__sgn,V0f1) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__CONG,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x)))) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,V0x)) ) ))).
fof(conj_thm_2Erat_2EFRAC__MINV__EQUIV,lemma,(! [V0y] : ( mem(V0y,ty_2Efrac_2Efrac) => ! [V1x] : ( mem(V1x,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V0y) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( p(ap(ap(c_2Erat_2Erat__equiv,V1x),V0y)) => p(ap(ap(c_2Erat_2Erat__equiv,ap(c_2Efrac_2Efrac__minv,V1x)),ap(c_2Efrac_2Efrac__minv,V0y))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MINV__CONG,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V0x) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x)))) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,V0x)) ) ) ))).
fof(conj_thm_2Erat_2EFRAC__ADD__EQUIV1,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1x_27] : ( mem(V1x_27,ty_2Efrac_2Efrac) => ! [V2y] : ( mem(V2y,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0x),V1x_27)) => p(ap(ap(c_2Erat_2Erat__equiv,ap(ap(c_2Efrac_2Efrac__add,V0x),V2y)),ap(ap(c_2Efrac_2Efrac__add,V1x_27),V2y))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__CONG1,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V0x),V1y)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__CONG2,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V0x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V1y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V0x),V1y)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__CONG,lemma,(( ( ! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V0x),V1y)) ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Efrac_2Efrac) => ! [V3y] : ( mem(V3y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V2x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V3y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V2x),V3y)) ) ) ) ))).
fof(conj_thm_2Erat_2EFRAC__MUL__EQUIV1,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1x_27] : ( mem(V1x_27,ty_2Efrac_2Efrac) => ! [V2y] : ( mem(V2y,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0x),V1x_27)) => p(ap(ap(c_2Erat_2Erat__equiv,ap(ap(c_2Efrac_2Efrac__mul,V0x),V2y)),ap(ap(c_2Efrac_2Efrac__mul,V1x_27),V2y))) ) ) ) ))).
fof(conj_thm_2Erat_2EFRAC__MUL__EQUIV2,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1x_27] : ( mem(V1x_27,ty_2Efrac_2Efrac) => ! [V2y] : ( mem(V2y,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__equiv,V0x),V1x_27)) => p(ap(ap(c_2Erat_2Erat__equiv,ap(ap(c_2Efrac_2Efrac__mul,V2y),V0x)),ap(ap(c_2Efrac_2Efrac__mul,V2y),V1x_27))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__CONG1,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V0x),V1y)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__CONG2,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V0x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V1y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V0x),V1y)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__CONG,lemma,(( ( ! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V0x),V1y)) ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Efrac_2Efrac) => ! [V3y] : ( mem(V3y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V2x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V3y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V2x),V3y)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__CONG1,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V0x),V1y)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__CONG2,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V0x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V1y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V0x),V1y)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__CONG,lemma,(( ( ! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V0x),V1y)) ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Efrac_2Efrac) => ! [V3y] : ( mem(V3y,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V2x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V3y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V2x),V3y)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__CONG1,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V1y) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__CONG2,lemma,(! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V1y) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V0x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V1y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V0x),V1y)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__CONG,lemma,(( ( ! [V0x] : ( mem(V0x,ty_2Efrac_2Efrac) => ! [V1y] : ( mem(V1y,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V1y) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V0x))),V1y)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V0x),V1y)) ) ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Efrac_2Efrac) => ! [V3y] : ( mem(V3y,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V3y) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V2x),ap(c_2Erat_2Erep__rat,ap(c_2Erat_2Eabs__rat,V3y)))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V2x),V3y)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NMRDNM__EQ,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( ( ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Eabs__frac,ap(ap(c_2Epair_2E_2C(ty_2Einteger_2Eint,ty_2Einteger_2Eint),ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Efrac_2Efrac__dnm,V0f1)))) = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) <=> ( ap(c_2Efrac_2Efrac__nmr,V0f1) = ap(c_2Efrac_2Efrac__dnm,V0f1) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Eabs__rat,V0f1)) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__ainv,V0f1)) ) ))).
fof(conj_thm_2Erat_2ERAT__MINV__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) = ap(c_2Efrac_2Efrac__nmr,V0f1) ) ) => ( ap(c_2Erat_2Erat__minv,ap(c_2Erat_2Eabs__rat,V0f1)) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Efrac__minv,V0f1)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Eabs__rat,V0f1)),ap(c_2Erat_2Eabs__rat,V1f2)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__add,V0f1),V1f2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ap(ap(c_2Erat_2Erat__sub,ap(c_2Erat_2Eabs__rat,V0f1)),ap(c_2Erat_2Eabs__rat,V1f2)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__sub,V0f1),V1f2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Eabs__rat,V0f1)),ap(c_2Erat_2Eabs__rat,V1f2)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__mul,V0f1),V1f2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ( ~~ ( ap(c_2Efrac_2Efrac__nmr,V1f2) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Erat_2Erat__div,ap(c_2Erat_2Eabs__rat,V0f1)),ap(c_2Erat_2Eabs__rat,V1f2)) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__div,V0f1),V1f2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( ( ap(c_2Erat_2Eabs__rat,V0f1) = ap(c_2Erat_2Eabs__rat,V1f2) ) <=> ( ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Efrac_2Efrac__dnm,V1f2)) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V1f2)),ap(c_2Efrac_2Efrac__dnm,V0f1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Eabs__rat,V0f1)),ap(c_2Erat_2Eabs__rat,V1f2))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Efrac_2Efrac__dnm,V1f2))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V1f2)),ap(c_2Efrac_2Efrac__dnm,V0f1)))) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ! [V1f2] : ( mem(V1f2,ty_2Efrac_2Efrac) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Eabs__rat,V0f1)),ap(c_2Erat_2Eabs__rat,V1f2))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V0f1)),ap(c_2Efrac_2Efrac__dnm,V1f2))),ap(ap(c_2Einteger_2Eint__mul,ap(c_2Efrac_2Efrac__nmr,V1f2)),ap(c_2Efrac_2Efrac__dnm,V0f1)))) ) ) ))).
fof(conj_thm_2Erat_2ERAT__OF__NUM__CALCULATE,lemma,(! [V0n1] : ( mem(V0n1,ty_2Enum_2Enum) => ( ap(c_2Erat_2Erat__of__num,V0n1) = ap(c_2Erat_2Eabs__rat,ap(c_2Efrac_2Eabs__frac,ap(ap(c_2Epair_2E_2C(ty_2Einteger_2Eint,ty_2Einteger_2Eint),ap(c_2Einteger_2Eint__of__num,V0n1)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))) ) ))).
fof(conj_thm_2Erat_2ERAT__OF__NUM__LEQ,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Erat__of__num,V0a)),ap(c_2Erat_2Erat__of__num,V1b))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V0a),V1b)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__OF__NUM__LES,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,V0a)),ap(c_2Erat_2Erat__of__num,V1b))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0a),V1b)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ0__NMR,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) <=> ( ap(c_2Erat_2Erat__nmr,V0r1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Erat_2ERAT__0LES__NMR,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1)) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Erat_2Erat__nmr,V0r1))) ) ))).
fof(conj_thm_2Erat_2ERAT__LES0__NMR,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Erat_2Erat__nmr,V0r1)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2Erat_2ERAT__0LEQ__NMR,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1)) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),ap(c_2Erat_2Erat__nmr,V0r1))) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ0__NMR,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Erat_2Erat__nmr,V0r1)),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__ASSOC,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,V0a),ap(ap(c_2Erat_2Erat__add,V1b),V2c)) = ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__add,V0a),V1b)),V2c) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__ASSOC,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V0a),ap(ap(c_2Erat_2Erat__mul,V1b),V2c)) = ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__mul,V0a),V1b)),V2c) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__COMM,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,V0a),V1b) = ap(ap(c_2Erat_2Erat__add,V1b),V0a) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__COMM,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V0a),V1b) = ap(ap(c_2Erat_2Erat__mul,V1b),V0a) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__RID,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,V0a),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)) = V0a ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__LID,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0a) = V0a ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__RID,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V0a),ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0a ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__LID,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0a) = V0a ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__RINV,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,V0a),ap(c_2Erat_2Erat__ainv,V0a)) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__LINV,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__ainv,V0a)),V0a) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__RINV,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ( ~~ ( V0a = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Erat_2Erat__mul,V0a),ap(c_2Erat_2Erat__minv,V0a)) = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__LINV,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ( ( ~~ ( V0a = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__minv,V0a)),V0a) = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RDISTRIB,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__add,V0a),V1b)),V2c) = ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__mul,V0a),V2c)),ap(ap(c_2Erat_2Erat__mul,V1b),V2c)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LDISTRIB,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V2c),ap(ap(c_2Erat_2Erat__add,V0a),V1b)) = ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__mul,V2c),V0a)),ap(ap(c_2Erat_2Erat__mul,V2c),V1b)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__1__NOT__0,lemma,(( ~~ ( ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__LZERO,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__RZERO,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__ADDAINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2) = ap(ap(c_2Erat_2Erat__add,V0r1),ap(c_2Erat_2Erat__ainv,V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__MULMINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__div,V0r1),V1r2) = ap(ap(c_2Erat_2Erat__mul,V0r1),ap(c_2Erat_2Erat__minv,V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__0,lemma,(! [V0x] : ( mem(V0x,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__div,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0x) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__0,lemma,(( ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Erat_2ERAT__AINV__AINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__ainv,V0r1)) = V0r1 ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__ADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__add,V0r1),V1r2)) = ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__ainv,V0r1)),ap(c_2Erat_2Erat__ainv,V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__SUB,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2)) = ap(ap(c_2Erat_2Erat__sub,V1r2),V0r1) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__RMUL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2)) = ap(ap(c_2Erat_2Erat__mul,V0r1),ap(c_2Erat_2Erat__ainv,V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__LMUL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__ainv,ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2)) = ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__ainv,V0r1)),V1r2) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__EQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ap(c_2Erat_2Erat__ainv,V0r1) = V1r2 ) <=> ( V0r1 = ap(c_2Erat_2Erat__ainv,V1r2) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__AINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ap(c_2Erat_2Erat__ainv,V0r1) = ap(c_2Erat_2Erat__ainv,V1r2) ) <=> ( V0r1 = V1r2 ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__MINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( ~~ ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__minv,V0r1)) = ap(c_2Erat_2Erat__minv,ap(c_2Erat_2Erat__ainv,V0r1)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__RDISTRIB,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__sub,V0a),V1b)),V2c) = ap(ap(c_2Erat_2Erat__sub,ap(ap(c_2Erat_2Erat__mul,V0a),V2c)),ap(ap(c_2Erat_2Erat__mul,V1b),V2c)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__LDISTRIB,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V2c),ap(ap(c_2Erat_2Erat__sub,V0a),V1b)) = ap(ap(c_2Erat_2Erat__sub,ap(ap(c_2Erat_2Erat__mul,V2c),V0a)),ap(ap(c_2Erat_2Erat__mul,V2c),V1b)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__LID,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__sub,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1) = ap(c_2Erat_2Erat__ainv,V0r1) ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__RID,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__sub,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)) = V0r1 ) ))).
fof(conj_thm_2Erat_2ERAT__SUB__ID,lemma,(! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__sub,V0r),V0r) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__SUB0,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) <=> ( V0r1 = V1r2 ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__0SUB,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) = ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2) ) <=> ( V0r1 = V1r2 ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__CALCULATE,lemma,(! [V0f1] : ( mem(V0f1,ty_2Efrac_2Efrac) => ( ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Eabs__rat,V0f1)) = ap(c_2Efrac_2Efrac__sgn,V0f1) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__CLAUSES,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) & ( ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) <=> ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) & ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) <=> p(ap(ap(c_2Erat_2Erat__gre,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__0,lemma,(( ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Erat_2ERAT__SGN__AINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ap(c_2Einteger_2Eint__neg,ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Erat__ainv,V0r1))) = ap(c_2Erat_2Erat__sgn,V0r1) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__MUL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ap(c_2Erat_2Erat__sgn,ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2)) = ap(ap(c_2Einteger_2Eint__mul,ap(c_2Erat_2Erat__sgn,V0r1)),ap(c_2Erat_2Erat__sgn,V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__MINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( ~~ ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Erat__sgn,ap(c_2Erat_2Erat__minv,V0r1)) = ap(c_2Erat_2Erat__sgn,V0r1) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__TOTAL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) | ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) | ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SGN__COMPLEMENT,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( ( ~~ ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) <=> ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) | ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ( ( ( ~~ ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) <=> ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) | ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ( ( ~~ ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) <=> ( ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) | ( ap(c_2Erat_2Erat__sgn,V0r1) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__REF,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ~~ p(ap(ap(c_2Erat_2Erat__les,V0r1),V0r1)) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__ANTISYM,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) => ( ~~ p(ap(ap(c_2Erat_2Erat__les,V1r2),V0r1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__TRANS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) & p(ap(ap(c_2Erat_2Erat__les,V1r2),V2r3)) ) => p(ap(ap(c_2Erat_2Erat__les,V0r1),V2r3)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__TOTAL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) | ( ( V0r1 = V1r2 ) | p(ap(ap(c_2Erat_2Erat__les,V1r2),V0r1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__REF,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => p(ap(ap(c_2Erat_2Erat__leq,V0r1),V0r1)) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__ANTISYM,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) & p(ap(ap(c_2Erat_2Erat__leq,V1r2),V0r1)) ) => ( V0r1 = V1r2 ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__TRANS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) & p(ap(ap(c_2Erat_2Erat__leq,V1r2),V2r3)) ) => p(ap(ap(c_2Erat_2Erat__leq,V0r1),V2r3)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__01,lemma,(p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))).
fof(conj_thm_2Erat_2ERAT__LES__IMP__LEQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) => p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__IMP__NEQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) => ( ~~ ( V0r1 = V1r2 ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__LES,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ~~ p(ap(ap(c_2Erat_2Erat__les,V1r2),V0r1)) ) <=> p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__LEQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ~~ p(ap(ap(c_2Erat_2Erat__leq,V1r2),V0r1)) ) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__LEQ2,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) <=> ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) & ( ~~ p(ap(ap(c_2Erat_2Erat__leq,V1r2),V0r1)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__LEQ__TRANS,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__les,V0a),V1b)) & p(ap(ap(c_2Erat_2Erat__leq,V1b),V2c)) ) => p(ap(ap(c_2Erat_2Erat__les,V0a),V2c)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__LES__TRANS,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__leq,V0a),V1b)) & p(ap(ap(c_2Erat_2Erat__les,V1b),V2c)) ) => p(ap(ap(c_2Erat_2Erat__les,V0a),V2c)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__0LES__0LES__ADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1)) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V1r2)) => p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),ap(ap(c_2Erat_2Erat__add,V0r1),V1r2))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES0__LES0__ADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__les,V1r2),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,V0r1),V1r2)),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__0LES__0LEQ__ADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1)) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V1r2)) => p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),ap(ap(c_2Erat_2Erat__add,V0r1),V1r2))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES0__LEQ0__ADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__leq,V1r2),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,V0r1),V1r2)),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LSUB__EQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2) = V2r3 ) <=> ( V0r1 = ap(ap(c_2Erat_2Erat__add,V1r2),V2r3) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RSUB__EQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( V0r1 = ap(ap(c_2Erat_2Erat__sub,V1r2),V2r3) ) <=> ( ap(ap(c_2Erat_2Erat__add,V0r1),V2r3) = V1r2 ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LDIV__EQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ~~ ( V1r2 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ( ap(ap(c_2Erat_2Erat__div,V0r1),V1r2) = V2r3 ) <=> ( V0r1 = ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3) ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RDIV__EQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ~~ ( V2r3 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ( V0r1 = ap(ap(c_2Erat_2Erat__div,V1r2),V2r3) ) <=> ( ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3) = V1r2 ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__ONE__ONE,lemma,(p(ap(c_2Ebool_2EONE__ONE(ty_2Erat_2Erat,ty_2Erat_2Erat),c_2Erat_2Erat__ainv)))).
fof(conj_thm_2Erat_2ERAT__ADD__ONE__ONE,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => p(ap(c_2Ebool_2EONE__ONE(ty_2Erat_2Erat,ty_2Erat_2Erat),ap(c_2Erat_2Erat__add,V0r1))) ))).
fof(conj_thm_2Erat_2ERAT__MUL__ONE__ONE,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( ( ~~ ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) <=> p(ap(c_2Ebool_2EONE__ONE(ty_2Erat_2Erat,ty_2Erat_2Erat),ap(c_2Erat_2Erat__mul,V0r1))) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__LADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ap(ap(c_2Erat_2Erat__add,V2r3),V0r1) = ap(ap(c_2Erat_2Erat__add,V2r3),V1r2) ) <=> ( V0r1 = V1r2 ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__RADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ap(ap(c_2Erat_2Erat__add,V0r1),V2r3) = ap(ap(c_2Erat_2Erat__add,V1r2),V2r3) ) <=> ( V0r1 = V1r2 ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__RMUL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ~~ ( V2r3 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ( ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3) = ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3) ) <=> ( V0r1 = V1r2 ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__EQ__LMUL,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ( ~~ ( V2r3 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ( ap(ap(c_2Erat_2Erat__mul,V2r3),V0r1) = ap(ap(c_2Erat_2Erat__mul,V2r3),V1r2) ) <=> ( V0r1 = V1r2 ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__RADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,V0r1),V2r3)),ap(ap(c_2Erat_2Erat__add,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__LADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,V2r3),V0r1)),ap(ap(c_2Erat_2Erat__add,V2r3),V1r2))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__RADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,V0r1),V2r3)),ap(ap(c_2Erat_2Erat__add,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LEQ__LADD,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,V2r3),V0r1)),ap(ap(c_2Erat_2Erat__add,V2r3),V1r2))) <=> p(ap(ap(c_2Erat_2Erat__leq,V0r1),V1r2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__ADD__MONO,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2c] : ( mem(V2c,ty_2Erat_2Erat) => ! [V3d] : ( mem(V3d,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__leq,V0a),V1b)) & p(ap(ap(c_2Erat_2Erat__leq,V2c),V3d)) ) => p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,V0a),V2c)),ap(ap(c_2Erat_2Erat__add,V1b),V3d))) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__AINV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__ainv,V0r1)),ap(c_2Erat_2Erat__ainv,V1r2))) <=> p(ap(ap(c_2Erat_2Erat__les,V1r2),V0r1)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LSUB__LES,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2)),V2r3)) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(ap(c_2Erat_2Erat__add,V1r2),V2r3))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RSUB__LES,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(ap(c_2Erat_2Erat__sub,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__add,V0r1),V2r3)),V1r2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LSUB__LEQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2)),V2r3)) <=> p(ap(ap(c_2Erat_2Erat__leq,V0r1),ap(ap(c_2Erat_2Erat__add,V1r2),V2r3))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RSUB__LEQ,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),ap(ap(c_2Erat_2Erat__sub,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__add,V0r1),V2r3)),V1r2)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__RMUL__POS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V2r3)) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3)),ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__LMUL__POS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V2r3)) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V2r3),V0r1)),ap(ap(c_2Erat_2Erat__mul,V2r3),V1r2))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__RMUL__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V2r3),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3)),ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__LMUL__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V2r3),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V2r3),V1r2)),ap(ap(c_2Erat_2Erat__mul,V2r3),V0r1))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__AINV__LES,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__ainv,V0r1)),V1r2)) <=> p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__ainv,V1r2)),V0r1)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LDIV__LES__POS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V1r2)) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__div,V0r1),V1r2)),V2r3)) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3))) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LDIV__LES__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V1r2),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__div,V0r1),V1r2)),V2r3)) <=> p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3)),V0r1)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RDIV__LES__POS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V2r3)) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(ap(c_2Erat_2Erat__div,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3)),V1r2)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RDIV__LES__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V2r3),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(ap(c_2Erat_2Erat__div,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__les,V1r2),ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3))) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LDIV__LEQ__POS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V1r2)) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__div,V0r1),V1r2)),V2r3)) <=> p(ap(ap(c_2Erat_2Erat__leq,V0r1),ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3))) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LDIV__LEQ__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V1r2),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__div,V0r1),V1r2)),V2r3)) <=> p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__mul,V1r2),V2r3)),V0r1)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RDIV__LEQ__POS,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V2r3)) => ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),ap(ap(c_2Erat_2Erat__div,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__leq,ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3)),V1r2)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__RDIV__LEQ__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V2r3),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) => ( p(ap(ap(c_2Erat_2Erat__leq,V0r1),ap(ap(c_2Erat_2Erat__div,V1r2),V2r3))) <=> p(ap(ap(c_2Erat_2Erat__leq,V1r2),ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3))) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__SUB0,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2)),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r2)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__LES__0SUB,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),ap(ap(c_2Erat_2Erat__sub,V0r1),V1r2))) <=> p(ap(ap(c_2Erat_2Erat__les,V1r2),V0r1)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MINV__LES,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1)) => ( ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__minv,V0r1)),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) <=> p(ap(ap(c_2Erat_2Erat__les,V0r1),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) & ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),ap(c_2Erat_2Erat__minv,V0r1))) <=> p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0r1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MUL__SIGN__CASES,lemma,(! [V0p] : ( mem(V0p,ty_2Erat_2Erat) => ! [V1q] : ( mem(V1q,ty_2Erat_2Erat) => ( ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),ap(ap(c_2Erat_2Erat__mul,V0p),V1q))) <=> ( ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0p)) & p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V1q)) ) | ( p(ap(ap(c_2Erat_2Erat__les,V0p),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Erat_2Erat__les,V1q),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) ) ) & ( p(ap(ap(c_2Erat_2Erat__les,ap(ap(c_2Erat_2Erat__mul,V0p),V1q)),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) <=> ( ( p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V0p)) & p(ap(ap(c_2Erat_2Erat__les,V1q),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) ) | ( p(ap(ap(c_2Erat_2Erat__les,V0p),ap(c_2Erat_2Erat__of__num,c_2Enum_2E0))) & p(ap(ap(c_2Erat_2Erat__les,ap(c_2Erat_2Erat__of__num,c_2Enum_2E0)),V1q)) ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NO__ZERODIV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) | ( V1r2 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) <=> ( ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NO__ZERODIV__THM,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) <=> ( ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) | ( V1r2 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NO__ZERODIV__NEG,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ~~ ( ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) <=> ( ( ~~ ( V0r1 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1r2 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__NO__IDDIV,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ( ( ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2) = V1r2 ) <=> ( ( V0r1 = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) | ( V1r2 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERDIV__MUL__OUT,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,V0r1),ap(ap(c_2Erat_2Erat__div,V1r2),V2r3)) = ap(ap(c_2Erat_2Erat__div,ap(ap(c_2Erat_2Erat__mul,V0r1),V1r2)),V2r3) ) ) ) ))).
fof(conj_thm_2Erat_2ELDIV__MUL__OUT,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r2] : ( mem(V1r2,ty_2Erat_2Erat) => ! [V2r3] : ( mem(V2r3,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__div,V0r1),V1r2)),V2r3) = ap(ap(c_2Erat_2Erat__div,ap(ap(c_2Erat_2Erat__mul,V0r1),V2r3)),V1r2) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DENSE__THM,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ! [V1r3] : ( mem(V1r3,ty_2Erat_2Erat) => ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V1r3)) => ? [V2r2] : ( mem(V2r2,ty_2Erat_2Erat) & ( p(ap(ap(c_2Erat_2Erat__les,V0r1),V2r2)) & p(ap(ap(c_2Erat_2Erat__les,V2r2),V1r3)) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SAVE,lemma,(! [V0r1] : ( mem(V0r1,ty_2Erat_2Erat) => ? [V1a1] : ( mem(V1a1,ty_2Einteger_2Eint) & ? [V2b1] : ( mem(V2b1,ty_2Enum_2Enum) & ( V0r1 = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__save,V1a1),V2b1)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SAVE__MINV,lemma,(! [V0a1] : ( mem(V0a1,ty_2Einteger_2Eint) => ! [V1b1] : ( mem(V1b1,ty_2Enum_2Enum) => ( ( ~~ ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__save,V0a1),V1b1)) = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Erat_2Erat__minv,ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__save,V0a1),V1b1))) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__save,ap(ap(c_2Einteger_2Eint__mul,ap(c_2EintExtension_2ESGN,V0a1)),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,V1b1)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))))),ap(c_2Einteger_2ENum,ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2EABS,V0a1)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))))) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__SAVE__TO__CONS,lemma,(! [V0a1] : ( mem(V0a1,ty_2Einteger_2Eint) => ! [V1b1] : ( mem(V1b1,ty_2Enum_2Enum) => ( ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__save,V0a1),V1b1)) = ap(ap(c_2Erat_2Erat__cons,V0a1),ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,V1b1)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Erat_2ERAT__OF__NUM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,A_27a) => ( ( ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) = c_2Erat_2Erat__0 ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Erat_2Erat__of__num,ap(c_2Enum_2ESUC,V1n)) = ap(ap(c_2Erat_2Erat__add,ap(c_2Erat_2Erat__of__num,V1n)),c_2Erat_2Erat__1) ) ) ) )))).
fof(conj_thm_2Erat_2ERAT__SAVE__NUM,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Erat_2Erat__of__num,V0n) = ap(c_2Erat_2Eabs__rat,ap(ap(c_2Efrac_2Efrac__save,ap(c_2Einteger_2Eint__of__num,V0n)),c_2Enum_2E0)) ) ))).
fof(conj_thm_2Erat_2ERAT__CONS__TO__NUM,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Erat_2Erat__cons,ap(c_2Einteger_2Eint__of__num,V0n)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Erat_2Erat__of__num,V0n) ) & ( ap(ap(c_2Erat_2Erat__cons,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,V0n))),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__of__num,V0n)) ) ) ))).
fof(conj_thm_2Erat_2ERAT__0,lemma,(( c_2Erat_2Erat__0 = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Erat_2ERAT__1,lemma,(( c_2Erat_2Erat__1 = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Erat_2ERAT__MINV__1,lemma,(( ap(c_2Erat_2Erat__minv,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Erat_2ERAT__DIV__1,lemma,(! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__div,V0r),ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0r ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__NEG1,lemma,(! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ap(ap(c_2Erat_2Erat__div,V0r),ap(c_2Erat_2Erat__ainv,ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) = ap(c_2Erat_2Erat__ainv,V0r) ) ))).
fof(conj_thm_2Erat_2ERAT__DIV__INV,lemma,(! [V0r] : ( mem(V0r,ty_2Erat_2Erat) => ( ( ~~ ( V0r = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Erat_2Erat__div,V0r),V0r) = ap(c_2Erat_2Erat__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Erat_2ERAT__MINV__MUL,lemma,(! [V0a] : ( mem(V0a,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ( ( ( ~~ ( V0a = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1b = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) => ( ap(c_2Erat_2Erat__minv,ap(ap(c_2Erat_2Erat__mul,V0a),V1b)) = ap(ap(c_2Erat_2Erat__mul,ap(c_2Erat_2Erat__minv,V0a)),ap(c_2Erat_2Erat__minv,V1b)) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIVDIV__MUL,lemma,(! [V0b] : ( mem(V0b,ty_2Erat_2Erat) => ! [V1d] : ( mem(V1d,ty_2Erat_2Erat) => ! [V2a] : ( mem(V2a,ty_2Erat_2Erat) => ! [V3c] : ( mem(V3c,ty_2Erat_2Erat) => ( ( ( ~~ ( V0b = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1d = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) => ( ap(ap(c_2Erat_2Erat__mul,ap(ap(c_2Erat_2Erat__div,V2a),V0b)),ap(ap(c_2Erat_2Erat__div,V3c),V1d)) = ap(ap(c_2Erat_2Erat__div,ap(ap(c_2Erat_2Erat__mul,V2a),V3c)),ap(ap(c_2Erat_2Erat__mul,V0b),V1d)) ) ) ) ) ) ))).
fof(conj_thm_2Erat_2ERAT__DIVDIV__ADD,conjecture,(! [V0y] : ( mem(V0y,ty_2Erat_2Erat) => ! [V1b] : ( mem(V1b,ty_2Erat_2Erat) => ! [V2x] : ( mem(V2x,ty_2Erat_2Erat) => ! [V3a] : ( mem(V3a,ty_2Erat_2Erat) => ( ( ( ~~ ( V0y = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1b = ap(c_2Erat_2Erat__of__num,c_2Enum_2E0) ) ) ) => ( ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__div,V2x),V0y)),ap(ap(c_2Erat_2Erat__div,V3a),V1b)) = ap(ap(c_2Erat_2Erat__div,ap(ap(c_2Erat_2Erat__add,ap(ap(c_2Erat_2Erat__mul,V2x),V1b)),ap(ap(c_2Erat_2Erat__mul,V3a),V0y))),ap(ap(c_2Erat_2Erat__mul,V0y),V1b)) ) ) ) ) ) ))).
