include('Axioms/integer_2.ax').
tff(tp_ty_2Eordinal_2Eordinal,type,( ty_2Eordinal_2Eordinal: del > del )).
tff(tp_c_2Eordinal_2EallOrds,type,(c_2Eordinal_2EallOrds:del > $i)).
tff(mem_c_2Eordinal_2EallOrds,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EallOrds(A_27a),ty_2Ewellorder_2Ewellorder(ty_2Eordinal_2Eordinal(A_27a))))).
tff(tp_c_2Eordinal_2Edclose,type,(c_2Eordinal_2Edclose:del > $i)).
tff(mem_c_2Eordinal_2Edclose,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Edclose(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),arr(ty_2Eordinal_2Eordinal(A_27a),bool))))).
tff(tp_c_2Eordinal_2Edownward__closed,type,(c_2Eordinal_2Edownward__closed:del > $i)).
tff(mem_c_2Eordinal_2Edownward__closed,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Edownward__closed(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),bool)))).
tff(tp_c_2Eordinal_2Eepsilon0,type,(c_2Eordinal_2Eepsilon0:del > $i)).
tff(mem_c_2Eordinal_2Eepsilon0,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eepsilon0(A_27a),ty_2Eordinal_2Eordinal(A_27a)))).
tff(tp_c_2Eordinal_2Eeval__poly,type,(c_2Eordinal_2Eeval__poly:del > $i)).
tff(mem_c_2Eordinal_2Eeval__poly,axiom,( ! [A_27a:del] : 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)))))).
tff(tp_c_2Eordinal_2EfromNat,type,(c_2Eordinal_2EfromNat:del > $i)).
tff(mem_c_2Eordinal_2EfromNat,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EfromNat(A_27a),arr(ty_2Enum_2Enum,ty_2Eordinal_2Eordinal(A_27a))))).
tff(tp_c_2Eordinal_2Eis__polyform,type,(c_2Eordinal_2Eis__polyform:(del * del) > $i)).
tff(mem_c_2Eordinal_2Eis__polyform,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))).
tff(tp_c_2Eordinal_2Eoleast,type,(c_2Eordinal_2Eoleast:del > $i)).
tff(mem_c_2Eordinal_2Eoleast,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eoleast(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),ty_2Eordinal_2Eordinal(A_27a))))).
tff(tp_c_2Eordinal_2Eomax,type,(c_2Eordinal_2Eomax:del > $i)).
tff(mem_c_2Eordinal_2Eomax,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eomax(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),ty_2Eoption_2Eoption(ty_2Eordinal_2Eordinal(A_27a)))))).
tff(tp_c_2Eordinal_2Eomega,type,(c_2Eordinal_2Eomega:del > $i)).
tff(mem_c_2Eordinal_2Eomega,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eomega(A_27a),ty_2Eordinal_2Eordinal(A_27a)))).
tff(tp_c_2Eordinal_2EordADD,type,(c_2Eordinal_2EordADD:del > $i)).
tff(mem_c_2Eordinal_2EordADD,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EordADD(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))))).
tff(tp_c_2Eordinal_2EordDIV,type,(c_2Eordinal_2EordDIV:del > $i)).
tff(mem_c_2Eordinal_2EordDIV,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EordDIV(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))))).
tff(tp_c_2Eordinal_2EordEXP,type,(c_2Eordinal_2EordEXP:del > $i)).
tff(mem_c_2Eordinal_2EordEXP,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EordEXP(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))))).
tff(tp_c_2Eordinal_2EordMOD,type,(c_2Eordinal_2EordMOD:del > $i)).
tff(mem_c_2Eordinal_2EordMOD,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EordMOD(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))))).
tff(tp_c_2Eordinal_2EordMULT,type,(c_2Eordinal_2EordMULT:del > $i)).
tff(mem_c_2Eordinal_2EordMULT,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EordMULT(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a)))))).
tff(tp_c_2Eordinal_2EordSUC,type,(c_2Eordinal_2EordSUC:del > $i)).
tff(mem_c_2Eordinal_2EordSUC,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2EordSUC(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))))).
tff(tp_c_2Eordinal_2Eordinal__ABS,type,(c_2Eordinal_2Eordinal__ABS:del > $i)).
tff(mem_c_2Eordinal_2Eordinal__ABS,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eordinal__ABS(A_27a),arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ty_2Eordinal_2Eordinal(A_27a))))).
tff(tp_c_2Eordinal_2Eordinal__ABS__CLASS,type,(c_2Eordinal_2Eordinal__ABS__CLASS:del > $i)).
tff(mem_c_2Eordinal_2Eordinal__ABS__CLASS,axiom,( ! [A_27a:del] : 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))))).
tff(tp_c_2Eordinal_2Eordinal__REP,type,(c_2Eordinal_2Eordinal__REP:del > $i)).
tff(mem_c_2Eordinal_2Eordinal__REP,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eordinal__REP(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))))).
tff(tp_c_2Eordinal_2Eordinal__REP__CLASS,type,(c_2Eordinal_2Eordinal__REP__CLASS:del > $i)).
tff(mem_c_2Eordinal_2Eordinal__REP__CLASS,axiom,( ! [A_27a:del] : 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))))).
tff(tp_c_2Eordinal_2Eordlt,type,(c_2Eordinal_2Eordlt:del > $i)).
tff(mem_c_2Eordinal_2Eordlt,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Eordlt(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),bool))))).
tff(tp_c_2Eordinal_2Epolyform,type,(c_2Eordinal_2Epolyform:del > $i)).
tff(mem_c_2Eordinal_2Epolyform,axiom,( ! [A_27a:del] : 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)))))))).
tff(tp_c_2Eordinal_2Epreds,type,(c_2Eordinal_2Epreds:del > $i)).
tff(mem_c_2Eordinal_2Epreds,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Epreds(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),arr(ty_2Eordinal_2Eordinal(A_27a),bool))))).
tff(tp_c_2Eordinal_2Esup,type,(c_2Eordinal_2Esup:del > $i)).
tff(mem_c_2Eordinal_2Esup,axiom,( ! [A_27a:del] : mem(c_2Eordinal_2Esup(A_27a),arr(arr(ty_2Eordinal_2Eordinal(A_27a),bool),ty_2Eordinal_2Eordinal(A_27a))))).
tff(ax_thm_2Eordinal_2Eordinal__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : (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)))))).
tff(ax_thm_2Eordinal_2Eordinal__bijections,axiom,( ! [A_27a:del]: (( ! [V0a:$i] : (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:$i] : (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))))))).
tff(conj_thm_2Eordinal_2Eordinal__ABS__REP__CLASS,lemma,(( ! [A_27a:del]: (( ! [V0a:$i] : (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:$i] : (mem(V1c,arr(ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool)) => ((? [V2r:$i] : (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)))))))).
tff(ax_thm_2Eordinal_2Eordinal__REP__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (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))))))).
tff(ax_thm_2Eordinal_2Eordinal__ABS__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (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))))))).
tff(conj_thm_2Eordinal_2Eordinal__QUOTIENT,lemma,(( ! [A_27a:del]: 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)))))).
tff(ax_thm_2Eordinal_2Eordlt__def,axiom,( ! [A_27a:del]: ( ! [V0T1:$i] : (mem(V0T1,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1T2:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Eordlt__REFL,lemma,(( ! [A_27a:del]: ( ! [V0w:$i] : (mem(V0w,ty_2Eordinal_2Eordinal(A_27a)) => (~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0w),V0w)))))))).
tff(conj_thm_2Eordinal_2Eordlt__TRANS,lemma,(( ! [A_27a:del]: ( ! [V0w1:$i] : (mem(V0w1,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1w2:$i] : (mem(V1w2,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2w3:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Eordlt__WF,lemma,(( ! [A_27a:del]: p(ap(c_2Erelation_2EWF(ty_2Eordinal_2Eordinal(A_27a)),c_2Eordinal_2Eordlt(A_27a)))))).
tff(conj_thm_2Eordinal_2Eordlt__trichotomy,lemma,(( ! [A_27a:del]: ( ! [V0w2:$i] : (mem(V0w2,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1w1:$i] : (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))))))))))).
tff(ax_thm_2Eordinal_2EallOrds__def,axiom,( ! [A_27a:del]: (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))))))).
tff(conj_thm_2Eordinal_2Ewellorder__allOrds,lemma,(( ! [A_27a:del]: 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)))))))).
tff(conj_thm_2Eordinal_2EWIN__allOrds,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1y:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2EelsOf__allOrds,lemma,(( ! [A_27a:del]: (ap(c_2Ewellorder_2EelsOf(ty_2Eordinal_2Eordinal(A_27a)),c_2Eordinal_2EallOrds(A_27a)) = c_2Epred__set_2EUNIV(ty_2Eordinal_2Eordinal(A_27a)))))).
tff(conj_thm_2Eordinal_2Eordlt__mkOrdinal,lemma,(( ! [A_27a:del]: ( ! [V0o1:$i] : (mem(V0o1,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1o2:$i] : (mem(V1o2,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0o1),V1o2)) <=> ( ! [V2w1:$i] : (mem(V2w1,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a))) => ( ! [V3w2:$i] : (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))))))))))))))).
tff(conj_thm_2Eordinal_2Eorderlt__iso__REFL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : (mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ! [V1w2:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Eorderiso__wobound2,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1w:$i] : (mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ! [V2y:$i] : (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))))))))))))))).
tff(conj_thm_2Eordinal_2Ewellorder__ordinal__isomorphism,lemma,(( ! [A_27a:del]: ( ! [V0w:$i] : (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))))))))).
tff(ax_thm_2Eordinal_2Epreds__def,axiom,( ! [A_27a:del]: ( ! [V0w:$i] : (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))))))).
tff(conj_thm_2Eordinal_2EIN__preds,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1w:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Epreds__11,lemma,(( ! [A_27a:del]: ( ! [V0w1:$i] : (mem(V0w1,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1w2:$i] : (mem(V1w2,ty_2Eordinal_2Eordinal(A_27a)) => ((ap(c_2Eordinal_2Epreds(A_27a),V0w1) = ap(c_2Eordinal_2Epreds(A_27a),V1w2)) <=> (V0w1 = V1w2))))))))).
tff(ax_thm_2Eordinal_2Edownward__closed__def,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => (p(ap(c_2Eordinal_2Edownward__closed(A_27a),V0s)) <=> ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Epreds__downward__closed,lemma,(( ! [A_27a:del]: ( ! [V0w:$i] : (mem(V0w,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(c_2Eordinal_2Edownward__closed(A_27a),ap(c_2Eordinal_2Epreds(A_27a),V0w)))))))).
tff(conj_thm_2Eordinal_2Epreds__bij,lemma,(( ! [A_27a:del]: 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)))))))).
tff(conj_thm_2Eordinal_2Epreds__lt__PSUBSET,lemma,(( ! [A_27a:del]: ( ! [V0w1:$i] : (mem(V0w1,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1w2:$i] : (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))))))))))).
tff(conj_thm_2Eordinal_2Epreds__wobound,lemma,(( ! [A_27a:del]: ( ! [V0ord:$i] : (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))))))))).
tff(conj_thm_2Eordinal_2Epreds__inj__univ,lemma,(( ! [A_27a:del]: ( ! [V0ord:$i] : (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))))))))).
tff(stp_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,type,(tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone : $tType)).
tff(stp_inj_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,type,(inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone : tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone > $i)).
tff(stp_surj_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,type,(surj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone : $i > tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone)).
tff(stp_inj_surj_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone] : (surj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone(inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone(X)) = X))).
tff(stp_inj_mem_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone] : (mem(inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone(X),ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Eone_2Eone))))).
tff(stp_iso_mem_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,axiom,( ! [X:$i] : (mem(X,ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Eone_2Eone)) => (X = inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone(surj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone(X)))))).
tff(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))))).
tff(stp_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,type,(tp__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone : $tType)).
tff(stp_inj_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,type,(inj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone : tp__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone > $i)).
tff(stp_surj_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,type,(surj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone : $i > tp__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone)).
tff(stp_inj_surj_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone] : (surj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone(inj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone(X)) = X))).
tff(stp_inj_mem_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone] : (mem(inj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone(X),ty_2Eordinal_2Eordinal(ty_2Eone_2Eone))))).
tff(stp_iso_mem_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,axiom,( ! [X:$i] : (mem(X,ty_2Eordinal_2Eordinal(ty_2Eone_2Eone)) => (X = inj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone(surj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone(X)))))).
tff(conj_thm_2Eordinal_2Ecord__countable__preds,lemma,(( ! [V0ord:tp__c_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),inj__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone(V0ord))))))).
tff(conj_thm_2Eordinal_2Euniv__ord__greater__cardinal,lemma,(( ! [A_27a:del]: (~~ 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)))))))).
tff(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))))))).
tff(conj_thm_2Eordinal_2Eordle__lteq,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Eordle__ANTISYM,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (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))))))))).
tff(conj_thm_2Eordinal_2Eordle__TRANS,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1y:$i] : (mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2z:$i] : (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))))))))))))).
tff(conj_thm_2Eordinal_2Eordlet__TRANS,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1y:$i] : (mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2z:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Eordlte__TRANS,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1y:$i] : (mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2z:$i] : (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)))))))))))).
tff(ax_thm_2Eordinal_2Eoleast__def,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : (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))))))).
tff(conj_thm_2Eordinal_2Eoleast__intro,lemma,(( ! [A_27a:del]: ( ! [V0Q:$i] : (mem(V0Q,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => (((? [V2a:$i] : (mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) & p(ap(V1P,V2a)))) & ( ! [V3a:$i] : (mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ((( ! [V4b:$i] : (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))))))))))).
tff(ax_thm_2Eordinal_2EordSUC__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (ap(c_2Eordinal_2EordSUC(A_27a),V0a) = ap(c_2Eordinal_2Eoleast(A_27a),f2150(A_27a,V0a))))))).
tff(ax_thm_2Eordinal_2EfromNat__def,axiom,( ! [A_27a:del]: ((ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = ap(c_2Eordinal_2Eoleast(A_27a),k(ty_2Eordinal_2Eordinal(A_27a),c_2Ebool_2ET))) & ( ! [V1n:tp__ty_2Enum_2Enum] : (ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Eordinal_2EfromNat__def__compute,lemma,(( ! [A_27a:del]: ((ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = ap(c_2Eordinal_2Eoleast(A_27a),k(ty_2Eordinal_2Eordinal(A_27a),c_2Ebool_2ET))) & (( ! [V1n:tp__ty_2Enum_2Enum] : (ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(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,inj__ty_2Enum_2Enum(V1n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : (ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2n)))) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2n)))))))))))).
tff(conj_thm_2Eordinal_2EfromNat__SUC,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))) = ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Eordinal_2Eordlt__ZERO,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Eordinal_2Epreds__surj,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (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:$i] : (mem(V1y,ty_2Eordinal_2Eordinal(A_27a)) & (ap(c_2Eordinal_2Epreds(A_27a),V1y) = V0x))))))))).
tff(conj_thm_2Eordinal_2Eno__maximal__ordinal,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (? [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) & p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b))))))))).
tff(conj_thm_2Eordinal_2Eordlt__SUC,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),ap(c_2Eordinal_2EordSUC(A_27a),V0a)))))))).
tff(conj_thm_2Eordinal_2EordSUC__ZERO,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (~~ (ap(c_2Eordinal_2EordSUC(A_27a),V0a) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Eordinal_2Eordlt__DISCRETE1,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Eordlt__SUC__DISCRETE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2EordSUC__MONO,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2EordSUC__11,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ((ap(c_2Eordinal_2EordSUC(A_27a),V0a) = ap(c_2Eordinal_2EordSUC(A_27a),V1b)) <=> (V0a = V1b))))))))).
tff(ax_thm_2Eordinal_2Esup__def,axiom,( ! [A_27a:del]: ( ! [V0ordset:$i] : (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))))))).
tff(conj_thm_2Eordinal_2Eord__induction,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => (( ! [V1min:$i] : (mem(V1min,ty_2Eordinal_2Eordinal(A_27a)) => (( ! [V2b:$i] : (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:$i] : (mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(V0P,V3a)))))))))).
tff(conj_thm_2Eordinal_2Esup__thm,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1a),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> (? [V2b:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2Esuple__thm,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1s:$i] : (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))))))))))).
tff(conj_thm_2Eordinal_2Esup__eq__sup,lemma,(( ! [A_27a:del]: ( ! [V0s1:$i] : (mem(V0s1,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1s2:$i] : (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:$i] : (mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V2a),V0s1)) => (? [V3b:$i] : (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:$i] : (mem(V4b,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V4b),V1s2)) => (? [V5a:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2EUnum__cle__Uinf,lemma,(( ! [A_27a:del]: 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))))))).
tff(conj_thm_2Eordinal_2Ecsup__thm,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => (p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),V0s)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> (? [V2d:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2Epredimage__sup__thm,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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:$i] : (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)))))))))))))))).
tff(conj_thm_2Eordinal_2Epredimage__suplt__ELIM,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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:$i] : (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))))))))))))))))).
tff(conj_thm_2Eordinal_2Esuppred__suplt__ELIM,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2Esup__EMPTY,lemma,(( ! [A_27a:del]: (ap(c_2Eordinal_2Esup(A_27a),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a))) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Eordinal_2Esup__SING,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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)))))).
tff(conj_thm_2Eordinal_2Esup__preds__SUC,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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)))))).
tff(conj_thm_2Eordinal_2Epreds__ordSUC,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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)))))))).
tff(conj_thm_2Eordinal_2EcountableOrds__dclosed,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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))))))))))).
tff(ax_thm_2Eordinal_2Eomax__def,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : (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))))))).
tff(conj_thm_2Eordinal_2Eomax__SOME,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1a:$i] : (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:$i] : (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))))))))))))))).
tff(conj_thm_2Eordinal_2Eomax__NONE,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Eordinal_2Eordinal(A_27a)),V1a),V0s)) => (? [V2b:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2Eomax__EMPTY,lemma,(( ! [A_27a:del]: (ap(c_2Eordinal_2Eomax(A_27a),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)))))).
tff(conj_thm_2Eordinal_2Epreds__0,lemma,(( ! [A_27a:del]: (ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)))))).
tff(conj_thm_2Eordinal_2Eordleq0,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ((~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0x))) <=> (V0x = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Eordinal_2Epreds__EQ__EMPTY,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Eordinal_2Eomax__sup,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1a:$i] : (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))))))))).
tff(conj_thm_2Eordinal_2Epreds__omax__SOME__SUC,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Esimple__ord__induction,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ((p(ap(V0P,ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & (( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(V0P,V1a)) => p(ap(V0P,ap(c_2Eordinal_2EordSUC(A_27a),V1a)))))) & ( ! [V2a:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V2a)) & ( ! [V3b:$i] : (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:$i] : (mem(V4a,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(V0P,V4a)))))))))).
tff(conj_thm_2Eordinal_2Esup__preds__omax__NONE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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))))))).
tff(ax_thm_2Eordinal_2Edclose__def,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : (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))))))).
tff(conj_thm_2Eordinal_2Epreds__sup,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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)))))))).
tff(conj_thm_2Eordinal_2Ecsup__lesup,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => (p(ap(c_2Epred__set_2Ecountable(ty_2Eordinal_2Eordinal(A_27a)),V0s)) => ( ! [V1d:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Ecsup__suple,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1b:$i] : (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:$i] : (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))))))))))))))).
tff(conj_thm_2Eordinal_2Epreds__sup__thm,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> (? [V2d:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2Epreds__lesup,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Epreds__suple,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1b:$i] : (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:$i] : (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))))))))))))))).
tff(conj_thm_2Eordinal_2EfromNat__11,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ((ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0x)) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1y))) <=> (V0x = V1y))))))).
tff(conj_thm_2Eordinal_2Eordlt__fromNat,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:$i] : (mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1x),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n)))) <=> (? [V2m:tp__ty_2Enum_2Enum] : ((V1x = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V2m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V0n)))))))))))).
tff(conj_thm_2Eordinal_2EfromNat__ordlt,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n))),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))))))))).
tff(ax_thm_2Eordinal_2Eomega__def,axiom,( ! [A_27a:del]: (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)))))).
tff(conj_thm_2Eordinal_2Elt__omega,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),c_2Eordinal_2Eomega(A_27a))) <=> (? [V1m:tp__ty_2Enum_2Enum] : (V0a = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1m)))))))))).
tff(conj_thm_2Eordinal_2EfromNat__lt__omega,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n))),c_2Eordinal_2Eomega(A_27a))))))).
tff(conj_thm_2Eordinal_2EfromNat__eq__omega,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (~~ (ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n)) = c_2Eordinal_2Eomega(A_27a))))))).
tff(conj_thm_2Eordinal_2Eord__RECURSION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0z:$i] : (mem(V0z,A_27b) => ( ! [V1sf:$i] : (mem(V1sf,arr(ty_2Eordinal_2Eordinal(A_27a),arr(A_27b,A_27b))) => ( ! [V2lf:$i] : (mem(V2lf,arr(ty_2Eordinal_2Eordinal(A_27a),arr(arr(A_27b,bool),A_27b))) => (? [V3h:$i] : (mem(V3h,arr(ty_2Eordinal_2Eordinal(A_27a),A_27b)) & ((ap(V3h,ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0z) & (( ! [V4a:$i] : (mem(V4a,ty_2Eordinal_2Eordinal(A_27a)) => (ap(V3h,ap(c_2Eordinal_2EordSUC(A_27a),V4a)) = ap(ap(V1sf,V4a),ap(V3h,V4a))))) & ( ! [V5a:$i] : (mem(V5a,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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))))))))))))))))))))).
tff(ax_thm_2Eordinal_2EordADD__def,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ((ap(ap(c_2Eordinal_2EordADD(A_27a),V0b),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0b) & (( ! [V1a:$i] : (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:$i] : (mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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))))))))))))).
tff(conj_thm_2Eordinal_2EordADD__0L,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (ap(ap(c_2Eordinal_2EordADD(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0a) = V0a)))))).
tff(conj_thm_2Eordinal_2Eubsup__thm,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => (( ! [V2a:$i] : (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:$i] : (mem(V3c,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V3c),ap(c_2Eordinal_2Esup(A_27a),V0s))) <=> (? [V4d:$i] : (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)))))))))))))))).
tff(conj_thm_2Eordinal_2EordADD__fromNat,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eordinal_2EordADD(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n))),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1m))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Eordinal_2Eomax__preds__omega,lemma,(( ! [A_27a:del]: (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)))))).
tff(conj_thm_2Eordinal_2Eomega__islimit,lemma,(( ! [A_27a:del]: (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)))))).
tff(conj_thm_2Eordinal_2EordADD__fromNat__omega,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eordinal_2EordADD(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n))),c_2Eordinal_2Eomega(A_27a)) = c_2Eordinal_2Eomega(A_27a)))))).
tff(conj_thm_2Eordinal_2Elt__suppreds,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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:$i] : (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))))))))))))).
tff(conj_thm_2Eordinal_2Eomax__preds__SUC,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (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))))))).
tff(conj_thm_2Eordinal_2EORD__ONE,lemma,(( ! [A_27a:del]: (ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Eordinal_2EordSUC__NUMERAL,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (ap(c_2Eordinal_2EordSUC(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V0n)))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Eordinal_2EordZERO__ltSUC,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Eordinal_2EordSUC(A_27a),V0x)))))))).
tff(conj_thm_2Eordinal_2Eordlt__CANCEL__ADDR,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0b)))))))))).
tff(conj_thm_2Eordinal_2Eordlt__CANCEL__ADDL,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (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)))))))).
tff(conj_thm_2Eordinal_2EordADD__CANCEL1,lemma,(( ! [A_27a:del]: (( ! [V0c:$i] : (mem(V0c,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ((V1a = ap(ap(c_2Eordinal_2EordADD(A_27a),V1a),V0c)) <=> (V0c = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))) & ( ! [V2c:$i] : (mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V3a:$i] : (mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ((ap(ap(c_2Eordinal_2EordADD(A_27a),V3a),V2c) = V3a) <=> (V2c = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
tff(conj_thm_2Eordinal_2EordADD__MONO,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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))))))))))))).
tff(conj_thm_2Eordinal_2Eordlt__CANCEL,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2EordADD__RIGHT__CANCEL,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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))))))))))).
tff(conj_thm_2Eordinal_2EleqLEFT__CANCEL,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Eordlt__EXISTS__ADD,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V0a),V1b)) <=> (? [V2c:$i] : (mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) & ((~~ (V2c = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & (V1b = ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V2c))))))))))))).
tff(conj_thm_2Eordinal_2Eordle__EXISTS__ADD,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ((~~ p(ap(ap(c_2Eordinal_2Eordlt(A_27a),V1b),V0a))) <=> (? [V2c:$i] : (mem(V2c,ty_2Eordinal_2Eordinal(A_27a)) & (V1b = ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V2c)))))))))))).
tff(conj_thm_2Eordinal_2Eordle__CANCEL__ADDR,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Edclose__BIGUNION,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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)))))))).
tff(conj_thm_2Eordinal_2EcountableOrds__uncountable,lemma,(( ! [A_27a:del]: (~~ 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)))))))).
tff(conj_thm_2Eordinal_2Edclose__cardleq__univinf,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Esup__lt__implies,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Esup__eq__max,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ((( ! [V2b:$i] : (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))))))))).
tff(conj_thm_2Eordinal_2Esup__eq__SUC,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Eordinal_2Eordinal(A_27a),bool)) => ( ! [V1a:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2Egeneric__continuity,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ((( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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:$i] : (mem(V2x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V3y:$i] : (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:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2Eord__CASES,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ((V0a = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) | ((? [V1a0:$i] : (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),inj__ty_2Enum_2Enum(fo__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))))))))))).
tff(conj_thm_2Eordinal_2Eislimit__0,lemma,(( ! [A_27a:del]: (ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a)))))).
tff(conj_thm_2Eordinal_2Eordinal__IVT,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Eordinal_2Eordinal(A_27a),ty_2Eordinal_2Eordinal(A_27a))) => ( ! [V1a1:$i] : (mem(V1a1,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2a2:$i] : (mem(V2a2,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V3c:$i] : (mem(V3c,ty_2Eordinal_2Eordinal(A_27a)) => ((( ! [V4a:$i] : (mem(V4a,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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:$i] : (mem(V5x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V6y:$i] : (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:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Eordinal_2EordADD__continuous,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1s:$i] : (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))))))))))).
tff(conj_thm_2Eordinal_2EordADD__ASSOC,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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))))))))))).
tff(conj_thm_2Eordinal_2EADD1R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = ap(c_2Eordinal_2EordSUC(A_27a),V0a))))))).
tff(conj_thm_2Eordinal_2EordADD__weak__MONO,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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)))))))))))))).
tff(ax_thm_2Eordinal_2EordMULT__def,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ((ap(ap(c_2Eordinal_2EordMULT(A_27a),V0b),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) & (( ! [V1a:$i] : (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:$i] : (mem(V2a,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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))))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__0L,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0a) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Eordinal_2EordMULT__0R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Eordinal_2EordMULT__1L,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V0a) = V0a)))))).
tff(conj_thm_2Eordinal_2EordMULT__1R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0a)))))).
tff(conj_thm_2Eordinal_2EordMULT__2R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = ap(ap(c_2Eordinal_2EordADD(A_27a),V0a),V0a))))))).
tff(conj_thm_2Eordinal_2Eislimit__SUC__lt,lemma,(( ! [A_27a:del]: ( ! [V0b:$i] : (mem(V0b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (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)))))))))).
tff(conj_thm_2Eordinal_2EordMULT__lt__MONO__R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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),inj__ty_2Enum_2Enum(fo__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))))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__le__MONO__R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__lt__MONO__R__EQN,lemma,(( ! [A_27a:del]: ( ! [V0c:$i] : (mem(V0c,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0c))))))))))))).
tff(conj_thm_2Eordinal_2EordADD__le__MONO__L,lemma,(( ! [A_27a:del]: ( ! [V0y:$i] : (mem(V0y,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1x:$i] : (mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2z:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__le__MONO__L,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__CANCEL__R,lemma,(( ! [A_27a:del]: ( ! [V0z:$i] : (mem(V0z,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1x:$i] : (mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2y:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) | (V1x = V2y)))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__continuous,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1s:$i] : (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))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__fromNat,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n))),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1m))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Eordinal_2Eomega__MUL__fromNat,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (ap(ap(c_2Eordinal_2EordMULT(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0n))),c_2Eordinal_2Eomega(A_27a)) = c_2Eordinal_2Eomega(A_27a))))))).
tff(conj_thm_2Eordinal_2EordMULT__LDISTRIB,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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)))))))))))).
tff(conj_thm_2Eordinal_2EordMULT__ASSOC,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2c:$i] : (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))))))))))).
tff(ax_thm_2Eordinal_2EordDIVISION,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => (p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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)))))))))).
tff(conj_thm_2Eordinal_2EordDIV__UNIQUE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2q:$i] : (mem(V2q,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V3r:$i] : (mem(V3r,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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))))))))))))).
tff(conj_thm_2Eordinal_2EordMOD__UNIQUE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1b:$i] : (mem(V1b,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2q:$i] : (mem(V2q,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V3r:$i] : (mem(V3r,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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))))))))))))).
tff(ax_thm_2Eordinal_2EordEXP__def,axiom,( ! [A_27a:del]: (( ! [V0a:$i] : (mem(V0a,ty_2Eordinal_2Eordinal(A_27a)) => (ap(ap(c_2Eordinal_2EordEXP(A_27a),V0a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2a_27:$i] : (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:$i] : (mem(V3a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V4a_27:$i] : (mem(V4a_27,ty_2Eordinal_2Eordinal(A_27a)) => ((p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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))))))))))))).
tff(conj_thm_2Eordinal_2EordEXP__1R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0a)))))).
tff(conj_thm_2Eordinal_2EordEXP__1L,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V0a) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Eordinal_2EordEXP__2R,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = ap(ap(c_2Eordinal_2EordMULT(A_27a),V0a),V0a))))))).
tff(conj_thm_2Eordinal_2EordEXP__fromNat,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eordinal_2EordEXP(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0x))),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V1n))) = ap(c_2Eordinal_2EfromNat(A_27a),ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Eordinal_2EordEXP__le__MONO__L,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1a:$i] : (mem(V1a,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V2b:$i] : (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)))))))))))))).
tff(conj_thm_2Eordinal_2EIFF__ZERO__lt,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Eordinal_2Eordinal(A_27a)) => (((~~ (V0x = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__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,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) <=> p(ap(ap(c_2Eordinal_2Eordlt(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0x))))))))).
tff(conj_thm_2Eordinal_2Eislimit__SUC,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (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)))))).
tff(conj_thm_2Eordinal_2Eislimit__fromNat,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ((ap(c_2Eordinal_2Eomax(A_27a),ap(c_2Eordinal_2Epreds(A_27a),ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(V0x)))) = c_2Eoption_2ENONE(ty_2Eordinal_2Eordinal(A_27a))) <=> (V0x = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Eordinal_2EordEXP__ZERO__limit,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0x) = ap(c_2Eordinal_2EfromNat(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Eordinal_2EordEXP__ZERO__nonlimit,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0x) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Eordinal_2Esup__EQ__0,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (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),inj__ty_2Enum_2Enum(fo__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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),c_2Epred__set_2EEMPTY(ty_2Eordinal_2Eordinal(A_27a)))))))))))).
tff(conj_thm_2Eordinal_2EordADD__EQ__0,lemma,(( ! [A_27a:del]: ( ! [V0y:$i] : (mem(V0y,ty_2Eordinal_2Eordinal(A_27a)) => ( ! [V1x:$i] : (mem(V1x,ty_2Eordinal_2Eordinal(A_27a)) => ((ap(ap(c_2Eordinal_2EordADD(A_27a),V1x),V0y) = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> ((V1x = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) & (V0y = ap(c_2Eordinal_2EfromNat(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))).
tff(conj_thm_2Eordinal_2EIMAGE__EQ__SING,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,A_27a)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2x:$i] : (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:$i] : (mem(V3y,A_27b) & p(ap(ap(c_2Ebool_2EIN(A_27b),V3y),V1s)))) & ( ! [V4y:$i] : (mem(V4y,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V4y),V1s)) => (ap(V0f,V4y) = V2x)))))))))))))))).
