include('Axioms/integer^2.ax').
thf(tp_ty_2Eordinal_2Eordinal,type,( ty_2Eordinal_2Eordinal: del >del )).
thf(tp_c_2Eordinal_2EallOrds,type,(c_2Eordinal_2EallOrds:(del>$i))).
thf(mem_c_2Eordinal_2EallOrds,axiom,( ! [A_27a:del] : (mem@(c_2Eordinal_2EallOrds@A_27a)@(ty_2Ewellorder_2Ewellorder@(ty_2Eordinal_2Eordinal@A_27a))))).
thf(tp_c_2Eordinal_2Edclose,type,(c_2Eordinal_2Edclose:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Edownward__closed,type,(c_2Eordinal_2Edownward__closed:(del>$i))).
thf(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)))).
thf(tp_c_2Eordinal_2Eepsilon0,type,(c_2Eordinal_2Eepsilon0:(del>$i))).
thf(mem_c_2Eordinal_2Eepsilon0,axiom,( ! [A_27a:del] : (mem@(c_2Eordinal_2Eepsilon0@A_27a)@(ty_2Eordinal_2Eordinal@A_27a)))).
thf(tp_c_2Eordinal_2Eeval__poly,type,(c_2Eordinal_2Eeval__poly:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2EfromNat,type,(c_2Eordinal_2EfromNat:(del>$i))).
thf(mem_c_2Eordinal_2EfromNat,axiom,( ! [A_27a:del] : (mem@(c_2Eordinal_2EfromNat@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Eordinal_2Eordinal@A_27a))))).
thf(tp_c_2Eordinal_2Eis__polyform,type,(c_2Eordinal_2Eis__polyform:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Eordinal_2Eoleast,type,(c_2Eordinal_2Eoleast:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Eomax,type,(c_2Eordinal_2Eomax:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2Eomega,type,(c_2Eordinal_2Eomega:(del>$i))).
thf(mem_c_2Eordinal_2Eomega,axiom,( ! [A_27a:del] : (mem@(c_2Eordinal_2Eomega@A_27a)@(ty_2Eordinal_2Eordinal@A_27a)))).
thf(tp_c_2Eordinal_2EordADD,type,(c_2Eordinal_2EordADD:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2EordDIV,type,(c_2Eordinal_2EordDIV:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2EordEXP,type,(c_2Eordinal_2EordEXP:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2EordMOD,type,(c_2Eordinal_2EordMOD:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2EordMULT,type,(c_2Eordinal_2EordMULT:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2EordSUC,type,(c_2Eordinal_2EordSUC:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Eordinal__ABS,type,(c_2Eordinal_2Eordinal__ABS:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Eordinal__ABS__CLASS,type,(c_2Eordinal_2Eordinal__ABS__CLASS:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Eordinal__REP,type,(c_2Eordinal_2Eordinal__REP:(del>$i))).
thf(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)))))).
thf(tp_c_2Eordinal_2Eordinal__REP__CLASS,type,(c_2Eordinal_2Eordinal__REP__CLASS:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Eordlt,type,(c_2Eordinal_2Eordlt:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Epolyform,type,(c_2Eordinal_2Epolyform:(del>$i))).
thf(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)))))))).
thf(tp_c_2Eordinal_2Epreds,type,(c_2Eordinal_2Epreds:(del>$i))).
thf(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))))).
thf(tp_c_2Eordinal_2Esup,type,(c_2Eordinal_2Esup:(del>$i))).
thf(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))))).
thf(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))@(lam@(arr@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool)@(^ [V1c:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)))@(lam@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(^ [V2r:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ewellorder_2Eorderiso@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@V2r)@V2r))@(ap@(ap@(c_2Emin_2E_3D@(arr@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool))@V1c)@(ap@(c_2Ewellorder_2Eorderiso@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@V2r)))))))))@V0rep)))))).
thf(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@(lam@(arr@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool)@(^ [V2c:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)))@(lam@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(^ [V3r:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ewellorder_2Eorderiso@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@V3r)@V3r))@(ap@(ap@(c_2Emin_2E_3D@(arr@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool))@V2c)@(ap@(c_2Ewellorder_2Eorderiso@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@V3r))))))))@V1r)) <=> ((ap@(c_2Eordinal_2Eordinal__REP__CLASS@A_27a)@(ap@(c_2Eordinal_2Eordinal__ABS__CLASS@A_27a)@V1r)) = V1r))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))).
thf(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)))))))))).
thf(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))))))).
thf(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))))))))))).
thf(conj_thm_2Eordinal_2Eordlt__WF,lemma,( ! [A_27a:del]: (p@(ap@(c_2Erelation_2EWF@(ty_2Eordinal_2Eordinal@A_27a))@(c_2Eordinal_2Eordlt@A_27a))))).
thf(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)))))))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V0x:$i] : (lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@bool)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@V0x)@V1y))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eordinal_2Eordinal@A_27a))@V0x)@V1y))@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V0x)@V1y))))))))))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V0x:$i] : (lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@bool)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@V0x)@V1y))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eordinal_2Eordinal@A_27a))@V0x)@V1y))@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V0x)@V1y))))))))))))).
thf(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))))))))).
thf(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))))).
thf(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)))))))))))))).
thf(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))))))))))).
thf(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)))))))))))))).
thf(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)))))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1w0:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@bool)@V1w0)@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V1w0)@V0w)))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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)))))))).
thf(stp_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone,type,(tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Eone_2Eone : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(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)))).
thf(stp_c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone,type,(tp__c_ty_2Eordinal_2Eordinal_ty_2Eone_2Eone : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(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)))))).
thf(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))))))).
thf(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)))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V1x))@(ap@(c_2Ebool_2E_21@(ty_2Eordinal_2Eordinal@A_27a))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V2y:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V2y)@V1x))@(ap@c_2Ebool_2E_7E@(ap@V0P@V2y))))))))))))))).
thf(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)))))))))).
thf(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)@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1b:$i] : (ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V0a)@V1b))))))))).
thf(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)@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V0a:$i] : 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)))))))).
thf(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)@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V0a:$i] : 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))))))))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1a:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@(ty_2Eordinal_2Eordinal@A_27a))@V1a)@(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))@V0ordset)))))))))))).
thf(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))))))))).
thf(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))))))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))).
thf(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))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))))))).
thf(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))))).
thf(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))))).
thf(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))))).
thf(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))))))).
thf(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)))))))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1a:$i] : (ap@(ap@(c_2Emin_2E_3D@(arr@(ty_2Eordinal_2Eordinal@A_27a)@bool))@(ap@(ap@(c_2Eset__relation_2Emaximal__elements@(ty_2Eordinal_2Eordinal@A_27a))@V0s)@(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V2x:$i] : (lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V3y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@bool)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@V2x)@V3y))@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V3y)@V2x)))))))))))@(ap@(ap@(c_2Epred__set_2EINSERT@(ty_2Eordinal_2Eordinal@A_27a))@V1a)@(c_2Epred__set_2EEMPTY@(ty_2Eordinal_2Eordinal@A_27a)))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))).
thf(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))))).
thf(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))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V1x:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@bool)@V1x)@(ap@(c_2Ebool_2E_3F@(ty_2Eordinal_2Eordinal@A_27a))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V2y:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@(ty_2Eordinal_2Eordinal@A_27a))@V2y)@V0s))@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V1x)@V2y)))))))))))))).
thf(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))))))).
thf(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))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))).
thf(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))))))))))).
thf(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)))))))))))))).
thf(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)))))).
thf(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))))))))))).
thf(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)))))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V0i:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@bool)@(ap@(c_2Eordinal_2EfromNat@A_27a)@V0i))@c_2Ebool_2ET)))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))))))))))))))))).
thf(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))))))))))))).
thf(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))))).
thf(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))))))))))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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))))).
thf(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)))))))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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))))))).
thf(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))@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V0a:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Eordinal_2Eordinal@A_27a)@bool)@V0a)@(ap@(c_2Epred__set_2Ecountable@(ty_2Eordinal_2Eordinal@A_27a))@(ap@(c_2Eordinal_2Epreds@A_27a)@V0a))))))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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))))).
thf(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)))))))))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))).
thf(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))))).
thf(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)))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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)))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))))).
thf(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))))))))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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)))))))))).
thf(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)))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(conj_thm_2Eordinal_2EIMAGE__EQ__SING,lemma,( ! [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))))))))))))))).
thf(conj_thm_2Eordinal_2EordMULT__EQ__0,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1y:$i] : ((mem@V1y@(ty_2Eordinal_2Eordinal@A_27a)) => (((ap@(ap@(c_2Eordinal_2EordMULT@A_27a)@V0x)@V1y) = (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))) | (V1y = (ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))).
thf(conj_thm_2Eordinal_2EordEXP__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_2EordEXP@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))) & (~~ ((ap@(c_2Eordinal_2Eomax@A_27a)@(ap@(c_2Eordinal_2Epreds@A_27a)@V0y)) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a)))))))))))).
thf(conj_thm_2Eordinal_2EZERO__lt__ordEXP__I,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(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)))@V0a)) => (p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@(ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Eordinal_2EordEXP@A_27a)@V0a)@V1x)))))))))).
thf(conj_thm_2Eordinal_2EZERO__lt__ordEXP,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(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@(ap@(c_2Eordinal_2EordEXP@A_27a)@V0a)@V1x))) <=> ((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)@V1x)) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a))))))))))).
thf(conj_thm_2Eordinal_2EordEXP__lt__MONO__R,lemma,( ! [A_27a:del]: ( ! [V0y:$i] : ((mem@V0y@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V2a:$i] : ((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@(inj__ty_2Enum_2Enum @ fo__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)))))))))))).
thf(conj_thm_2Eordinal_2EordEXP__lt__IFF,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1y:$i] : ((mem@V1y@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V2a:$i] : ((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@(inj__ty_2Enum_2Enum @ fo__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)))))))))))).
thf(conj_thm_2Eordinal_2EordEXP__le__MONO__R,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1y:$i] : ((mem@V1y@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [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)) & (~~ (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))))))))))))).
thf(conj_thm_2Eordinal_2EordEXP__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_2Eordinal_2Eordlt@A_27a)@(ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ fo__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)))))))))).
thf(conj_thm_2Eordinal_2EordEXP__ADD,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)@(ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ fo__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)))))))))))).
thf(conj_thm_2Eordinal_2EordEXP__MUL,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)@(ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ fo__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))))))))))).
thf(conj_thm_2Eordinal_2Efixpoints__exist,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))) => ((( ! [V1s:$i] : ((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:$i] : ((mem@V2x@(ty_2Eordinal_2Eordinal@A_27a)) => (~~ (p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@(ap@V0f@V2x))@V2x)))))) => ( ! [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))) & ((ap@V0f@V4b) = V4b))))))))))).
thf(conj_thm_2Eordinal_2Ex__le__ordEXP__x,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(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@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V0a)) => (~~ (p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@(ap@(ap@(c_2Eordinal_2EordEXP@A_27a)@V0a)@V1x))@V1x)))))))))).
thf(ax_thm_2Eordinal_2Eepsilon0__def,axiom,( ! [A_27a:del]: ((c_2Eordinal_2Eepsilon0@A_27a) = (ap@(c_2Eordinal_2Eoleast@A_27a)@(lam@(ty_2Eordinal_2Eordinal@A_27a)@(^ [V0x:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eordinal_2Eordinal@A_27a))@(ap@(ap@(c_2Eordinal_2EordEXP@A_27a)@(c_2Eordinal_2Eomega@A_27a))@V0x))@V0x))))))).
thf(conj_thm_2Eordinal_2Eepsilon0__fixpoint,lemma,( ! [A_27a:del]: ((ap@(ap@(c_2Eordinal_2EordEXP@A_27a)@(c_2Eordinal_2Eomega@A_27a))@(c_2Eordinal_2Eepsilon0@A_27a)) = (c_2Eordinal_2Eepsilon0@A_27a)))).
thf(conj_thm_2Eordinal_2Eepsilon0__least__fixpoint,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Eordinal_2Eordinal@A_27a)) => ((p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V0a)@(c_2Eordinal_2Eepsilon0@A_27a))) => ((p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V0a)@(ap@(ap@(c_2Eordinal_2EordEXP@A_27a)@(c_2Eordinal_2Eomega@A_27a))@V0a))) & (p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@(ap@(ap@(c_2Eordinal_2EordEXP@A_27a)@(c_2Eordinal_2Eomega@A_27a))@V0a))@(c_2Eordinal_2Eepsilon0@A_27a))))))))).
thf(conj_thm_2Eordinal_2Eomega__lt__epsilon0,lemma,( ! [A_27a:del]: (p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@(c_2Eordinal_2Eomega@A_27a))@(c_2Eordinal_2Eepsilon0@A_27a))))).
thf(conj_thm_2Eordinal_2EfromNat__lt__epsilon0,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_2Eepsilon0@A_27a)))))).
thf(conj_thm_2Eordinal_2Eadd__nat__islimit,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1a:$i] : ((mem@V1a@(ty_2Eordinal_2Eordinal@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) => (((ap@(c_2Eordinal_2Eomax@A_27a)@(ap@(c_2Eordinal_2Epreds@A_27a)@(ap@(ap@(c_2Eordinal_2EordADD@A_27a)@V1a)@(ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ V0n))))) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a))) <=> $false))))))).
thf(conj_thm_2Eordinal_2Estrict__continuity__preserves__islimit,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)) => ((( ! [V2s:$i] : ((mem@V2s@(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))@V2s)@(c_2Epred__set_2EUNIV@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)))) & (~~ (V2s = (c_2Epred__set_2EEMPTY@(ty_2Eordinal_2Eordinal@A_27a))))) => ((ap@V0f@(ap@(c_2Eordinal_2Esup@A_27a)@V2s)) = (ap@(c_2Eordinal_2Esup@A_27a)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eordinal_2Eordinal@A_27a)@(ty_2Eordinal_2Eordinal@A_27a))@V0f)@V2s)))))) & (( ! [V3x:$i] : ((mem@V3x@(ty_2Eordinal_2Eordinal@A_27a)) => ( ! [V4y:$i] : ((mem@V4y@(ty_2Eordinal_2Eordinal@A_27a)) => ((p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@V3x)@V4y)) => (p@(ap@(ap@(c_2Eordinal_2Eordlt@A_27a)@(ap@V0f@V3x))@(ap@V0f@V4y)))))))) & (((ap@(c_2Eordinal_2Eomax@A_27a)@(ap@(c_2Eordinal_2Epreds@A_27a)@V1a)) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a))) & (~~ (V1a = (ap@(c_2Eordinal_2EfromNat@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))) => ((ap@(c_2Eordinal_2Eomax@A_27a)@(ap@(c_2Eordinal_2Epreds@A_27a)@(ap@V0f@V1a))) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a)))))))))).
thf(conj_thm_2Eordinal_2Eadd__omega__islimit,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)@(ap@(ap@(c_2Eordinal_2EordADD@A_27a)@V0a)@(c_2Eordinal_2Eomega@A_27a)))) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a))))))).
thf(conj_thm_2Eordinal_2Eislimit__mul__R,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)@V1a)) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a))) => ((ap@(c_2Eordinal_2Eomax@A_27a)@(ap@(c_2Eordinal_2Epreds@A_27a)@(ap@(ap@(c_2Eordinal_2EordMULT@A_27a)@V0b)@V1a))) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a)))))))))).
thf(conj_thm_2Eordinal_2Emul__omega__islimit,conjecture,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Eordinal_2Eordinal@A_27a)) => ((ap@(c_2Eordinal_2Eomax@A_27a)@(ap@(c_2Eordinal_2Epreds@A_27a)@(ap@(ap@(c_2Eordinal_2EordMULT@A_27a)@(c_2Eordinal_2Eomega@A_27a))@V0a))) = (c_2Eoption_2ENONE@(ty_2Eordinal_2Eordinal@A_27a))))))).
