include('Axioms/poset+2.ax').
fof(mem_c_2Earithmetic_2E_2A,axiom,( mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2E_2B,axiom,( mem(c_2Earithmetic_2E_2B,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2E_2D,axiom,( mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2E_3C_3D,axiom,( mem(c_2Earithmetic_2E_3C_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) )).
fof(mem_c_2Earithmetic_2E_3E,axiom,( mem(c_2Earithmetic_2E_3E,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) )).
fof(mem_c_2Earithmetic_2E_3E_3D,axiom,( mem(c_2Earithmetic_2E_3E_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) )).
fof(mem_c_2Earithmetic_2EABS__DIFF,axiom,( mem(c_2Earithmetic_2EABS__DIFF,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EBIT1,axiom,( mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2EBIT2,axiom,( mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2EDIV,axiom,( mem(c_2Earithmetic_2EDIV,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EDIV2,axiom,( mem(c_2Earithmetic_2EDIV2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2EDIVMOD,axiom,( mem(c_2Earithmetic_2EDIVMOD,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EEVEN,axiom,( mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool)) )).
fof(mem_c_2Earithmetic_2EEXP,axiom,( mem(c_2Earithmetic_2EEXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EFACT,axiom,( mem(c_2Earithmetic_2EFACT,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2EFUNPOW,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Earithmetic_2EFUNPOW(A_27a),arr(arr(A_27a,A_27a),arr(ty_2Enum_2Enum,arr(A_27a,A_27a)))) ) )).
fof(mem_c_2Earithmetic_2EMAX,axiom,( mem(c_2Earithmetic_2EMAX,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EMIN,axiom,( mem(c_2Earithmetic_2EMIN,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EMOD,axiom,( mem(c_2Earithmetic_2EMOD,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Earithmetic_2EMODEQ,axiom,( mem(c_2Earithmetic_2EMODEQ,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))) )).
fof(mem_c_2Earithmetic_2ENRC,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Earithmetic_2ENRC(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Enum_2Enum,arr(A_27a,arr(A_27a,bool))))) ) )).
fof(mem_c_2Earithmetic_2ENUMERAL,axiom,( mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2EODD,axiom,( mem(c_2Earithmetic_2EODD,arr(ty_2Enum_2Enum,bool)) )).
fof(mem_c_2Earithmetic_2EZERO,axiom,( mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum) )).
fof(mem_c_2Earithmetic_2Efindq,axiom,( mem(c_2Earithmetic_2Efindq,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2Enat__elim____magic,axiom,( mem(c_2Earithmetic_2Enat__elim____magic,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) )).
fof(mem_c_2Earithmetic_2Enum__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Earithmetic_2Enum__CASE(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,arr(arr(ty_2Enum_2Enum,A_27a),A_27a)))) ) )).
fof(ax_thm_2Earithmetic_2EADD,axiom, ( ( ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,c_2Enum_2E0),V0n) = V0n ) ) ) & ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,V1m)),V2n) = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V1m),V2n)) ) ) ) )).
fof(ax_thm_2Earithmetic_2ENUMERAL__DEF,axiom, ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ( ap(c_2Earithmetic_2ENUMERAL,V0x) = V0x ) )).
fof(ax_thm_2Earithmetic_2EALT__ZERO,axiom, ( c_2Earithmetic_2EZERO = c_2Enum_2E0 )).
fof(ax_thm_2Earithmetic_2EBIT1,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Earithmetic_2EBIT1,V0n) = ap(ap(c_2Earithmetic_2E_2B,V0n),ap(ap(c_2Earithmetic_2E_2B,V0n),ap(c_2Enum_2ESUC,c_2Enum_2E0))) ) )).
fof(ax_thm_2Earithmetic_2EBIT2,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Earithmetic_2EBIT2,V0n) = ap(ap(c_2Earithmetic_2E_2B,V0n),ap(ap(c_2Earithmetic_2E_2B,V0n),ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,c_2Enum_2E0)))) ) )).
fof(ax_thm_2Earithmetic_2Enat__elim____magic,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Earithmetic_2Enat__elim____magic,V0n) = V0n ) )).
fof(ax_thm_2Earithmetic_2ESUB,axiom, ( ( ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,c_2Enum_2E0),V0m) = c_2Enum_2E0 ) ) ) & ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V1m)),V2n) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,V1m),V2n)),c_2Enum_2E0),ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2D,V1m),V2n))) ) ) ) )).
fof(ax_thm_2Earithmetic_2EMULT,axiom, ( ( ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,c_2Enum_2E0),V0n) = c_2Enum_2E0 ) ) ) & ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V1m)),V2n) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,V1m),V2n)),V2n) ) ) ) )).
fof(ax_thm_2Earithmetic_2EEXP,axiom, ( ( ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EEXP,V0m),c_2Enum_2E0) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) & ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EEXP,V1m),ap(c_2Enum_2ESUC,V2n)) = ap(ap(c_2Earithmetic_2E_2A,V1m),ap(ap(c_2Earithmetic_2EEXP,V1m),V2n)) ) ) ) )).
fof(ax_thm_2Earithmetic_2EGREATER__DEF,axiom, ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E,V0m),V1n)) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) ) ) )).
fof(ax_thm_2Earithmetic_2ELESS__OR__EQ,axiom, ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) | ( V0m = V1n ) ) ) ) )).
fof(ax_thm_2Earithmetic_2EGREATER__OR__EQ,axiom, ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E_3D,V0m),V1n)) <=> ( p(ap(ap(c_2Earithmetic_2E_3E,V0m),V1n)) | ( V0m = V1n ) ) ) ) )).
fof(ax_thm_2Earithmetic_2EEVEN,axiom, ( ( p(ap(c_2Earithmetic_2EEVEN,c_2Enum_2E0)) <=> $true ) & ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,ap(c_2Enum_2ESUC,V0n))) <=> ( ~~ p(ap(c_2Earithmetic_2EEVEN,V0n)) ) ) ) )).
fof(ax_thm_2Earithmetic_2EODD,axiom, ( ( p(ap(c_2Earithmetic_2EODD,c_2Enum_2E0)) <=> $false ) & ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EODD,ap(c_2Enum_2ESUC,V0n))) <=> ( ~~ p(ap(c_2Earithmetic_2EODD,V0n)) ) ) ) )).
fof(ax_thm_2Earithmetic_2Enum__case__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0v] : ( mem(V0v,A_27a) => ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => ( ap(ap(ap(c_2Earithmetic_2Enum__CASE(A_27a),c_2Enum_2E0),V0v),V1f) = V0v ) ) ) ) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3v] : ( mem(V3v,A_27a) => ! [V4f] : ( mem(V4f,arr(ty_2Enum_2Enum,A_27a)) => ( ap(ap(ap(c_2Earithmetic_2Enum__CASE(A_27a),ap(c_2Enum_2ESUC,V2n)),V3v),V4f) = ap(V4f,V2n) ) ) ) ) ) ) )).
fof(ax_thm_2Earithmetic_2EFUNPOW,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( ap(ap(ap(c_2Earithmetic_2EFUNPOW(A_27a),V0f),c_2Enum_2E0),V1x) = V1x ) ) ) ) & ! [V2f] : ( mem(V2f,arr(A_27a,A_27a)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4x] : ( mem(V4x,A_27a) => ( ap(ap(ap(c_2Earithmetic_2EFUNPOW(A_27a),V2f),ap(c_2Enum_2ESUC,V3n)),V4x) = ap(ap(ap(c_2Earithmetic_2EFUNPOW(A_27a),V2f),V3n),ap(V2f,V4x)) ) ) ) ) ) ) )).
fof(ax_thm_2Earithmetic_2ENRC,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27a,bool))) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A_27a),V0R),c_2Enum_2E0),V1x),V2y)) <=> ( V1x = V2y ) ) ) ) ) ) & ! [V3R] : ( mem(V3R,arr(A_27a,arr(A_27a,bool))) => ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6y] : ( mem(V6y,A_27a) => ( p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A_27a),V3R),ap(c_2Enum_2ESUC,V4n)),V5x),V6y)) <=> ? [V7z] : ( mem(V7z,A_27a) & ( p(ap(ap(V3R,V5x),V7z)) & p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A_27a),V3R),V4n),V7z),V6y)) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Earithmetic_2EONE,lemma,(( ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,c_2Enum_2E0) ))).
fof(conj_thm_2Earithmetic_2ETWO,lemma,(( ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Earithmetic_2ENORM__0,lemma,(( ap(c_2Earithmetic_2ENUMERAL,c_2Earithmetic_2EZERO) = c_2Enum_2E0 ))).
fof(conj_thm_2Earithmetic_2Enum__case__compute,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,A_27a) => ! [V1g] : ( mem(V1g,arr(ty_2Enum_2Enum,A_27a)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(ap(c_2Earithmetic_2Enum__CASE(A_27a),V2n),V0f),V1g) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V2n),c_2Enum_2E0)),V0f),ap(V1g,ap(c_2Eprim__rec_2EPRE,V2n))) ) ) ) )))).
fof(conj_thm_2Earithmetic_2ESUC__NOT,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ~~ ( c_2Enum_2E0 = ap(c_2Enum_2ESUC,V0n) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,V0m),c_2Enum_2E0) = V0m ) ))).
fof(conj_thm_2Earithmetic_2EADD__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) = ap(ap(c_2Earithmetic_2E_2B,V0m),ap(c_2Enum_2ESUC,V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__CLAUSES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,c_2Enum_2E0),V0m) = V0m ) & ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),c_2Enum_2E0) = V0m ) & ( ( ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,V0m)),V1n) = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) ) & ( ap(ap(c_2Earithmetic_2E_2B,V0m),ap(c_2Enum_2ESUC,V1n)) = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__SYM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = ap(ap(c_2Earithmetic_2E_2B,V1n),V0m) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__COMM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = ap(ap(c_2Earithmetic_2E_2B,V1n),V0m) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__ASSOC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,V0m),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p)) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)),V2p) ) ) ) ))).
fof(conj_thm_2Earithmetic_2Enum__CASES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ( V0m = c_2Enum_2E0 ) | ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( V0m = ap(c_2Enum_2ESUC,V1n) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__ZERO__LT__ZERO,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ( ~~ ( V0n = c_2Enum_2E0 ) ) <=> p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__LT__ZERO__EQ__ZERO,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) ) <=> ( V0n = c_2Enum_2E0 ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__OR__EQ__ALT,lemma,(( c_2Earithmetic_2E_3C_3D = ap(c_2Erelation_2ERTC(ty_2Enum_2Enum),f159) ))).
fof(conj_thm_2Earithmetic_2ELESS__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) => ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( ap(ap(c_2Earithmetic_2E_2B,V2p),V1n) = V0m ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2Etransitive__LESS,lemma,(p(ap(c_2Erelation_2Etransitive(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C)))).
fof(conj_thm_2Earithmetic_2ELESS__TRANS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V2p)) ) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__ANTISYM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ~~ ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__REV,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,V0m)),ap(c_2Enum_2ESUC,V1n))) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,V0m)),ap(c_2Enum_2ESUC,V1n))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__MONO,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0n)),ap(c_2Enum_2ESUC,V1m))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),V1m)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__LESS__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ~~ ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & p(ap(ap(c_2Eprim__rec_2E_3C,V1n),ap(c_2Enum_2ESUC,V0m))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2Etransitive__measure,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => p(ap(c_2Erelation_2Etransitive(A_27a),ap(c_2Eprim__rec_2Emeasure(A_27a),V0f))) )))).
fof(conj_thm_2Earithmetic_2ELESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0m)),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__OR,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0m)),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EOR__LESS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0m)),V1n)) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__IFF__LESS__SUC,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),V1m)) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Enum_2ESUC,V1m))) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__IMP__LESS__SUC,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),V1m)) => p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Enum_2ESUC,V1m))) ) ) ))).
fof(conj_thm_2Earithmetic_2EZERO__LESS__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(ap(c_2Earithmetic_2E_3C_3D,c_2Enum_2E0),V0n)) ))).
fof(conj_thm_2Earithmetic_2ELESS__SUC__EQ__COR,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & ( ~~ ( ap(c_2Enum_2ESUC,V0m) = V1n ) ) ) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,V0m)),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__NOT__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & ( ~~ ( V1n = ap(c_2Enum_2ESUC,V0m) ) ) ) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,V0m)),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__0__CASES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ( c_2Enum_2E0 = V0m ) | p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__CASES__IMP,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ( ~~ p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) & ( ~~ ( V0m = V1n ) ) ) => p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__CASES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__INV__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = V0m ) => ( V1n = c_2Enum_2E0 ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(ap(c_2Earithmetic_2E_2B,V0m),V1n))) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__ADD__EXISTS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) => ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( ap(ap(c_2Earithmetic_2E_2B,V2p),V1n) = V0m ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__STRONG__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) => ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,V2p)),V1n) = V0m ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__SUC__REFL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(c_2Enum_2ESUC,V0m))) ))).
fof(conj_thm_2Earithmetic_2ELESS__ADD__NONZERO,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ ( V1n = c_2Enum_2E0 ) ) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2B,V0m),V1n))) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__SUC__LESS__EQ__0,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0n)),c_2Enum_2E0)) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__LESS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__LESS__EQUAL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) ) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__ANTISYM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ~~ ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__0,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),c_2Enum_2E0)) <=> ( V0n = c_2Enum_2E0 ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2D,c_2Enum_2E0),V0m) = c_2Enum_2E0 ) & ( ap(ap(c_2Earithmetic_2E_2D,V0m),c_2Enum_2E0) = V0m ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__MONO__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0n)),ap(c_2Enum_2ESUC,V1m)) = ap(ap(c_2Earithmetic_2E_2D,V0n),V1m) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__EQ__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2D,V0m),V1n) = c_2Enum_2E0 ) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(c_2Enum_2ESUC,V0m) = ap(ap(c_2Earithmetic_2E_2B,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Earithmetic_2ESUC__SUB1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = V0m ) ))).
fof(conj_thm_2Earithmetic_2EPRE__SUB1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(c_2Eprim__rec_2EPRE,V0m) = ap(ap(c_2Earithmetic_2E_2D,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V0m),c_2Enum_2E0) = c_2Enum_2E0 ) ))).
fof(conj_thm_2Earithmetic_2EMULT__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V0m),ap(c_2Enum_2ESUC,V1n)) = ap(ap(c_2Earithmetic_2E_2B,V0m),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__LEFT__1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V0m) = V0m ) ))).
fof(conj_thm_2Earithmetic_2EMULT__RIGHT__1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = V0m ) ))).
fof(conj_thm_2Earithmetic_2EMULT__CLAUSES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,c_2Enum_2E0),V0m) = c_2Enum_2E0 ) & ( ( ap(ap(c_2Earithmetic_2E_2A,V0m),c_2Enum_2E0) = c_2Enum_2E0 ) & ( ( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V0m) = V0m ) & ( ( ap(ap(c_2Earithmetic_2E_2A,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = V0m ) & ( ( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V0m)),V1n) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),V1n) ) & ( ap(ap(c_2Earithmetic_2E_2A,V0m),ap(c_2Enum_2ESUC,V1n)) = ap(ap(c_2Earithmetic_2E_2B,V0m),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)) ) ) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__SYM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V0m),V1n) = ap(ap(c_2Earithmetic_2E_2A,V1n),V0m) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__COMM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V0m),V1n) = ap(ap(c_2Earithmetic_2E_2A,V1n),V0m) ) ) ))).
fof(conj_thm_2Earithmetic_2ERIGHT__ADD__DISTRIB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)),V2p) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2A,V1n),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELEFT__ADD__DISTRIB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V2p),ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,V2p),V0m)),ap(ap(c_2Earithmetic_2E_2A,V2p),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__ASSOC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V0m),ap(ap(c_2Earithmetic_2E_2A,V1n),V2p)) = ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),V2p) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) => ( ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V1n) = V0m ) ) ) ))).
fof(conj_thm_2Earithmetic_2EPRE__SUB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Eprim__rec_2EPRE,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Eprim__rec_2EPRE,V0m)),V1n) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__EQ__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = c_2Enum_2E0 ) <=> ( ( V0m = c_2Enum_2E0 ) & ( V1n = c_2Enum_2E0 ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__EQ__1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) <=> ( ( ( V0m = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) & ( V1n = c_2Enum_2E0 ) ) | ( ( V0m = c_2Enum_2E0 ) & ( V1n = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__INV__0__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = V0m ) <=> ( V1n = c_2Enum_2E0 ) ) ) ))).
fof(conj_thm_2Earithmetic_2EPRE__SUC__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) => ( ( V0m = ap(c_2Eprim__rec_2EPRE,V1n) ) <=> ( ap(c_2Enum_2ESUC,V0m) = V1n ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EINV__PRE__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) => ( ( ap(c_2Eprim__rec_2EPRE,V0m) = ap(c_2Eprim__rec_2EPRE,V1n) ) <=> ( V0m = V1n ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__SUC__NOT,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) => ( ~~ p(ap(ap(c_2Eprim__rec_2E_3C,V1n),ap(c_2Enum_2ESUC,V0m))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__EQ__SUB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = V2p ) <=> ( V0m = ap(ap(c_2Earithmetic_2E_2D,V2p),V1n) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__ADD__INV,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__ADD__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELT__ADD__RCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELT__ADD__LCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V2p),V0m)),ap(ap(c_2Earithmetic_2E_2B,V2p),V1n))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEQ__MONO__ADD__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V2p) = ap(ap(c_2Earithmetic_2E_2B,V1n),V2p) ) <=> ( V0m = V1n ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__MONO__ADD__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__TRANS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__LESS__TRANS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) & p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V2p)) ) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__LESS__EQ__TRANS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__LESS__EQ__MONO,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ! [V3q] : ( mem(V3q,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V2p)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V3q)) ) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2B,V2p),V3q))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__REFL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V0m)) ))).
fof(conj_thm_2Earithmetic_2ELESS__IMP__LESS__OR__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__MULT,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2A,V1n),V2p))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MONO__MULT2,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3j] : ( mem(V3j,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V2i)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V3j)) ) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2A,V2i),V3j))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ERIGHT__SUB__DISTRIB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2A,V0m),V2p)),ap(ap(c_2Earithmetic_2E_2A,V1n),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELEFT__SUB__DISTRIB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,V2p),ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2A,V2p),V0m)),ap(ap(c_2Earithmetic_2E_2A,V2p),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__ADD__1,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) => ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( V0m = ap(ap(c_2Earithmetic_2E_2B,V1n),ap(ap(c_2Earithmetic_2E_2B,V2p),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEXP__ADD,lemma,(! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1q] : ( mem(V1q,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EEXP,V2n),ap(ap(c_2Earithmetic_2E_2B,V0p),V1q)) = ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EEXP,V2n),V0p)),ap(ap(c_2Earithmetic_2EEXP,V2n),V1q)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__ODD__EQ__EVEN,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ~~ ( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0n),V0n)) = ap(ap(c_2Earithmetic_2E_2B,V1m),V1m) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQUAL__ANTISYM,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),V1m)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V0n)) ) => ( V0n = V1m ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__ADD__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2B,V0m),ap(c_2Enum_2ESUC,V1n)))) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__OR__EQ__ADD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0n),V1m)) | ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( V0n = ap(ap(c_2Earithmetic_2E_2B,V2p),V1m) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EWOP,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ( ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & p(ap(V0P,V1n)) ) ) => ? [V2n] : ( mem(V2n,ty_2Enum_2Enum) & ( p(ap(V0P,V2n)) & ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3m),V2n)) => ( ~~ p(ap(V0P,V3m)) ) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ECOMPLETE__INDUCTION,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2m),V1n)) => p(ap(V0P,V2m)) ) ) ) => p(ap(V0P,V1n)) ) ) ) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => p(ap(V0P,V3n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EFORALL__NUM__THM,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(V0P,V1n)) ) ) <=> ( p(ap(V0P,c_2Enum_2E0)) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(V0P,V2n)) => p(ap(V0P,ap(c_2Enum_2ESUC,V2n))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUC__SUB,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0a)),V0a) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__PLUS,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ! [V2c] : ( mem(V2c,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,V0a),ap(ap(c_2Earithmetic_2E_2B,V1b),V2c)) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,V0a),V1b)),V2c) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EINV__PRE__LESS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Eprim__rec_2EPRE,V0m)),ap(c_2Eprim__rec_2EPRE,V1n))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EINV__PRE__LESS__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Eprim__rec_2EPRE,V1m)),ap(c_2Eprim__rec_2EPRE,V0n))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V0n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EPRE__LESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Eprim__rec_2EPRE,V0m)),ap(c_2Eprim__rec_2EPRE,V1n))) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LESS__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,V0n),V1m)),V0n)) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__EQ__EQ__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2D,V0m),V1n) = V0m ) <=> ( ( V0m = c_2Enum_2E0 ) | ( V1n = c_2Enum_2E0 ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LESS__0,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1m),V0n)) <=> p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(ap(c_2Earithmetic_2E_2D,V0n),V1m))) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LESS__OR,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),ap(ap(c_2Earithmetic_2E_2D,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__SUB__ADD__LESS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2i),ap(ap(c_2Earithmetic_2E_2D,V0n),V1m))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V2i),V1m)),V0n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ETIMES2,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V0n) = ap(ap(c_2Earithmetic_2E_2B,V0n),V0n) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MULT__MONO,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V2n)),V0m)),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V2n)),V1i))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1i)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__MONO__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V2n)),V0m) = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V2n)),V1i) ) <=> ( V0m = V1i ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__SUC__EQ,lemma,(! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V2n),ap(c_2Enum_2ESUC,V0p)) = ap(ap(c_2Earithmetic_2E_2A,V1m),ap(c_2Enum_2ESUC,V0p)) ) <=> ( V2n = V1m ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__EXP__MONO,lemma,(! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1q] : ( mem(V1q,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V2n),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,V1q)),V0p)) = ap(ap(c_2Earithmetic_2E_2A,V3m),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,V1q)),V0p)) ) <=> ( V2n = V3m ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEQ__ADD__LCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = ap(ap(c_2Earithmetic_2E_2B,V0m),V2p) ) <=> ( V1n = V2p ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEQ__ADD__RCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V2p) = ap(ap(c_2Earithmetic_2E_2B,V1n),V2p) ) <=> ( V0m = V1n ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEQ__MULT__LCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V0m),V1n) = ap(ap(c_2Earithmetic_2E_2A,V0m),V2p) ) <=> ( ( V0m = c_2Enum_2E0 ) | ( V1n = V2p ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEQ__MULT__RCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V1n),V0m) = ap(ap(c_2Earithmetic_2E_2A,V2p),V0m) ) <=> ( ( V0m = c_2Enum_2E0 ) | ( V1n = V2p ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__SUB,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1c] : ( mem(V1c,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V0a),V1c)),V1c) = V0a ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__ADD__SUB,lemma,(! [V0c] : ( mem(V0c,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0c),V1b)) => ! [V2a] : ( mem(V2a,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V2a),V1b)),V0c) = ap(ap(c_2Earithmetic_2E_2B,V2a),ap(ap(c_2Earithmetic_2E_2D,V1b),V0c)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__EQUAL__0,lemma,(! [V0c] : ( mem(V0c,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,V0c),V0c) = c_2Enum_2E0 ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__SUB__LESS,lemma,(! [V0a] : ( mem(V0a,ty_2Enum_2Enum) => ! [V1b] : ( mem(V1b,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1b),V0a)) => ! [V2c] : ( mem(V2c,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2D,V0a),V1b)),V2c)) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0a),ap(ap(c_2Earithmetic_2E_2B,V1b),V2c))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__SUC__LESS__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0n)),V1m)) ) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V0n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__SUB,lemma,(! [V0b] : ( mem(V0b,ty_2Enum_2Enum) => ! [V1c] : ( mem(V1c,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1c),V0b)) => ! [V2a] : ( mem(V2a,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,V2a),ap(ap(c_2Earithmetic_2E_2D,V0b),V1c)) = ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V2a),V1c)),V0b) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__IMP__LESS__ADD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0n),V1m)) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(ap(c_2Earithmetic_2E_2B,V1m),V2p))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LESS__EQ__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1p)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,V1p),V0m)),V2n)) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1p),ap(ap(c_2Earithmetic_2E_2B,V0m),V2n))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LESS__SUC,lemma,(! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2D,V0p),V1m)),ap(c_2Enum_2ESUC,V0p))) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__CANCEL,lemma,(! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0p)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V2m),V0p)) ) => ( ( ap(ap(c_2Earithmetic_2E_2D,V0p),V1n) = ap(ap(c_2Earithmetic_2E_2D,V0p),V2m) ) <=> ( V1n = V2m ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ECANCEL__SUB,lemma,(! [V0p] : ( mem(V0p,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0p),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V0p),V2m)) ) => ( ( ap(ap(c_2Earithmetic_2E_2D,V1n),V0p) = ap(ap(c_2Earithmetic_2E_2D,V2m),V0p) ) <=> ( V1n = V2m ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__EXP__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ~~ ( ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,V1n)),V0m) = c_2Enum_2E0 ) ) ) ))).
fof(conj_thm_2Earithmetic_2EZERO__LESS__EXP,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,V1n)),V0m))) ) ))).
fof(conj_thm_2Earithmetic_2EODD__OR__EVEN,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ? [V1m] : ( mem(V1m,ty_2Enum_2Enum) & ( ( V0n = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,c_2Enum_2E0))),V1m) ) | ( V0n = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,c_2Enum_2E0))),V1m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EXP__SUC__MONO,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,V1m))),V0n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,V1m))),ap(c_2Enum_2ESUC,V0n)))) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__LESS__CASES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( V0m = V1n ) | ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V1n)) | p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V0m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EGREATER__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E_3D,V0n),V1m)) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V0n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__CASES,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQUAL__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) => ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( V1n = ap(ap(c_2Earithmetic_2E_2B,V0m),V2p) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__EQ__EXISTS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) <=> ? [V2p] : ( mem(V2p,ty_2Enum_2Enum) & ( V1n = ap(ap(c_2Earithmetic_2E_2B,V0m),V2p) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__EQ__0,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V0m),V1n) = c_2Enum_2E0 ) <=> ( ( V0m = c_2Enum_2E0 ) | ( V1n = c_2Enum_2E0 ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__EQ__1,lemma,(! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1y] : ( mem(V1y,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V0x),V1y) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) <=> ( ( V0x = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) & ( V1y = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__EQ__ID,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2A,V0m),V1n) = V1n ) <=> ( ( V0m = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) | ( V1n = c_2Enum_2E0 ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELESS__MULT2,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n))) ) ) ))).
fof(conj_thm_2Earithmetic_2EZERO__LESS__MULT,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EZERO__LESS__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(ap(c_2Earithmetic_2E_2B,V0m),V1n))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) | p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) ) ) ))).
fof(ax_thm_2Earithmetic_2EFACT,axiom, ( ( ap(c_2Earithmetic_2EFACT,c_2Enum_2E0) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) ) & ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Earithmetic_2EFACT,ap(c_2Enum_2ESUC,V0n)) = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V0n)),ap(c_2Earithmetic_2EFACT,V0n)) ) ) )).
fof(conj_thm_2Earithmetic_2EFACT__LESS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2EFACT,V0n))) ))).
fof(conj_thm_2Earithmetic_2EEVEN__ODD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,V0n)) <=> ( ~~ p(ap(c_2Earithmetic_2EODD,V0n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EODD__EVEN,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EODD,V0n)) <=> ( ~~ p(ap(c_2Earithmetic_2EEVEN,V0n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__OR__ODD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,V0n)) | p(ap(c_2Earithmetic_2EODD,V0n)) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__AND__ODD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ~~ ( p(ap(c_2Earithmetic_2EEVEN,V0n)) & p(ap(c_2Earithmetic_2EODD,V0n)) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n))) <=> ( p(ap(c_2Earithmetic_2EEVEN,V0m)) <=> p(ap(c_2Earithmetic_2EEVEN,V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__MULT,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n))) <=> ( p(ap(c_2Earithmetic_2EEVEN,V0m)) | p(ap(c_2Earithmetic_2EEVEN,V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EODD__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n))) <=> ( ~~ ( p(ap(c_2Earithmetic_2EODD,V0m)) <=> p(ap(c_2Earithmetic_2EODD,V1n)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EODD__MULT,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n))) <=> ( p(ap(c_2Earithmetic_2EODD,V0m)) & p(ap(c_2Earithmetic_2EODD,V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__DOUBLE,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V0n))) ))).
fof(conj_thm_2Earithmetic_2EODD__DOUBLE,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(c_2Earithmetic_2EODD,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V0n)))) ))).
fof(conj_thm_2Earithmetic_2EEVEN__ODD__EXISTS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ( p(ap(c_2Earithmetic_2EEVEN,V0n)) => ? [V1m] : ( mem(V1m,ty_2Enum_2Enum) & ( V0n = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V1m) ) ) ) & ( p(ap(c_2Earithmetic_2EODD,V0n)) => ? [V2m] : ( mem(V2m,ty_2Enum_2Enum) & ( V0n = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V2m)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__EXISTS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,V0n)) <=> ? [V1m] : ( mem(V1m,ty_2Enum_2Enum) & ( V0n = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V1m) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EODD__EXISTS,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EODD,V0n)) <=> ? [V1m] : ( mem(V1m,ty_2Enum_2Enum) & ( V0n = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),V1m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__EXP__IFF,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2EEXP,V1m),V0n))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) & p(ap(c_2Earithmetic_2EEVEN,V1m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EEVEN__EXP,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) & p(ap(c_2Earithmetic_2EEVEN,V0m)) ) => p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2EEXP,V0m),V1n))) ) ) ))).
fof(conj_thm_2Earithmetic_2EODD__EXP__IFF,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2EEXP,V1m),V0n))) <=> ( ( V0n = c_2Enum_2E0 ) | p(ap(c_2Earithmetic_2EODD,V1m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EODD__EXP,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) & p(ap(c_2Earithmetic_2EODD,V0m)) ) => p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2EEXP,V0m),V1n))) ) ) ))).
fof(conj_thm_2Earithmetic_2EEQ__LESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( V0m = V1n ) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V0m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EADD__MONO__LESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2B,V0m),V2p))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE__ADD__LCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2B,V0m),V2p))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE__ADD__RCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V1n),V0m)),ap(ap(c_2Earithmetic_2E_2B,V2p),V0m))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__LEQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) ) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V1n)),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__NUM__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ ( V0m = V1n ) ) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0m)),V1n)) | p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V1n)),V0m)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__GREATER,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Earithmetic_2E_3E,V0m),V1n)) ) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__GREATER__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ p(ap(ap(c_2Earithmetic_2E_3E_3D,V0m),V1n)) ) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,V0m)),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUC__ONE__ADD,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Enum_2ESUC,V0n) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V0n) ) ))).
fof(conj_thm_2Earithmetic_2ESUC__ADD__SYM,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,V1n)),V0m) ) ) ))).
fof(conj_thm_2Earithmetic_2ENOT__SUC__ADD__LESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n))),V0m)) ) ) ))).
fof(conj_thm_2Earithmetic_2EMULT__LESS__EQ__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V2p)),V0m)),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,V2p)),V1n))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE__MULT__LCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2A,V0m),V2p))) <=> ( ( V0m = c_2Enum_2E0 ) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE__MULT__RCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2A,V2p),V1n))) <=> ( ( V1n = c_2Enum_2E0 ) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V2p)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELT__MULT__LCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2A,V0m),V2p))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & p(ap(ap(c_2Eprim__rec_2E_3C,V1n),V2p)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELT__MULT__RCANCEL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),ap(ap(c_2Earithmetic_2E_2A,V2p),V1n))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) & p(ap(ap(c_2Eprim__rec_2E_3C,V0m),V2p)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELT__MULT__CANCEL__LBARE,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V1n)) ) ) & ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2A,V1n),V0m))) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),V1n)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELT__MULT__CANCEL__RBARE,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),V0m)) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0m)) & ( V1n = c_2Enum_2E0 ) ) ) & ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),V1n)) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) & ( V0m = c_2Enum_2E0 ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE__MULT__CANCEL__LBARE,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(ap(c_2Earithmetic_2E_2A,V0m),V1n))) <=> ( ( V0m = c_2Enum_2E0 ) | p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) ) & ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(ap(c_2Earithmetic_2E_2A,V1n),V0m))) <=> ( ( V0m = c_2Enum_2E0 ) | p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE__MULT__CANCEL__RBARE,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),V0m)) <=> ( ( V0m = c_2Enum_2E0 ) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) & ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)),V1n)) <=> ( ( V1n = c_2Enum_2E0 ) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,V0m),ap(ap(c_2Earithmetic_2E_2D,V1n),V2p)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)),V0m),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)),V2p),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__SUB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,V0m),ap(ap(c_2Earithmetic_2E_2D,V1n),V2p)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)),V0m),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__SUB,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p) = ap(ap(c_2Earithmetic_2E_2D,V0m),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__SUC,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)),ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,V0m)),V1n)) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__LESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(ap(c_2Earithmetic_2E_2D,V1n),V2p))) <=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),V1n)) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),c_2Enum_2E0)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__LESS__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p)) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__LESS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2D,V1n),V2p))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__LESS,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p)) <=> ( p(ap(ap(c_2Eprim__rec_2E_3C,V0m),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) & p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V2p)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__GREATER__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E_3D,V0m),ap(ap(c_2Earithmetic_2E_2D,V1n),V2p))) <=> p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),V1n)) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__GREATER__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p)) <=> ( p(ap(ap(c_2Earithmetic_2E_3E_3D,V0m),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) | p(ap(ap(c_2Earithmetic_2E_3E_3D,c_2Enum_2E0),V2p)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__GREATER,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E,V0m),ap(ap(c_2Earithmetic_2E_2D,V1n),V2p))) <=> ( p(ap(ap(c_2Earithmetic_2E_3E,ap(ap(c_2Earithmetic_2E_2B,V0m),V2p)),V1n)) & p(ap(ap(c_2Earithmetic_2E_3E,V0m),c_2Enum_2E0)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__GREATER,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3E,ap(ap(c_2Earithmetic_2E_2D,V0m),V1n)),V2p)) <=> p(ap(ap(c_2Earithmetic_2E_3E,V0m),ap(ap(c_2Earithmetic_2E_2B,V1n),V2p))) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__LEFT__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( V0m = ap(ap(c_2Earithmetic_2E_2D,V1n),V2p) ) <=> ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V2p) = V1n ) | ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),c_2Enum_2E0)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2p)) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ESUB__RIGHT__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Enum_2Enum) => ( ( ap(ap(c_2Earithmetic_2E_2D,V0m),V1n) = V2p ) <=> ( ( V0m = ap(ap(c_2Earithmetic_2E_2B,V1n),V2p) ) | ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V2p),c_2Enum_2E0)) ) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2ELE,lemma,(( ( ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),c_2Enum_2E0)) <=> ( V0n = c_2Enum_2E0 ) ) ) ) & ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),ap(c_2Enum_2ESUC,V2n))) <=> ( ( V1m = ap(c_2Enum_2ESUC,V2n) ) | p(ap(ap(c_2Earithmetic_2E_3C_3D,V1m),V2n)) ) ) ) ) ))).
fof(conj_thm_2Earithmetic_2EDA,lemma,(! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V1n)) => ? [V2r] : ( mem(V2r,ty_2Enum_2Enum) & ? [V3q] : ( mem(V3q,ty_2Enum_2Enum) & ( ( V0k = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,V3q),V1n)),V2r) ) & p(ap(ap(c_2Eprim__rec_2E_3C,V2r),V1n)) ) ) ) ) ) ))).
fof(ax_thm_2Earithmetic_2EDIVISION,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ( ( V1k = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EDIV,V1k),V0n)),V0n)),ap(ap(c_2Earithmetic_2EMOD,V1k),V0n)) ) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EMOD,V1k),V0n)),V0n)) ) ) ) )).
fof(ax_thm_2Earithmetic_2EDIV2__def,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Earithmetic_2EDIV2,V0n) = ap(ap(c_2Earithmetic_2EDIV,V0n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) ) )).
fof(conj_thm_2Earithmetic_2EMOD__ONE,lemma,(! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EMOD,V0k),ap(c_2Enum_2ESUC,c_2Enum_2E0)) = c_2Enum_2E0 ) ))).
fof(conj_thm_2Earithmetic_2EMOD__1,conjecture,(! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ( ap(ap(c_2Earithmetic_2EMOD,V0k),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = c_2Enum_2E0 ) ))).
