include('Axioms/integer+2.ax').
fof(ne_ty_2Eordinal_2Eordinal,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Eordinal_2Eordinal(A0)) ) )).
fof(mem_c_2Eordinal_2EallOrds,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EallOrds(A_27a),ty_2Ewellorder_2Ewellorder(ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(mem_c_2Eordinal_2Edclose,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Edclose(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),arr(ty_2Eordinal_2Eordinal(A_27a),bool))) ) )).
fof(mem_c_2Eordinal_2Edownward__closed,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Edownward__closed(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),bool)) ) )).
fof(mem_c_2Eordinal_2Eepsilon0,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eepsilon0(A_27a),ty_2Eordinal_2Eordinal(A_27a)) ) )).
fof(mem_c_2Eordinal_2Eeval__poly,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eeval__poly(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))),ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2EfromNat,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EfromNat(A_27a),arr(ty_2Enum_2Enum,ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(mem_c_2Eordinal_2Eis__polyform,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eordinal_2Eis__polyform(A_27a,A_27b),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27b))),bool))) ) ) )).
fof(mem_c_2Eordinal_2Eoleast,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eoleast(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(mem_c_2Eordinal_2Eomax,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eomax(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),ty_2Eoption_2Eoption(ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2Eomega,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eomega(A_27a),ty_2Eordinal_2Eordinal(A_27a)) ) )).
fof(mem_c_2Eordinal_2EordADD,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EordADD(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2EordDIV,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EordDIV(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2EordEXP,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EordEXP(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2EordMOD,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EordMOD(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2EordMULT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EordMULT(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))) ) )).
fof(mem_c_2Eordinal_2EordSUC,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2EordSUC(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(mem_c_2Eordinal_2Eordinal__ABS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eordinal__ABS(A_27a),arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(mem_c_2Eordinal_2Eordinal__ABS__CLASS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eordinal__ABS__CLASS(A_27a),arr(arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool),ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(mem_c_2Eordinal_2Eordinal__REP,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eordinal__REP(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) ) )).
fof(mem_c_2Eordinal_2Eordinal__REP__CLASS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eordinal__REP__CLASS(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool))) ) )).
fof(mem_c_2Eordinal_2Eordlt,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Eordlt(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),bool))) ) )).
fof(mem_c_2Eordinal_2Epolyform,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Epolyform(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))))) ) )).
fof(mem_c_2Eordinal_2Epreds,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Epreds(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),bool))) ) )).
fof(mem_c_2Eordinal_2Esup,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eordinal_2Esup(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),ty_2Eordinal_2Eordinal(A_27a))) ) )).
fof(ax_thm_2Eordinal_2Eordinal__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool),ty_2Eordinal_2Eordinal(A_27a)),f2142(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Eordinal_2Eordinal__bijections,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Eordinal__ABS__CLASS(A_27a),ap(c_2Eordinal_2Eordinal__REP__CLASS(A_27a),V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool)) => ( p(ap(f2144(A_27a),V1r)) <=> ( ap(c_2Eordinal_2Eordinal__REP__CLASS(A_27a),ap(c_2Eordinal_2Eordinal__ABS__CLASS(A_27a),V1r)) = V1r ) ) ) ) ) )).
fof(conj_thm_2Eordinal_2Eordinal__ABS__REP__CLASS,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Eordinal__ABS__CLASS(A_27a),ap(c_2Eordinal_2Eordinal__REP__CLASS(A_27a),V0a)) = V0a ) ) ) & ! [V1c] : ( mem(V1c,arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool)) => ( ( ? [V2r] : ( mem(V2r,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))) & ( p(ap(ap(c_2Ewellorder_2Eorderiso(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V2r),V2r)) & ( V1c = ap(c_2Ewellorder_2Eorderiso(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V2r) ) ) ) ) <=> ( ap(c_2Eordinal_2Eordinal__REP__CLASS(A_27a),ap(c_2Eordinal_2Eordinal__ABS__CLASS(A_27a),V1c)) = V1c ) ) ) )))).
fof(ax_thm_2Eordinal_2Eordinal__REP__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Eordinal__REP(A_27a),V0a) = ap(c_2Emin_2E_40(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))),ap(c_2Eordinal_2Eordinal__REP__CLASS(A_27a),V0a)) ) ) ) )).
fof(ax_thm_2Eordinal_2Eordinal__ABS__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))) => ( ap(c_2Eordinal_2Eordinal__ABS(A_27a),V0r) = ap(c_2Eordinal_2Eordinal__ABS__CLASS(A_27a),ap(c_2Ewellorder_2Eorderiso(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0r)) ) ) ) )).
fof(conj_thm_2Eordinal_2Eordinal__QUOTIENT,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(ap(c_2Equotient_2EQUOTIENT(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ty_2Eordinal_2Eordinal(A_27a)),c_2Ewellorder_2Eorderiso(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))),c_2Eordinal_2Eordinal__ABS(A_27a)),c_2Eordinal_2Eordinal__REP(A_27a)))))).
fof(ax_thm_2Eordinal_2Eordlt__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0T1] : ( mem(V0T1,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1T2] : ( mem(V1T2,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0T1),V1T2)) <=> p(ap(ap(c_2Ewellorder_2Eorderlt(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ap(c_2Eordinal_2Eordinal__REP(A_27a),V0T1)),ap(c_2Eordinal_2Eordinal__REP(A_27a),V1T2))) ) ) ) ) )).
fof(conj_thm_2Eordinal_2Eordlt__REFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0w),V0w)) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w1] : ( mem(V0w1,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2w3] : ( mem(V2w3,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0w1),V1w2)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1w2),V2w3)) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0w1),V2w3)) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__WF,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Erelation_2EWF(ty_2Eordinal_2Eordinal(A_27a)),c_2Eordinal_2Eordlt(A_27a)))))).
fof(conj_thm_2Eordinal_2Eordlt__trichotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w2] : ( mem(V0w2,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1w1] : ( mem(V1w1,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1w1),V0w2)) | ( ( V1w1 = V0w2 ) | p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0w2),V1w1)) ) ) ) )))).
fof(ax_thm_2Eordinal_2EallOrds__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Eordinal_2EallOrds(A_27a) = ap(c_2Ewellorder_2Ewellorder__ABS(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))),ap(c_2Epair_2EUNCURRY(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a),ty_2Epair_2Eprod(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),bool)),f2146(A_27a)))) ) ) )).
fof(conj_thm_2Eordinal_2Ewellorder__allOrds,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Ewellorder_2Ewellorder(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))),ap(c_2Epair_2EUNCURRY(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a),ty_2Epair_2Eprod(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),bool)),f2146(A_27a)))))))).
fof(conj_thm_2Eordinal_2EWIN__allOrds,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))),ap(ap(c_2Epair_2E_2C(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0x),V1y)),ap(c_2Eset__relation_2Estrict(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Ewellorder_2Ewellorder__REP(ty_2Eordinal_2Eordinal(A_27a)),c_2Eordinal_2EallOrds(A_27a))))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),V1y)) ) ) )))).
fof(conj_thm_2Eordinal_2EelsOf__allOrds,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ewellorder_2EelsOf(ty_2Eordinal_2Eordinal(A_27a)),c_2Eordinal_2EallOrds(A_27a)) = c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)) )))).
fof(conj_thm_2Eordinal_2Eordlt__mkOrdinal,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0o1] : ( mem(V0o1,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1o2] : ( mem(V1o2,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0o1),V1o2)) <=> ! [V2w1] : ( mem(V2w1,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))) => ! [V3w2] : ( mem(V3w2,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))) => ( ( ( ap(c_2Eordinal_2Eordinal__ABS(A_27a),V2w1) = V0o1 ) & ( ap(c_2Eordinal_2Eordinal__ABS(A_27a),V3w2) = V1o2 ) ) => p(ap(ap(c_2Ewellorder_2Eorderlt(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V2w1),V3w2)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eorderlt__iso__REFL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) => ( ~~ p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27b),V0w1),V1w2)) ) ) ) ))))).
fof(conj_thm_2Eordinal_2Eorderiso__wobound2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27a),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V0x),V1w)),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V2y),V1w))) => ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V2y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w)))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Ewellorder__ordinal__isomorphism,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))) => p(ap(ap(c_2Ewellorder_2Eorderiso(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0w),ap(ap(c_2Ewellorder_2Ewobound(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2Eordinal__ABS(A_27a),V0w)),c_2Eordinal_2EallOrds(A_27a)))) )))).
fof(ax_thm_2Eordinal_2Epreds__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Epreds(A_27a),V0w) = ap(c_2Epred__set_2EGSPEC(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),f2147(A_27a,V0w)) ) ) ) )).
fof(conj_thm_2Eordinal_2EIN__preds,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1w] : ( mem(V1w,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V0x),ap(c_2Eordinal_2Epreds(A_27a),V1w))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),V1w)) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w1] : ( mem(V0w1,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Epreds(A_27a),V0w1) = ap(c_2Eordinal_2Epreds(A_27a),V1w2) ) <=> ( V0w1 = V1w2 ) ) ) )))).
fof(ax_thm_2Eordinal_2Edownward__closed__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(c_2Eordinal_2Edownward__closed(A_27a),V0s)) <=> ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1a),V0s)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),V1a)) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2b),V0s)) ) ) ) ) ) ) )).
fof(conj_thm_2Eordinal_2Epreds__downward__closed,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(c_2Eordinal_2Edownward__closed(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0w))) )))).
fof(conj_thm_2Eordinal_2Epreds__bij,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),bool)),c_2Eordinal_2Epreds(A_27a)),c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a))),ap(ap(c_2Epred__set_2EDELETE(arr(ty_2Eordinal_2Eordinal(A_27a),bool)),c_2Eordinal_2Edownward__closed(A_27a)),c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)))))))).
fof(conj_thm_2Eordinal_2Epreds__lt__PSUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w1] : ( mem(V0w1,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0w1),V1w2)) <=> p(ap(ap(c_2Epred__set_2EPSUBSET(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2Epreds(A_27a),V0w1)),ap(c_2Eordinal_2Epreds(A_27a),V1w2))) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__wobound,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0ord] : ( mem(V0ord,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Epreds(A_27a),V0ord) = ap(c_2Ewellorder_2EelsOf(ty_2Eordinal_2Eordinal(A_27a)),ap(ap(c_2Ewellorder_2Ewobound(ty_2Eordinal_2Eordinal(A_27a)),V0ord),c_2Eordinal_2EallOrds(A_27a))) ) )))).
fof(conj_thm_2Eordinal_2Epreds__inj__univ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0ord] : ( mem(V0ord,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ap(c_2Eordinal_2Epreds(A_27a),V0ord)),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) )))).
fof(conj_thm_2Eordinal_2Eunitinf__univnum,lemma,(p(ap(ap(c_2Ecardinal_2Ecardeq(ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Eone_2Eone),ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Eone_2Eone))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))))).
fof(conj_thm_2Eordinal_2Ecord__countable__preds,lemma,(! [V0ord] : ( mem(V0ord,ty_2Eordinal_2Eordinal(ty_2Eone_2Eone)) => p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(ty_2Eone_2Eone)),ap(c_2Eordinal_2Epreds(ty_2Eone_2Eone),V0ord))) ))).
fof(conj_thm_2Eordinal_2Euniv__ord__greater__cardinal,lemma,( ! [A_27a]: ( ne(A_27a) => ( ~~ p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a))),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) )))).
fof(conj_thm_2Eordinal_2Euniv__cord__uncountable,lemma,(( ~~ p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(ty_2Eone_2Eone)),c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(ty_2Eone_2Eone)))) ))).
fof(conj_thm_2Eordinal_2Eordle__lteq,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0b),V1a)) ) <=> ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V0b)) | ( V1a = V0b ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordle__ANTISYM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0b),V1a)) ) & ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V0b)) ) ) => ( V1a = V0b ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordle__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2z] : ( mem(V2z,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1y),V0x)) ) & ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2z),V1y)) ) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2z),V0x)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlet__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2z] : ( mem(V2z,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1y),V0x)) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1y),V2z)) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),V2z)) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlte__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2z] : ( mem(V2z,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),V1y)) & ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2z),V1y)) ) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),V2z)) ) ) ) )))).
fof(ax_thm_2Eordinal_2Eoleast__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ap(c_2Eordinal_2Eoleast(A_27a),V0P) = ap(c_2Emin_2E_40(ty_2Eordinal_2Eordinal(A_27a)),f2149(A_27a,V0P)) ) ) ) )).
fof(conj_thm_2Eordinal_2Eoleast__intro,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0Q] : ( mem(V0Q,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1P] : ( mem(V1P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( ( ? [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) & p(ap(V1P,V2a)) ) ) & ! [V3a] : ( mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ! [V4b] : ( mem(V4b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V4b),V3a)) => ( ~~ p(ap(V1P,V4b)) ) ) ) ) & p(ap(V1P,V3a)) ) => p(ap(V0Q,V3a)) ) ) ) => p(ap(V0Q,ap(c_2Eordinal_2Eoleast(A_27a),V1P))) ) ) )))).
fof(ax_thm_2Eordinal_2EordSUC__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2EordSUC(A_27a),V0a) = ap(c_2Eordinal_2Eoleast(A_27a),f2150(A_27a,V0a)) ) ) ) )).
fof(ax_thm_2Eordinal_2EfromNat__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) = ap(c_2Eordinal_2Eoleast(A_27a),k(ty_2Eordinal_2Eordinal(A_27a),c_2Ebool_2ET)) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Enum_2ESUC,V1n)) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V1n)) ) ) ) ) )).
fof(conj_thm_2Eordinal_2EfromNat__def__compute,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) = ap(c_2Eordinal_2Eoleast(A_27a),k(ty_2Eordinal_2Eordinal(A_27a),c_2Ebool_2ET)) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V2n))) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V2n)))) ) ) ) )))).
fof(conj_thm_2Eordinal_2EfromNat__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Enum_2ESUC,V0n)) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__ZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0))) ) )))).
fof(conj_thm_2Eordinal_2Epreds__surj,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(c_2Eordinal_2Edownward__closed(A_27a),V0x)) & ( ~~ ( V0x = c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) => ? [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) & ( ap(c_2Eordinal_2Epreds(A_27a),V1y) = V0x ) ) ) )))).
fof(conj_thm_2Eordinal_2Eno__maximal__ordinal,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ? [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),ap(c_2Eordinal_2EordSUC(A_27a),V0a))) )))).
fof(conj_thm_2Eordinal_2EordSUC__ZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ ( ap(c_2Eordinal_2EordSUC(A_27a),V0a) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__DISCRETE1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2EordSUC(A_27a),V0a))) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__SUC__DISCRETE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),ap(c_2Eordinal_2EordSUC(A_27a),V1b))) <=> ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) | ( V0a = V1b ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordSUC__MONO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EordSUC(A_27a),V0a)),ap(c_2Eordinal_2EordSUC(A_27a),V1b))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) ) ) )))).
fof(conj_thm_2Eordinal_2EordSUC__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2EordSUC(A_27a),V0a) = ap(c_2Eordinal_2EordSUC(A_27a),V1b) ) <=> ( V0a = V1b ) ) ) )))).
fof(ax_thm_2Eordinal_2Esup__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0ordset] : ( mem(V0ordset,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ap(c_2Eordinal_2Esup(A_27a),V0ordset) = ap(c_2Eordinal_2Eoleast(A_27a),f2151(A_27a,V0ordset)) ) ) ) )).
fof(conj_thm_2Eordinal_2Eord__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( ! [V1min] : ( mem(V1min,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),V1min)) => p(ap(V0P,V2b)) ) ) ) => p(ap(V0P,V1min)) ) ) ) => ! [V3a] : ( mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(V0P,V3a)) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> ? [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2b),V0s)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V2b)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Esuple__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1s] : ( mem(V1s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V1s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V0b),V1s)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2Esup(A_27a),V1s)),V0b)) ) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__eq__sup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s1] : ( mem(V0s1,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1s2] : ( mem(V1s2,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s1),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V1s2),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( ( ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2a),V0s1)) => ? [V3b] : ( mem(V3b,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V3b),V1s2)) & ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3b),V2a)) ) ) ) ) ) ) & ! [V4b] : ( mem(V4b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V4b),V1s2)) => ? [V5a] : ( mem(V5a,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V5a),V0s1)) & ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V5a),V4b)) ) ) ) ) ) ) ) ) => ( ap(c_2Eordinal_2Esup(A_27a),V0s1) = ap(c_2Eordinal_2Esup(A_27a),V1s2) ) ) ) )))).
fof(conj_thm_2Eordinal_2EUnum__cle__Uinf,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Enum_2Enum,ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))))))).
fof(conj_thm_2Eordinal_2Ecsup__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),V0s)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> ? [V2d] : ( mem(V2d,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2d),V0s)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V2d)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Epredimage__sup__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0f),ap(c_2Eordinal_2Epreds(A_27a),V1a))))) <=> ? [V3d] : ( mem(V3d,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3d),V1a)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),ap(V0f,V3d))) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Epredimage__suplt__ELIM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0f),ap(c_2Eordinal_2Epreds(A_27a),V1a)))),V2b)) => ! [V3d] : ( mem(V3d,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3d),V1a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),ap(V0f,V3d))) ) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Esuppred__suplt__ELIM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2Esup(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0a))),V1b)) => ! [V2d] : ( mem(V2d,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2d),V0a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V2d)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2Esup(A_27a),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a))) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) )))).
fof(conj_thm_2Eordinal_2Esup__SING,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EINSERT(ty_2Eordinal_2Eordinal(A_27a)),V0a),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)))) = V0a ) )))).
fof(conj_thm_2Eordinal_2Esup__preds__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Esup(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EordSUC(A_27a),V0a))) = V0a ) )))).
fof(conj_thm_2Eordinal_2Epreds__ordSUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EordSUC(A_27a),V0a)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Eordinal_2Eordinal(A_27a)),V0a),ap(c_2Eordinal_2Epreds(A_27a),V0a)) ) )))).
fof(conj_thm_2Eordinal_2EcountableOrds__dclosed,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) & p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2Epreds(A_27a),V1b))) ) => p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2Epreds(A_27a),V0a))) ) ) )))).
fof(ax_thm_2Eordinal_2Eomax__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ap(c_2Eordinal_2Eomax(A_27a),V0s) = ap(c_2Eoption_2Esome(ty_2Eordinal_2Eordinal(A_27a)),f2154(A_27a,V0s)) ) ) ) )).
fof(conj_thm_2Eordinal_2Eomax__SOME,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),V0s) = ap(c_2Eoption_2ESOME(ty_2Eordinal_2Eordinal(A_27a)),V1a) ) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1a),V0s)) & ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2b),V0s)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V2b)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eomax__NONE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),V0s) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) <=> ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1a),V0s)) => ? [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2b),V0s)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V2b)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eomax__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2Eomax(A_27a),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) )))).
fof(conj_thm_2Eordinal_2Epreds__0,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) )))).
fof(conj_thm_2Eordinal_2Eordleq0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x)) ) <=> ( V0x = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__EQ__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Epreds(A_27a),V0x) = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) ) <=> ( V0x = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Eordinal_2Eomax__sup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),V0s) = ap(c_2Eoption_2ESOME(ty_2Eordinal_2Eordinal(A_27a)),V1a) ) => ( ap(c_2Eordinal_2Esup(A_27a),V0s) = V1a ) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__omax__SOME__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0a)) = ap(c_2Eoption_2ESOME(ty_2Eordinal_2Eordinal(A_27a)),V1b) ) <=> ( V0a = ap(c_2Eordinal_2EordSUC(A_27a),V1b) ) ) ) )))).
fof(conj_thm_2Eordinal_2Esimple__ord__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(V0P,ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0))) & ( ( ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(V0P,V1a)) => p(ap(V0P,ap(c_2Eordinal_2EordSUC(A_27a),V1a))) ) ) ) & ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V2a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) & ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V2a)) & ! [V3b] : ( mem(V3b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3b),V2a)) => p(ap(V0P,V3b)) ) ) ) ) => p(ap(V0P,V2a)) ) ) ) ) => ! [V4a] : ( mem(V4a,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(V0P,V4a)) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__preds__omax__NONE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) <=> ( ap(c_2Eordinal_2Esup(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0a)) = V0a ) ) )))).
fof(ax_thm_2Eordinal_2Edclose__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ap(c_2Eordinal_2Edclose(A_27a),V0s) = ap(c_2Epred__set_2EGSPEC(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),f2156(A_27a,V0s)) ) ) ) )).
fof(conj_thm_2Eordinal_2Epreds__sup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) => ( ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2Esup(A_27a),V0s)) = ap(c_2Eordinal_2Edclose(A_27a),V0s) ) ) )))).
fof(conj_thm_2Eordinal_2Ecsup__lesup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),V0s)) => ! [V1d] : ( mem(V1d,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1d),V0s)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2Esup(A_27a),V0s)),V1d)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Ecsup__suple,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),V0s)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),V0s))) ) <=> ! [V2d] : ( mem(V2d,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2d),V0s)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V2d)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__sup__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(c_2Eordinal_2Edownward__closed(A_27a),V0s)) & ( ~~ ( V0s = c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> ? [V2d] : ( mem(V2d,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2d),V0s)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V2d)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__lesup,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(c_2Eordinal_2Edownward__closed(A_27a),V0s)) & ( ~~ ( V0s = c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) => ! [V1d] : ( mem(V1d,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1d),V0s)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2Esup(A_27a),V0s)),V1d)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Epreds__suple,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(c_2Eordinal_2Edownward__closed(A_27a),V0s)) & ( ~~ ( V0s = c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),V0s))) ) <=> ! [V2d] : ( mem(V2d,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2d),V0s)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V2d)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EfromNat__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1y] : ( mem(V1y,ty_2Enum_2Enum) => ( ( ap(c_2Eordinal_2EfromNat(A_27a),V0x) = ap(c_2Eordinal_2EfromNat(A_27a),V1y) ) <=> ( V0x = V1y ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__fromNat,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1x),ap(c_2Eordinal_2EfromNat(A_27a),V0n))) <=> ? [V2m] : ( mem(V2m,ty_2Enum_2Enum) & ( ( V1x = ap(c_2Eordinal_2EfromNat(A_27a),V2m) ) & p(ap(ap(c_2Eprim__rec_2E_3C,V2m),V0n)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EfromNat__ordlt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)),ap(c_2Eordinal_2EfromNat(A_27a),V1m))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,V0n),V1m)) ) ) )))).
fof(ax_thm_2Eordinal_2Eomega__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Eordinal_2Eomega(A_27a) = ap(c_2Eordinal_2Esup(A_27a),ap(c_2Epred__set_2EGSPEC(ty_2Eordinal_2Eordinal(A_27a),ty_2Enum_2Enum),f2157(A_27a))) ) ) )).
fof(conj_thm_2Eordinal_2Elt__omega,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),c_2Eordinal_2Eomega(A_27a))) <=> ? [V1m] : ( mem(V1m,ty_2Enum_2Enum) & ( V0a = ap(c_2Eordinal_2EfromNat(A_27a),V1m) ) ) ) )))).
fof(conj_thm_2Eordinal_2EfromNat__lt__omega,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)),c_2Eordinal_2Eomega(A_27a))) )))).
fof(conj_thm_2Eordinal_2EfromNat__eq__omega,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ~~ ( ap(c_2Eordinal_2EfromNat(A_27a),V0n) = c_2Eordinal_2Eomega(A_27a) ) ) )))).
fof(conj_thm_2Eordinal_2Eord__RECURSION,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0z] : ( mem(V0z,A_27b) => ! [V1sf] : ( mem(V1sf,arr(ty_2Eordinal_2Eordinal(A_27a),arr(A_27b,A_27b))) => ! [V2lf] : ( mem(V2lf,arr(ty_2Eordinal_2Eordinal(A_27a),arr(arr(A_27b,bool),A_27b))) => ? [V3h] : ( mem(V3h,arr(ty_2Eordinal_2Eordinal(A_27a),A_27b)) & ( ( ap(V3h,ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = V0z ) & ( ( ! [V4a] : ( mem(V4a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(V3h,ap(c_2Eordinal_2EordSUC(A_27a),V4a)) = ap(ap(V1sf,V4a),ap(V3h,V4a)) ) ) ) & ! [V5a] : ( mem(V5a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V5a)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V5a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(V3h,V5a) = ap(ap(V2lf,V5a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),A_27b),V3h),ap(c_2Eordinal_2Epreds(A_27a),V5a))) ) ) ) ) ) ) ) ) ))))).
fof(ax_thm_2Eordinal_2EordADD__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordADD(A_27a),V0b),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = V0b ) & ( ( ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),V0b),ap(c_2Eordinal_2EordSUC(A_27a),V1a)) = ap(c_2Eordinal_2EordSUC(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V0b),V1a)) ) ) ) & ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V2a)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V2a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),V0b),V2a) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordADD(A_27a),V0b)),ap(c_2Eordinal_2Epreds(A_27a),V2a))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eordinal_2EordADD__0L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0a) = V0a ) )))).
fof(conj_thm_2Eordinal_2Eubsup__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2a),V0s)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2a),V1b)) ) ) ) => ! [V3c] : ( mem(V3c,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> ? [V4d] : ( mem(V4d,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V4d),V0s)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),V4d)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__fromNat,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)),ap(c_2Eordinal_2EfromNat(A_27a),V1m)) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2B,V0n),V1m)) ) ) )))).
fof(conj_thm_2Eordinal_2Eomax__preds__omega,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),c_2Eordinal_2Eomega(A_27a))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) )))).
fof(conj_thm_2Eordinal_2Eomega__islimit,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),c_2Eordinal_2Eomega(A_27a))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) )))).
fof(conj_thm_2Eordinal_2EordADD__fromNat__omega,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)),c_2Eordinal_2Eomega(A_27a)) = c_2Eordinal_2Eomega(A_27a) ) )))).
fof(conj_thm_2Eordinal_2Elt__suppreds,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0a)))) <=> ? [V2d] : ( mem(V2d,ty_2Eordinal_2Eordinal(A_27a)) & ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2d),V0a)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V2d)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eomax__preds__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EordSUC(A_27a),V0x))) = ap(c_2Eoption_2ESOME(ty_2Eordinal_2Eordinal(A_27a)),V0x) ) )))).
fof(conj_thm_2Eordinal_2EORD__ONE,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) )))).
fof(conj_thm_2Eordinal_2EordSUC__NUMERAL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,V0n))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) )))).
fof(conj_thm_2Eordinal_2EordZERO__ltSUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),ap(c_2Eordinal_2EordSUC(A_27a),V0x))) )))).
fof(conj_thm_2Eordinal_2Eordlt__CANCEL__ADDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V0b))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0b)) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__CANCEL__ADDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V1b)),V0a)) <=> $false ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__CANCEL1,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0c] : ( mem(V0c,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( V1a = ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V0c) ) <=> ( V0c = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) ) ) ) & ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ! [V3a] : ( mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordADD(A_27a),V3a),V2c) = V3a ) <=> ( V2c = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__MONO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V0b)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V2c),V1a)),ap(ap(c_2Eordinal_2EordADD(A_27a),V2c),V0b))) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__CANCEL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V2c),V1a)),ap(ap(c_2Eordinal_2EordADD(A_27a),V2c),V0b))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V0b)) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__RIGHT__CANCEL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V0b) = ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V2c) ) <=> ( V0b = V2c ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EleqLEFT__CANCEL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V0x)),V0x)) ) ) )))).
fof(conj_thm_2Eordinal_2Eordlt__EXISTS__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) <=> ? [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) & ( ( ~~ ( V2c = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) & ( V1b = ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V2c) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordle__EXISTS__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V0a)) ) <=> ? [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) & ( V1b = ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V2c) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eordle__CANCEL__ADDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V0x),V1a)),V0x)) ) ) )))).
fof(conj_thm_2Eordinal_2Edclose__BIGUNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ap(c_2Eordinal_2Edclose(A_27a),V0s) = ap(c_2Epred__set_2EBIGUNION(ty_2Eordinal_2Eordinal(A_27a)),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),bool)),c_2Eordinal_2Epreds(A_27a)),V0s)) ) )))).
fof(conj_thm_2Eordinal_2EcountableOrds__uncountable,lemma,( ! [A_27a]: ( ne(A_27a) => ( ~~ p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Epred__set_2EGSPEC(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),f2158(A_27a)))) )))).
fof(conj_thm_2Eordinal_2Edclose__cardleq__univinf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) => p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ap(c_2Eordinal_2Edclose(A_27a),V0s)),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) ) )))).
fof(conj_thm_2Eordinal_2Esup__lt__implies,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2Esup(A_27a),V0s)),V1a)) & p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2b),V0s)) ) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),V1a)) ) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__eq__max,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2b),V0s)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V2b)) ) ) ) ) & p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1a),V0s)) ) => ( ap(c_2Eordinal_2Esup(A_27a),V0s) = V1a ) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__eq__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( ap(c_2Eordinal_2Esup(A_27a),V0s) = ap(c_2Eordinal_2EordSUC(A_27a),V1a) ) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordSUC(A_27a),V1a)),V0s)) ) ) )))).
fof(conj_thm_2Eordinal_2Egeneric__continuity,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ( ( ( ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V1a)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V1a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(V0f,V1a) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0f),ap(c_2Eordinal_2Epreds(A_27a),V1a))) ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V3y] : ( mem(V3y,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3y),V2x)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(V0f,V3y)),ap(V0f,V2x))) ) ) ) ) ) => ! [V4s] : ( mem(V4s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V4s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( ~~ ( V4s = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) => ( ap(V0f,ap(c_2Eordinal_2Esup(A_27a),V4s)) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0f),V4s)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eord__CASES,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( V0a = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) | ( ( ? [V1a0] : ( mem(V1a0,ty_2Eordinal_2Eordinal(A_27a)) & ( V0a = ap(c_2Eordinal_2EordSUC(A_27a),V1a0) ) ) ) | ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0a)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Eislimit__0,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) )))).
fof(conj_thm_2Eordinal_2Eordinal__IVT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ! [V1a1] : ( mem(V1a1,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2a2] : ( mem(V2a2,ty_2Eordinal_2Eordinal(A_27a)) => ! [V3c] : ( mem(V3c,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ! [V4a] : ( mem(V4a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V4a)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V4a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(V0f,V4a) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0f),ap(c_2Eordinal_2Epreds(A_27a),V4a))) ) ) ) ) & ( ( ! [V5x] : ( mem(V5x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V6y] : ( mem(V6y,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V6y),V5x)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(V0f,V6y)),ap(V0f,V5x))) ) ) ) ) ) & ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a1),V2a2)) & ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),ap(V0f,V1a1))) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),ap(V0f,V2a2))) ) ) ) ) => ? [V7b] : ( mem(V7b,ty_2Eordinal_2Eordinal(A_27a)) & ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V7b),V1a1)) ) & ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V7b),V2a2)) & ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),ap(V0f,V7b))) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),ap(V0f,ap(c_2Eordinal_2EordSUC(A_27a),V7b)))) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__continuous,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1s] : ( mem(V1s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V1s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( ~~ ( V1s = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),ap(c_2Eordinal_2Esup(A_27a),V1s)) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordADD(A_27a),V0a)),V1s)) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__ASSOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),ap(ap(c_2Eordinal_2EordADD(A_27a),V1b),V2c)) = ap(ap(c_2Eordinal_2EordADD(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V1b)),V2c) ) ) ) )))).
fof(conj_thm_2Eordinal_2EADD1R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Eordinal_2EordSUC(A_27a),V0a) ) )))).
fof(conj_thm_2Eordinal_2EordADD__weak__MONO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0c] : ( mem(V0c,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V2b)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V2b),V0c)),ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V0c))) ) ) ) ) )))).
fof(ax_thm_2Eordinal_2EordMULT__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0b),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) & ( ( ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0b),ap(c_2Eordinal_2EordSUC(A_27a),V1a)) = ap(ap(c_2Eordinal_2EordADD(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V0b),V1a)),V0b) ) ) ) & ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V2a)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V2a)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0b),V2a) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordMULT(A_27a),V0b)),ap(c_2Eordinal_2Epreds(A_27a),V2a))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eordinal_2EordMULT__0L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0a) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__0R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__1L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0a) = V0a ) )))).
fof(conj_thm_2Eordinal_2EordMULT__1R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0a ) )))).
fof(conj_thm_2Eordinal_2EordMULT__2R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V0a) ) )))).
fof(conj_thm_2Eordinal_2Eislimit__SUC__lt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0b] : ( mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0b)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V0b)) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EordSUC(A_27a),V1a)),V0b)) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__lt__MONO__R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V2c)) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),V0a)),ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),V1b))) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__le__MONO__R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V0a)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),V1b)),ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),V0a))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__lt__MONO__R__EQN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0c] : ( mem(V0c,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V0c),V1a)),ap(ap(c_2Eordinal_2EordMULT(A_27a),V0c),V2b))) <=> ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),V2b)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0c)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__le__MONO__L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0y] : ( mem(V0y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2z] : ( mem(V2z,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0y),V1x)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordADD(A_27a),V0y),V2z)),ap(ap(c_2Eordinal_2EordADD(A_27a),V1x),V2z))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__le__MONO__L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V0a)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V1b),V2c)),ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),V2c))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__CANCEL__R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0z] : ( mem(V0z,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2y] : ( mem(V2y,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0z),V1x) = ap(ap(c_2Eordinal_2EordMULT(A_27a),V0z),V2y) ) <=> ( ( V0z = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) | ( V1x = V2y ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__continuous,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1s] : ( mem(V1s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V1s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),ap(c_2Eordinal_2Esup(A_27a),V1s)) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordMULT(A_27a),V0a)),V1s)) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__fromNat,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)),ap(c_2Eordinal_2EfromNat(A_27a),V1m)) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2A,V0n),V1m)) ) ) )))).
fof(conj_thm_2Eordinal_2Eomega__MUL__fromNat,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0n)),c_2Eordinal_2Eomega(A_27a)) = c_2Eordinal_2Eomega(A_27a) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__LDISTRIB,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V1b)) = ap(ap(c_2Eordinal_2EordADD(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),V0a)),ap(ap(c_2Eordinal_2EordMULT(A_27a),V2c),V1b)) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMULT__ASSOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2c] : ( mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V1b),V2c)) = ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),V1b)),V2c) ) ) ) )))).
fof(ax_thm_2Eordinal_2EordDIVISION,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V1b)) => ( ( V0a = ap(ap(c_2Eordinal_2EordADD(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V1b),ap(ap(c_2Eordinal_2EordDIV(A_27a),V0a),V1b))),ap(ap(c_2Eordinal_2EordMOD(A_27a),V0a),V1b)) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordMOD(A_27a),V0a),V1b)),V1b)) ) ) ) ) ) )).
fof(conj_thm_2Eordinal_2EordDIV__UNIQUE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2q] : ( mem(V2q,ty_2Eordinal_2Eordinal(A_27a)) => ! [V3r] : ( mem(V3r,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V1b)) & ( ( V0a = ap(ap(c_2Eordinal_2EordADD(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V1b),V2q)),V3r) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3r),V1b)) ) ) => ( ap(ap(c_2Eordinal_2EordDIV(A_27a),V0a),V1b) = V2q ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordMOD__UNIQUE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1b] : ( mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2q] : ( mem(V2q,ty_2Eordinal_2Eordinal(A_27a)) => ! [V3r] : ( mem(V3r,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V1b)) & ( ( V0a = ap(ap(c_2Eordinal_2EordADD(A_27a),ap(ap(c_2Eordinal_2EordMULT(A_27a),V1b),V2q)),V3r) ) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3r),V1b)) ) ) => ( ap(ap(c_2Eordinal_2EordMOD(A_27a),V0a),V1b) = V3r ) ) ) ) ) )))).
fof(ax_thm_2Eordinal_2EordEXP__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ( ( ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2a_27] : ( mem(V2a_27,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V1a),ap(c_2Eordinal_2EordSUC(A_27a),V2a_27)) = ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V1a),V2a_27)),V1a) ) ) ) ) & ! [V3a] : ( mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V4a_27] : ( mem(V4a_27,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V4a_27)) & ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V4a_27)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V3a),V4a_27) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordEXP(A_27a),V3a)),ap(c_2Eordinal_2Epreds(A_27a),V4a_27))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eordinal_2EordEXP__1R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0a ) )))).
fof(conj_thm_2Eordinal_2EordEXP__1L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0a) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__2R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),V0a) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__fromNat,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0x)),ap(c_2Eordinal_2EfromNat(A_27a),V1n)) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2EEXP,V0x),V1n)) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__le__MONO__L,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1a] : ( mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V2b),V1a)) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2b),V0x)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V1a),V0x))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EIFF__ZERO__lt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ( ~~ ( V0x = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x)) ) & ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x)) ) ) )))).
fof(conj_thm_2Eordinal_2Eislimit__SUC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EordSUC(A_27a),V0x))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) <=> $false ) )))).
fof(conj_thm_2Eordinal_2Eislimit__fromNat,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Enum_2Enum) => ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),V0x))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) <=> ( V0x = c_2Enum_2E0 ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__ZERO__limit,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0x)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__ZERO__nonlimit,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ~~ ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0x)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) )))).
fof(conj_thm_2Eordinal_2Esup__EQ__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V0s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) => ( ( ap(c_2Eordinal_2Esup(A_27a),V0s) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) <=> ( ( V0s = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) ) | ( V0s = ap(ap(c_2Epred__set_2EINSERT(ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordADD__EQ__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0y] : ( mem(V0y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordADD(A_27a),V1x),V0y) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) <=> ( ( V1x = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) & ( V0y = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EIMAGE__EQ__SING,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27b,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( ap(ap(c_2Epred__set_2EIMAGE(A_27b,A_27a),V0f),V1s) = ap(ap(c_2Epred__set_2EINSERT(A_27a),V2x),c_2Epred__set_2EEMPTY(A_27a)) ) <=> ( ( ? [V3y] : ( mem(V3y,A_27b) & p(ap(ap(c_2Ebool_2EIN(A_27b),V3y),V1s)) ) ) & ! [V4y] : ( mem(V4y,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V4y),V1s)) => ( ap(V0f,V4y) = V2x ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eordinal_2EordMULT__EQ__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordMULT(A_27a),V0x),V1y) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) <=> ( ( V0x = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) | ( V1y = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__EQ__0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0y] : ( mem(V0y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V1x),V0y) = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) <=> ( ( V1x = ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0) ) & ( ~~ ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0y)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EZERO__lt__ordEXP__I,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0a)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),V1x))) ) ) )))).
fof(conj_thm_2Eordinal_2EZERO__lt__ordEXP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),V1x))) <=> ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0a)) | ( ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V1x)) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__lt__MONO__R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0y] : ( mem(V0y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1x] : ( mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2a)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1x),V0y)) ) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2a),V1x)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2a),V0y))) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__lt__IFF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2a),V0x)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2a),V1y))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0x),V1y)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__le__MONO__R,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2a] : ( mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V2a)) & ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1y),V0x)) ) ) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2a),V1y)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V2a),V0x))) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__continuous,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1s] : ( mem(V1s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0a)) & ( p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V1s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) & ( ~~ ( V1s = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) ) ) ) ) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),ap(c_2Eordinal_2Esup(A_27a),V1s)) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),ap(c_2Eordinal_2EordEXP(A_27a),V0a)),V1s)) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__ADD,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2z] : ( mem(V2z,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V0x),ap(ap(c_2Eordinal_2EordADD(A_27a),V1y),V2z)) = ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V0x),V1y)),ap(ap(c_2Eordinal_2EordEXP(A_27a),V0x),V2z)) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2EordEXP__MUL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ! [V1y] : ( mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ! [V2z] : ( mem(V2z,ty_2Eordinal_2Eordinal(A_27a)) => ( p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),c_2Enum_2E0)),V0x)) => ( ap(ap(c_2Eordinal_2EordEXP(A_27a),V0x),ap(ap(c_2Eordinal_2EordMULT(A_27a),V1y),V2z)) = ap(ap(c_2Eordinal_2EordEXP(A_27a),ap(ap(c_2Eordinal_2EordEXP(A_27a),V0x),V1y)),V2z) ) ) ) ) )))).
fof(conj_thm_2Eordinal_2Efixpoints__exist,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ( ( ( ! [V1s] : ( mem(V1s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ( ( ~~ ( V1s = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)) ) ) & p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Eordinal_2Eordinal(A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),V1s),c_2Epred__set_2EUNIV(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) ) => ( ap(V0f,ap(c_2Eordinal_2Esup(A_27a),V1s)) = ap(c_2Eordinal_2Esup(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)),V0f),V1s)) ) ) ) ) & ! [V2x] : ( mem(V2x,ty_2Eordinal_2Eordinal(A_27a)) => ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(V0f,V2x)),V2x)) ) ) ) => ! [V3a] : ( mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ? [V4b] : ( mem(V4b,ty_2Eordinal_2Eordinal(A_27a)) & ( ( ~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V4b),V3a)) ) & ( ap(V0f,V4b) = V4b ) ) ) ) ) )))).
