include('Axioms/intExtension_2.ax').
tff(tp_ty_2EordinalNotation_2Eosyntax,type,( ty_2EordinalNotation_2Eosyntax: del )).
tff(stp_ty_2EordinalNotation_2Eosyntax,type,(tp__ty_2EordinalNotation_2Eosyntax : $tType)).
tff(stp_inj_ty_2EordinalNotation_2Eosyntax,type,(inj__ty_2EordinalNotation_2Eosyntax : tp__ty_2EordinalNotation_2Eosyntax > $i)).
tff(stp_surj_ty_2EordinalNotation_2Eosyntax,type,(surj__ty_2EordinalNotation_2Eosyntax : $i > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_inj_surj_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(inj__ty_2EordinalNotation_2Eosyntax(X)) = X))).
tff(stp_inj_mem_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__ty_2EordinalNotation_2Eosyntax] : (mem(inj__ty_2EordinalNotation_2Eosyntax(X),ty_2EordinalNotation_2Eosyntax)))).
tff(stp_iso_mem_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:$i] : (mem(X,ty_2EordinalNotation_2Eosyntax) => (X = inj__ty_2EordinalNotation_2Eosyntax(surj__ty_2EordinalNotation_2Eosyntax(X)))))).
tff(tp_c_2EordinalNotation_2EEnd,type,(c_2EordinalNotation_2EEnd:$i)).
tff(mem_c_2EordinalNotation_2EEnd,axiom,mem(c_2EordinalNotation_2EEnd,arr(ty_2Enum_2Enum,ty_2EordinalNotation_2Eosyntax))).
tff(stp_fo_c_2EordinalNotation_2EEnd,type,(fo__c_2EordinalNotation_2EEnd:(tp__ty_2Enum_2Enum) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2EEnd,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2EEnd(X0)) = ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2EordinalNotation_2EPlus,type,(c_2EordinalNotation_2EPlus:$i)).
tff(mem_c_2EordinalNotation_2EPlus,axiom,mem(c_2EordinalNotation_2EPlus,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax))))).
tff(stp_fo_c_2EordinalNotation_2EPlus,type,(fo__c_2EordinalNotation_2EPlus:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2Enum_2Enum * tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2EPlus,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2EPlus(X0,X1,X2)) = ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2EordinalNotation_2Eosyntax(X2))))))).
tff(tp_c_2EordinalNotation_2Ecf1,type,(c_2EordinalNotation_2Ecf1:$i)).
tff(mem_c_2EordinalNotation_2Ecf1,axiom,mem(c_2EordinalNotation_2Ecf1,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,ty_2Enum_2Enum)))).
tff(stp_fo_c_2EordinalNotation_2Ecf1,type,(fo__c_2EordinalNotation_2Ecf1:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2EordinalNotation_2Ecf1,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2Enum_2Enum(fo__c_2EordinalNotation_2Ecf1(X0,X1)) = ap(ap(c_2EordinalNotation_2Ecf1,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)))))).
tff(tp_c_2EordinalNotation_2Ecf2,type,(c_2EordinalNotation_2Ecf2:$i)).
tff(mem_c_2EordinalNotation_2Ecf2,axiom,mem(c_2EordinalNotation_2Ecf2,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(stp_fo_c_2EordinalNotation_2Ecf2,type,(fo__c_2EordinalNotation_2Ecf2:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2EordinalNotation_2Ecf2,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2EordinalNotation_2Ecf2(X0,X1,X2)) = ap(ap(ap(c_2EordinalNotation_2Ecf2,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2EordinalNotation_2Ecoeff,type,(c_2EordinalNotation_2Ecoeff:$i)).
tff(mem_c_2EordinalNotation_2Ecoeff,axiom,mem(c_2EordinalNotation_2Ecoeff,arr(ty_2EordinalNotation_2Eosyntax,ty_2Enum_2Enum))).
tff(stp_fo_c_2EordinalNotation_2Ecoeff,type,(fo__c_2EordinalNotation_2Ecoeff:(tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2EordinalNotation_2Ecoeff,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2Enum_2Enum(fo__c_2EordinalNotation_2Ecoeff(X0)) = ap(c_2EordinalNotation_2Ecoeff,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(tp_c_2EordinalNotation_2Eexpt,type,(c_2EordinalNotation_2Eexpt:$i)).
tff(mem_c_2EordinalNotation_2Eexpt,axiom,mem(c_2EordinalNotation_2Eexpt,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax))).
tff(stp_fo_c_2EordinalNotation_2Eexpt,type,(fo__c_2EordinalNotation_2Eexpt:(tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Eexpt,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Eexpt(X0)) = ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(tp_c_2EordinalNotation_2Efinp,type,(c_2EordinalNotation_2Efinp:$i)).
tff(mem_c_2EordinalNotation_2Efinp,axiom,mem(c_2EordinalNotation_2Efinp,arr(ty_2EordinalNotation_2Eosyntax,bool))).
tff(stp_fo_c_2EordinalNotation_2Efinp,type,(fo__c_2EordinalNotation_2Efinp:(tp__ty_2EordinalNotation_2Eosyntax) > tp__o)).
tff(stp_eq_fo_c_2EordinalNotation_2Efinp,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__o(fo__c_2EordinalNotation_2Efinp(X0)) = ap(c_2EordinalNotation_2Efinp,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(tp_c_2EordinalNotation_2Eis__ord,type,(c_2EordinalNotation_2Eis__ord:$i)).
tff(mem_c_2EordinalNotation_2Eis__ord,axiom,mem(c_2EordinalNotation_2Eis__ord,arr(ty_2EordinalNotation_2Eosyntax,bool))).
tff(stp_fo_c_2EordinalNotation_2Eis__ord,type,(fo__c_2EordinalNotation_2Eis__ord:(tp__ty_2EordinalNotation_2Eosyntax) > tp__o)).
tff(stp_eq_fo_c_2EordinalNotation_2Eis__ord,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__o(fo__c_2EordinalNotation_2Eis__ord(X0)) = ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(tp_c_2EordinalNotation_2Eoless,type,(c_2EordinalNotation_2Eoless:$i)).
tff(mem_c_2EordinalNotation_2Eoless,axiom,mem(c_2EordinalNotation_2Eoless,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool)))).
tff(stp_fo_c_2EordinalNotation_2Eoless,type,(fo__c_2EordinalNotation_2Eoless:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax) > tp__o)).
tff(stp_eq_fo_c_2EordinalNotation_2Eoless,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : (inj__o(fo__c_2EordinalNotation_2Eoless(X0,X1)) = ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)))))).
tff(tp_c_2EordinalNotation_2Eord__add,type,(c_2EordinalNotation_2Eord__add:$i)).
tff(mem_c_2EordinalNotation_2Eord__add,axiom,mem(c_2EordinalNotation_2Eord__add,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax)))).
tff(stp_fo_c_2EordinalNotation_2Eord__add,type,(fo__c_2EordinalNotation_2Eord__add:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Eord__add,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Eord__add(X0,X1)) = ap(ap(c_2EordinalNotation_2Eord__add,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)))))).
tff(tp_c_2EordinalNotation_2Eord__less,type,(c_2EordinalNotation_2Eord__less:$i)).
tff(mem_c_2EordinalNotation_2Eord__less,axiom,mem(c_2EordinalNotation_2Eord__less,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool)))).
tff(stp_fo_c_2EordinalNotation_2Eord__less,type,(fo__c_2EordinalNotation_2Eord__less:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax) > tp__o)).
tff(stp_eq_fo_c_2EordinalNotation_2Eord__less,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : (inj__o(fo__c_2EordinalNotation_2Eord__less(X0,X1)) = ap(ap(c_2EordinalNotation_2Eord__less,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)))))).
tff(tp_c_2EordinalNotation_2Eord__mult,type,(c_2EordinalNotation_2Eord__mult:$i)).
tff(mem_c_2EordinalNotation_2Eord__mult,axiom,mem(c_2EordinalNotation_2Eord__mult,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax)))).
tff(stp_fo_c_2EordinalNotation_2Eord__mult,type,(fo__c_2EordinalNotation_2Eord__mult:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Eord__mult,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Eord__mult(X0,X1)) = ap(ap(c_2EordinalNotation_2Eord__mult,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)))))).
tff(tp_c_2EordinalNotation_2Eord__sub,type,(c_2EordinalNotation_2Eord__sub:$i)).
tff(mem_c_2EordinalNotation_2Eord__sub,axiom,mem(c_2EordinalNotation_2Eord__sub,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax)))).
tff(stp_fo_c_2EordinalNotation_2Eord__sub,type,(fo__c_2EordinalNotation_2Eord__sub:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Eord__sub,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Eord__sub(X0,X1)) = ap(ap(c_2EordinalNotation_2Eord__sub,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)))))).
tff(tp_c_2EordinalNotation_2Eosyntax__CASE,type,(c_2EordinalNotation_2Eosyntax__CASE:del > $i)).
tff(mem_c_2EordinalNotation_2Eosyntax__CASE,axiom,( ! [A_27a:del] : mem(c_2EordinalNotation_2Eosyntax__CASE(A_27a),arr(ty_2EordinalNotation_2Eosyntax,arr(arr(ty_2Enum_2Enum,A_27a),arr(arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,A_27a))),A_27a)))))).
tff(tp_c_2EordinalNotation_2Eosyntax__size,type,(c_2EordinalNotation_2Eosyntax__size:$i)).
tff(mem_c_2EordinalNotation_2Eosyntax__size,axiom,mem(c_2EordinalNotation_2Eosyntax__size,arr(ty_2EordinalNotation_2Eosyntax,ty_2Enum_2Enum))).
tff(stp_fo_c_2EordinalNotation_2Eosyntax__size,type,(fo__c_2EordinalNotation_2Eosyntax__size:(tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2EordinalNotation_2Eosyntax__size,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2Enum_2Enum(fo__c_2EordinalNotation_2Eosyntax__size(X0)) = ap(c_2EordinalNotation_2Eosyntax__size,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(tp_c_2EordinalNotation_2Epadd,type,(c_2EordinalNotation_2Epadd:$i)).
tff(mem_c_2EordinalNotation_2Epadd,axiom,mem(c_2EordinalNotation_2Epadd,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,ty_2EordinalNotation_2Eosyntax))))).
tff(stp_fo_c_2EordinalNotation_2Epadd,type,(fo__c_2EordinalNotation_2Epadd:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2Enum_2Enum) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Epadd,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Epadd(X0,X1,X2)) = ap(ap(ap(c_2EordinalNotation_2Epadd,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2EordinalNotation_2Epmult,type,(c_2EordinalNotation_2Epmult:$i)).
tff(mem_c_2EordinalNotation_2Epmult,axiom,mem(c_2EordinalNotation_2Epmult,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,ty_2EordinalNotation_2Eosyntax))))).
tff(stp_fo_c_2EordinalNotation_2Epmult,type,(fo__c_2EordinalNotation_2Epmult:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2Enum_2Enum) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Epmult,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Epmult(X0,X1,X2)) = ap(ap(ap(c_2EordinalNotation_2Epmult,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2EordinalNotation_2Eosyntax(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2EordinalNotation_2Erank,type,(c_2EordinalNotation_2Erank:$i)).
tff(mem_c_2EordinalNotation_2Erank,axiom,mem(c_2EordinalNotation_2Erank,arr(ty_2EordinalNotation_2Eosyntax,ty_2Enum_2Enum))).
tff(stp_fo_c_2EordinalNotation_2Erank,type,(fo__c_2EordinalNotation_2Erank:(tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2EordinalNotation_2Erank,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2Enum_2Enum(fo__c_2EordinalNotation_2Erank(X0)) = ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(tp_c_2EordinalNotation_2Erestn,type,(c_2EordinalNotation_2Erestn:$i)).
tff(mem_c_2EordinalNotation_2Erestn,axiom,mem(c_2EordinalNotation_2Erestn,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,ty_2EordinalNotation_2Eosyntax)))).
tff(stp_fo_c_2EordinalNotation_2Erestn,type,(fo__c_2EordinalNotation_2Erestn:(tp__ty_2EordinalNotation_2Eosyntax * tp__ty_2Enum_2Enum) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Erestn,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Erestn(X0,X1)) = ap(ap(c_2EordinalNotation_2Erestn,inj__ty_2EordinalNotation_2Eosyntax(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2EordinalNotation_2Etail,type,(c_2EordinalNotation_2Etail:$i)).
tff(mem_c_2EordinalNotation_2Etail,axiom,mem(c_2EordinalNotation_2Etail,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax))).
tff(stp_fo_c_2EordinalNotation_2Etail,type,(fo__c_2EordinalNotation_2Etail:(tp__ty_2EordinalNotation_2Eosyntax) > tp__ty_2EordinalNotation_2Eosyntax)).
tff(stp_eq_fo_c_2EordinalNotation_2Etail,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : (inj__ty_2EordinalNotation_2Eosyntax(fo__c_2EordinalNotation_2Etail(X0)) = ap(c_2EordinalNotation_2Etail,inj__ty_2EordinalNotation_2Eosyntax(X0))))).
tff(stp_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,type,(tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,type,(inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum : tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,type,(surj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum : $i > tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum] : (surj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum(inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum] : (mem(inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum(X),ty_2Eind__type_2Erecspace(ty_2Enum_2Enum))))).
tff(stp_iso_mem_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Eind__type_2Erecspace(ty_2Enum_2Enum)) => (X = inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum(surj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum(X)))))).
tff(ax_thm_2EordinalNotation_2Eosyntax__TY__DEF,axiom,(? [V0rep:$i] : (mem(V0rep,arr(ty_2EordinalNotation_2Eosyntax,ty_2Eind__type_2Erecspace(ty_2Enum_2Enum))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(ty_2Enum_2Enum),ty_2EordinalNotation_2Eosyntax),f2762),V0rep))))).
tff(ax_thm_2EordinalNotation_2Eosyntax__case__def,axiom,( ! [A_27a:del]: (( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V2f1:$i] : (mem(V2f1,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,A_27a)))) => (ap(ap(ap(c_2EordinalNotation_2Eosyntax__CASE(A_27a),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0a))),V1f),V2f1) = ap(V1f,inj__ty_2Enum_2Enum(V0a)))))))) & ( ! [V3a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4a1:tp__ty_2Enum_2Enum] : ( ! [V5a2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V6f:$i] : (mem(V6f,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V7f1:$i] : (mem(V7f1,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,A_27a)))) => (ap(ap(ap(c_2EordinalNotation_2Eosyntax__CASE(A_27a),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V3a0)),inj__ty_2Enum_2Enum(V4a1)),inj__ty_2EordinalNotation_2Eosyntax(V5a2))),V6f),V7f1) = ap(ap(ap(V7f1,inj__ty_2EordinalNotation_2Eosyntax(V3a0)),inj__ty_2Enum_2Enum(V4a1)),inj__ty_2EordinalNotation_2Eosyntax(V5a2))))))))))))).
tff(ax_thm_2EordinalNotation_2Eosyntax__size__def,axiom,(( ! [V0a:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Eosyntax__size,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0a)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0a))))) & ( ! [V1a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2a1:tp__ty_2Enum_2Enum] : ( ! [V3a2:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Eosyntax__size,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1a0)),inj__ty_2Enum_2Enum(V2a1)),inj__ty_2EordinalNotation_2Eosyntax(V3a2)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2B,ap(c_2EordinalNotation_2Eosyntax__size,inj__ty_2EordinalNotation_2Eosyntax(V1a0))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2a1)),ap(c_2EordinalNotation_2Eosyntax__size,inj__ty_2EordinalNotation_2Eosyntax(V3a2)))))))))))).
tff(conj_thm_2EordinalNotation_2Edatatype__osyntax,lemma,(( ! [V0osyntax:$i] : (mem(V0osyntax,arr(arr(ty_2Enum_2Enum,ty_2EordinalNotation_2Eosyntax),arr(arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax))),bool))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(V0osyntax,c_2EordinalNotation_2EEnd),c_2EordinalNotation_2EPlus))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__11,lemma,((( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1a_27:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0a))) = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1a_27)))) <=> (V0a = V1a_27)))) & ( ! [V2a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3a1:tp__ty_2Enum_2Enum] : ( ! [V4a2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5a0_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V6a1_27:tp__ty_2Enum_2Enum] : ( ! [V7a2_27:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2a0)),inj__ty_2Enum_2Enum(V3a1)),inj__ty_2EordinalNotation_2Eosyntax(V4a2))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V5a0_27)),inj__ty_2Enum_2Enum(V6a1_27)),inj__ty_2EordinalNotation_2Eosyntax(V7a2_27)))) <=> ((V2a0 = V5a0_27) & ((V3a1 = V6a1_27) & (V4a2 = V7a2_27))))))))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__distinct,lemma,(( ! [V0a2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1a1:tp__ty_2Enum_2Enum] : ( ! [V2a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3a:tp__ty_2Enum_2Enum] : (~~ (surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3a))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2a0)),inj__ty_2Enum_2Enum(V1a1)),inj__ty_2EordinalNotation_2Eosyntax(V0a2))))))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__nchotomy,lemma,(( ! [V0oo:tp__ty_2EordinalNotation_2Eosyntax] : ((? [V1n:tp__ty_2Enum_2Enum] : (V0oo = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1n))))) | (? [V2o:tp__ty_2EordinalNotation_2Eosyntax] : (? [V3n:tp__ty_2Enum_2Enum] : (? [V4o0:tp__ty_2EordinalNotation_2Eosyntax] : (V0oo = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2o)),inj__ty_2Enum_2Enum(V3n)),inj__ty_2EordinalNotation_2Eosyntax(V4o0))))))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__Axiom,lemma,(( ! [A_27a:del]: ( ! [V0f0:$i] : (mem(V0f0,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V1f1:$i] : (mem(V1f1,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,arr(A_27a,arr(A_27a,A_27a)))))) => (? [V2fn:$i] : (mem(V2fn,arr(ty_2EordinalNotation_2Eosyntax,A_27a)) & (( ! [V3a:tp__ty_2Enum_2Enum] : (ap(V2fn,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3a))) = ap(V0f0,inj__ty_2Enum_2Enum(V3a)))) & ( ! [V4a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5a1:tp__ty_2Enum_2Enum] : ( ! [V6a2:tp__ty_2EordinalNotation_2Eosyntax] : (ap(V2fn,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V4a0)),inj__ty_2Enum_2Enum(V5a1)),inj__ty_2EordinalNotation_2Eosyntax(V6a2))) = ap(ap(ap(ap(ap(V1f1,inj__ty_2Enum_2Enum(V5a1)),inj__ty_2EordinalNotation_2Eosyntax(V4a0)),inj__ty_2EordinalNotation_2Eosyntax(V6a2)),ap(V2fn,inj__ty_2EordinalNotation_2Eosyntax(V4a0))),ap(V2fn,inj__ty_2EordinalNotation_2Eosyntax(V6a2))))))))))))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__induction,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2EordinalNotation_2Eosyntax,bool)) => ((( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1n))))) & ( ! [V2o:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3o0:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V2o))) & p(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V3o0)))) => ( ! [V4n:tp__ty_2Enum_2Enum] : p(ap(V0P,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2o)),inj__ty_2Enum_2Enum(V4n)),inj__ty_2EordinalNotation_2Eosyntax(V3o0))))))))) => ( ! [V5o:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V5o))))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__case__cong,lemma,(( ! [A_27a:del]: ( ! [V0f_27:$i] : (mem(V0f_27,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V1f1_27:$i] : (mem(V1f1_27,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,A_27a)))) => ( ! [V2M:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3M_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4f:$i] : (mem(V4f,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V5f1:$i] : (mem(V5f1,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,A_27a)))) => (((V2M = V3M_27) & (( ! [V6a:tp__ty_2Enum_2Enum] : ((V3M_27 = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V6a)))) => (ap(V4f,inj__ty_2Enum_2Enum(V6a)) = ap(V0f_27,inj__ty_2Enum_2Enum(V6a))))) & ( ! [V7a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8a1:tp__ty_2Enum_2Enum] : ( ! [V9a2:tp__ty_2EordinalNotation_2Eosyntax] : ((V3M_27 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V7a0)),inj__ty_2Enum_2Enum(V8a1)),inj__ty_2EordinalNotation_2Eosyntax(V9a2)))) => (ap(ap(ap(V5f1,inj__ty_2EordinalNotation_2Eosyntax(V7a0)),inj__ty_2Enum_2Enum(V8a1)),inj__ty_2EordinalNotation_2Eosyntax(V9a2)) = ap(ap(ap(V1f1_27,inj__ty_2EordinalNotation_2Eosyntax(V7a0)),inj__ty_2Enum_2Enum(V8a1)),inj__ty_2EordinalNotation_2Eosyntax(V9a2))))))))) => (ap(ap(ap(c_2EordinalNotation_2Eosyntax__CASE(A_27a),inj__ty_2EordinalNotation_2Eosyntax(V2M)),V4f),V5f1) = ap(ap(ap(c_2EordinalNotation_2Eosyntax__CASE(A_27a),inj__ty_2EordinalNotation_2Eosyntax(V3M_27)),V0f_27),V1f1_27)))))))))))))))).
tff(conj_thm_2EordinalNotation_2Eosyntax__case__eq,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V2f1:$i] : (mem(V2f1,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2Enum_2Enum,arr(ty_2EordinalNotation_2Eosyntax,A_27a)))) => ( ! [V3v:$i] : (mem(V3v,A_27a) => ((ap(ap(ap(c_2EordinalNotation_2Eosyntax__CASE(A_27a),inj__ty_2EordinalNotation_2Eosyntax(V0x)),V1f),V2f1) = V3v) <=> ((? [V4n:tp__ty_2Enum_2Enum] : ((V0x = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V4n)))) & (ap(V1f,inj__ty_2Enum_2Enum(V4n)) = V3v))) | (? [V5o_27:tp__ty_2EordinalNotation_2Eosyntax] : (? [V6n:tp__ty_2Enum_2Enum] : (? [V7o0:tp__ty_2EordinalNotation_2Eosyntax] : ((V0x = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V5o_27)),inj__ty_2Enum_2Enum(V6n)),inj__ty_2EordinalNotation_2Eosyntax(V7o0)))) & (ap(ap(ap(V2f1,inj__ty_2EordinalNotation_2Eosyntax(V5o_27)),inj__ty_2Enum_2Enum(V6n)),inj__ty_2EordinalNotation_2Eosyntax(V7o0)) = V3v))))))))))))))))).
tff(ax_thm_2EordinalNotation_2Eexpt__def,axiom,(( ! [V0v0:tp__ty_2Enum_2Enum] : (surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2Eexpt,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0v0)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2Eexpt,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1e)),inj__ty_2Enum_2Enum(V2k)),inj__ty_2EordinalNotation_2Eosyntax(V3t)))) = V1e)))))).
tff(ax_thm_2EordinalNotation_2Ecoeff__def,axiom,(( ! [V0x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Ecoeff,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0x)))) = V0x)) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Ecoeff,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1e)),inj__ty_2Enum_2Enum(V2k)),inj__ty_2EordinalNotation_2Eosyntax(V3t)))) = V2k)))))).
tff(ax_thm_2EordinalNotation_2Efinp__def,axiom,(( ! [V0v0:tp__ty_2Enum_2Enum] : (p(ap(c_2EordinalNotation_2Efinp,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0v0)))) <=> $true)) & ( ! [V1v1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2v2:tp__ty_2Enum_2Enum] : ( ! [V3v3:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Efinp,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1v1)),inj__ty_2Enum_2Enum(V2v2)),inj__ty_2EordinalNotation_2Eosyntax(V3v3)))) <=> $false)))))).
tff(ax_thm_2EordinalNotation_2Etail__def,axiom,( ! [V0e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2Etail,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V0e)),inj__ty_2Enum_2Enum(V1k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) = V2t))))).
tff(ax_thm_2EordinalNotation_2Erank__def,axiom,(( ! [V0v0:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0v0)))) = fo__c_2Enum_2E0)) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1e)),inj__ty_2Enum_2Enum(V2k)),inj__ty_2EordinalNotation_2Eosyntax(V3t)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V1e)))))))))).
tff(ax_thm_2EordinalNotation_2Eoless__def,axiom,(c_2EordinalNotation_2Eoless = f2791)).
tff(conj_thm_2EordinalNotation_2Eoless__rules,lemma,((( ! [V0k1:tp__ty_2Enum_2Enum] : ( ! [V1k2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0k1)),inj__ty_2Enum_2Enum(V1k2))) => p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0k1))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k2))))))) & (( ! [V2k1:tp__ty_2Enum_2Enum] : ( ! [V3e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4k2:tp__ty_2Enum_2Enum] : ( ! [V5t2:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2k1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V3e2)),inj__ty_2Enum_2Enum(V4k2)),inj__ty_2EordinalNotation_2Eosyntax(V5t2)))))))) & (( ! [V6e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7k1:tp__ty_2Enum_2Enum] : ( ! [V8t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V9e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10k2:tp__ty_2Enum_2Enum] : ( ! [V11t2:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V6e1)),inj__ty_2EordinalNotation_2Eosyntax(V9e2))) => p(ap(ap(c_2EordinalNotation_2Eoless,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V6e1)),inj__ty_2Enum_2Enum(V7k1)),inj__ty_2EordinalNotation_2Eosyntax(V8t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V9e2)),inj__ty_2Enum_2Enum(V10k2)),inj__ty_2EordinalNotation_2Eosyntax(V11t2))))))))))) & (( ! [V12e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V13k1:tp__ty_2Enum_2Enum] : ( ! [V14t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16k2:tp__ty_2Enum_2Enum] : ( ! [V17t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V12e1 = V15e2) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V13k1)),inj__ty_2Enum_2Enum(V16k2)))) => p(ap(ap(c_2EordinalNotation_2Eoless,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V12e1)),inj__ty_2Enum_2Enum(V13k1)),inj__ty_2EordinalNotation_2Eosyntax(V14t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V15e2)),inj__ty_2Enum_2Enum(V16k2)),inj__ty_2EordinalNotation_2Eosyntax(V17t2))))))))))) & ( ! [V18e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V19k1:tp__ty_2Enum_2Enum] : ( ! [V20t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V21e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22k2:tp__ty_2Enum_2Enum] : ( ! [V23t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V18e1 = V21e2) & ((V19k1 = V22k2) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V20t1)),inj__ty_2EordinalNotation_2Eosyntax(V23t2))))) => p(ap(ap(c_2EordinalNotation_2Eoless,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V18e1)),inj__ty_2Enum_2Enum(V19k1)),inj__ty_2EordinalNotation_2Eosyntax(V20t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V21e2)),inj__ty_2Enum_2Enum(V22k2)),inj__ty_2EordinalNotation_2Eosyntax(V23t2))))))))))))))))).
tff(conj_thm_2EordinalNotation_2Eoless__ind,lemma,(( ! [V0oless_27:$i] : (mem(V0oless_27,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool))) => ((( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1k1)),inj__ty_2Enum_2Enum(V2k2))) => p(ap(ap(V0oless_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k1))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2k2))))))) & (( ! [V3k1:tp__ty_2Enum_2Enum] : ( ! [V4e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k2:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0oless_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3k1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V4e2)),inj__ty_2Enum_2Enum(V5k2)),inj__ty_2EordinalNotation_2Eosyntax(V6t2)))))))) & (( ! [V7e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k1:tp__ty_2Enum_2Enum] : ( ! [V9t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11k2:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2EordinalNotation_2Eosyntax(V10e2))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2Enum_2Enum(V8k1)),inj__ty_2EordinalNotation_2Eosyntax(V9t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V10e2)),inj__ty_2Enum_2Enum(V11k2)),inj__ty_2EordinalNotation_2Eosyntax(V12t2))))))))))) & (( ! [V13e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14k1:tp__ty_2Enum_2Enum] : ( ! [V15t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V17k2:tp__ty_2Enum_2Enum] : ( ! [V18t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V13e1 = V16e2) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V14k1)),inj__ty_2Enum_2Enum(V17k2)))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V13e1)),inj__ty_2Enum_2Enum(V14k1)),inj__ty_2EordinalNotation_2Eosyntax(V15t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V16e2)),inj__ty_2Enum_2Enum(V17k2)),inj__ty_2EordinalNotation_2Eosyntax(V18t2))))))))))) & ( ! [V19e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V20k1:tp__ty_2Enum_2Enum] : ( ! [V21t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V23k2:tp__ty_2Enum_2Enum] : ( ! [V24t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V19e1 = V22e2) & ((V20k1 = V23k2) & p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V21t1)),inj__ty_2EordinalNotation_2Eosyntax(V24t2))))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V19e1)),inj__ty_2Enum_2Enum(V20k1)),inj__ty_2EordinalNotation_2Eosyntax(V21t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V22e2)),inj__ty_2Enum_2Enum(V23k2)),inj__ty_2EordinalNotation_2Eosyntax(V24t2))))))))))))))) => ( ! [V25a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V26a1:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V25a0)),inj__ty_2EordinalNotation_2Eosyntax(V26a1))) => p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V25a0)),inj__ty_2EordinalNotation_2Eosyntax(V26a1))))))))))).
tff(conj_thm_2EordinalNotation_2Eoless__strongind,lemma,(( ! [V0oless_27:$i] : (mem(V0oless_27,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool))) => ((( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1k1)),inj__ty_2Enum_2Enum(V2k2))) => p(ap(ap(V0oless_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k1))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2k2))))))) & (( ! [V3k1:tp__ty_2Enum_2Enum] : ( ! [V4e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k2:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0oless_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3k1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V4e2)),inj__ty_2Enum_2Enum(V5k2)),inj__ty_2EordinalNotation_2Eosyntax(V6t2)))))))) & (( ! [V7e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k1:tp__ty_2Enum_2Enum] : ( ! [V9t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11k2:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2EordinalNotation_2Eosyntax(V10e2))) & p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2EordinalNotation_2Eosyntax(V10e2)))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2Enum_2Enum(V8k1)),inj__ty_2EordinalNotation_2Eosyntax(V9t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V10e2)),inj__ty_2Enum_2Enum(V11k2)),inj__ty_2EordinalNotation_2Eosyntax(V12t2))))))))))) & (( ! [V13e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14k1:tp__ty_2Enum_2Enum] : ( ! [V15t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V17k2:tp__ty_2Enum_2Enum] : ( ! [V18t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V13e1 = V16e2) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V14k1)),inj__ty_2Enum_2Enum(V17k2)))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V13e1)),inj__ty_2Enum_2Enum(V14k1)),inj__ty_2EordinalNotation_2Eosyntax(V15t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V16e2)),inj__ty_2Enum_2Enum(V17k2)),inj__ty_2EordinalNotation_2Eosyntax(V18t2))))))))))) & ( ! [V19e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V20k1:tp__ty_2Enum_2Enum] : ( ! [V21t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V23k2:tp__ty_2Enum_2Enum] : ( ! [V24t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V19e1 = V22e2) & ((V20k1 = V23k2) & (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V21t1)),inj__ty_2EordinalNotation_2Eosyntax(V24t2))) & p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V21t1)),inj__ty_2EordinalNotation_2Eosyntax(V24t2)))))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V19e1)),inj__ty_2Enum_2Enum(V20k1)),inj__ty_2EordinalNotation_2Eosyntax(V21t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V22e2)),inj__ty_2Enum_2Enum(V23k2)),inj__ty_2EordinalNotation_2Eosyntax(V24t2))))))))))))))) => ( ! [V25a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V26a1:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V25a0)),inj__ty_2EordinalNotation_2Eosyntax(V26a1))) => p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V25a0)),inj__ty_2EordinalNotation_2Eosyntax(V26a1))))))))))).
tff(conj_thm_2EordinalNotation_2Eoless__cases,lemma,(( ! [V0a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1a1:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0a0)),inj__ty_2EordinalNotation_2Eosyntax(V1a1))) <=> ((? [V2k1:tp__ty_2Enum_2Enum] : (? [V3k2:tp__ty_2Enum_2Enum] : ((V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2k1)))) & ((V1a1 = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3k2)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2k1)),inj__ty_2Enum_2Enum(V3k2))))))) | ((? [V4k1:tp__ty_2Enum_2Enum] : (? [V5e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V6k2:tp__ty_2Enum_2Enum] : (? [V7t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V4k1)))) & (V1a1 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V5e2)),inj__ty_2Enum_2Enum(V6k2)),inj__ty_2EordinalNotation_2Eosyntax(V7t2))))))))) | ((? [V8e1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V9k1:tp__ty_2Enum_2Enum] : (? [V10t1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V11e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V12k2:tp__ty_2Enum_2Enum] : (? [V13t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V8e1)),inj__ty_2Enum_2Enum(V9k1)),inj__ty_2EordinalNotation_2Eosyntax(V10t1)))) & ((V1a1 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V11e2)),inj__ty_2Enum_2Enum(V12k2)),inj__ty_2EordinalNotation_2Eosyntax(V13t2)))) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V8e1)),inj__ty_2EordinalNotation_2Eosyntax(V11e2))))))))))) | ((? [V14e1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V15k1:tp__ty_2Enum_2Enum] : (? [V16t1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V17e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V18k2:tp__ty_2Enum_2Enum] : (? [V19t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e1)),inj__ty_2Enum_2Enum(V15k1)),inj__ty_2EordinalNotation_2Eosyntax(V16t1)))) & ((V1a1 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V17e2)),inj__ty_2Enum_2Enum(V18k2)),inj__ty_2EordinalNotation_2Eosyntax(V19t2)))) & ((V14e1 = V17e2) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V15k1)),inj__ty_2Enum_2Enum(V18k2)))))))))))) | (? [V20e1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V21k1:tp__ty_2Enum_2Enum] : (? [V22t1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V23e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V24k2:tp__ty_2Enum_2Enum] : (? [V25t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V20e1)),inj__ty_2Enum_2Enum(V21k1)),inj__ty_2EordinalNotation_2Eosyntax(V22t1)))) & ((V1a1 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V23e2)),inj__ty_2Enum_2Enum(V24k2)),inj__ty_2EordinalNotation_2Eosyntax(V25t2)))) & ((V20e1 = V23e2) & ((V21k1 = V24k2) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V22t1)),inj__ty_2EordinalNotation_2Eosyntax(V25t2)))))))))))))))))))))).
tff(conj_thm_2EordinalNotation_2Eoless__strong__ind,lemma,(( ! [V0oless_27:$i] : (mem(V0oless_27,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool))) => ((( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1k1)),inj__ty_2Enum_2Enum(V2k2))) => p(ap(ap(V0oless_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k1))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2k2))))))) & (( ! [V3k1:tp__ty_2Enum_2Enum] : ( ! [V4e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k2:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0oless_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3k1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V4e2)),inj__ty_2Enum_2Enum(V5k2)),inj__ty_2EordinalNotation_2Eosyntax(V6t2)))))))) & (( ! [V7e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k1:tp__ty_2Enum_2Enum] : ( ! [V9t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11k2:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2EordinalNotation_2Eosyntax(V10e2))) & p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2EordinalNotation_2Eosyntax(V10e2)))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V7e1)),inj__ty_2Enum_2Enum(V8k1)),inj__ty_2EordinalNotation_2Eosyntax(V9t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V10e2)),inj__ty_2Enum_2Enum(V11k2)),inj__ty_2EordinalNotation_2Eosyntax(V12t2))))))))))) & (( ! [V13e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14k1:tp__ty_2Enum_2Enum] : ( ! [V15t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V17k2:tp__ty_2Enum_2Enum] : ( ! [V18t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V13e1 = V16e2) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V14k1)),inj__ty_2Enum_2Enum(V17k2)))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V13e1)),inj__ty_2Enum_2Enum(V14k1)),inj__ty_2EordinalNotation_2Eosyntax(V15t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V16e2)),inj__ty_2Enum_2Enum(V17k2)),inj__ty_2EordinalNotation_2Eosyntax(V18t2))))))))))) & ( ! [V19e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V20k1:tp__ty_2Enum_2Enum] : ( ! [V21t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V23k2:tp__ty_2Enum_2Enum] : ( ! [V24t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V19e1 = V22e2) & ((V20k1 = V23k2) & (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V21t1)),inj__ty_2EordinalNotation_2Eosyntax(V24t2))) & p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V21t1)),inj__ty_2EordinalNotation_2Eosyntax(V24t2)))))) => p(ap(ap(V0oless_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V19e1)),inj__ty_2Enum_2Enum(V20k1)),inj__ty_2EordinalNotation_2Eosyntax(V21t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V22e2)),inj__ty_2Enum_2Enum(V23k2)),inj__ty_2EordinalNotation_2Eosyntax(V24t2))))))))))))))) => ( ! [V25a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V26a1:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V25a0)),inj__ty_2EordinalNotation_2Eosyntax(V26a1))) => p(ap(ap(V0oless_27,inj__ty_2EordinalNotation_2Eosyntax(V25a0)),inj__ty_2EordinalNotation_2Eosyntax(V26a1))))))))))).
tff(conj_thm_2EordinalNotation_2Eoless__End__End,lemma,(( ! [V0k1:tp__ty_2Enum_2Enum] : ( ! [V1k2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0k1))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k2)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0k1)),inj__ty_2Enum_2Enum(V1k2)))))))).
tff(conj_thm_2EordinalNotation_2Eoless__equations,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V6k1:tp__ty_2Enum_2Enum] : ( ! [V7t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V9k2:tp__ty_2Enum_2Enum] : ( ! [V10t2:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0m))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) & ((p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0m))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2e)),inj__ty_2Enum_2Enum(V3k)),inj__ty_2EordinalNotation_2Eosyntax(V4t)))) <=> $true) & ((p(ap(ap(c_2EordinalNotation_2Eoless,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2e)),inj__ty_2Enum_2Enum(V3k)),inj__ty_2EordinalNotation_2Eosyntax(V4t))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0m)))) <=> $false) & (p(ap(ap(c_2EordinalNotation_2Eoless,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V5e1)),inj__ty_2Enum_2Enum(V6k1)),inj__ty_2EordinalNotation_2Eosyntax(V7t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V8e2)),inj__ty_2Enum_2Enum(V9k2)),inj__ty_2EordinalNotation_2Eosyntax(V10t2)))) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V5e1)),inj__ty_2EordinalNotation_2Eosyntax(V8e2))),inj__o(fo__c_2Ebool_2ET)),ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Emin_2E_3D(ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V5e1)),inj__ty_2EordinalNotation_2Eosyntax(V8e2))),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V6k1)),inj__ty_2Enum_2Enum(V9k2)))),inj__o(fo__c_2Ebool_2ET)),ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Emin_2E_3D(ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V5e1)),inj__ty_2EordinalNotation_2Eosyntax(V8e2))),ap(ap(c_2Ebool_2E_2F_5C,ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V6k1)),inj__ty_2Enum_2Enum(V9k2))),ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V7t1)),inj__ty_2EordinalNotation_2Eosyntax(V10t2))))),inj__o(fo__c_2Ebool_2ET)),inj__o(fo__c_2Ebool_2EF)))))))))))))))))))))).
tff(ax_thm_2EordinalNotation_2Eis__ord__def,axiom,(c_2EordinalNotation_2Eis__ord = f2798)).
tff(conj_thm_2EordinalNotation_2Eis__ord__rules,lemma,((( ! [V0k:tp__ty_2Enum_2Enum] : p(ap(c_2EordinalNotation_2Eis__ord,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0k))))) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1e))) & ((~~ (V1e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2k))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V3t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V3t))),inj__ty_2EordinalNotation_2Eosyntax(V1e))))))) => p(ap(c_2EordinalNotation_2Eis__ord,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1e)),inj__ty_2Enum_2Enum(V2k)),inj__ty_2EordinalNotation_2Eosyntax(V3t))))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__ind,lemma,(( ! [V0is__ord_27:$i] : (mem(V0is__ord_27,arr(ty_2EordinalNotation_2Eosyntax,bool)) => ((( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(V0is__ord_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k))))) & ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V2e))) & ((~~ (V2e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3k))) & (p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V4t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V4t))),inj__ty_2EordinalNotation_2Eosyntax(V2e))))))) => p(ap(V0is__ord_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2e)),inj__ty_2Enum_2Enum(V3k)),inj__ty_2EordinalNotation_2Eosyntax(V4t))))))))) => ( ! [V5a0:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V5a0))) => p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V5a0)))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__strongind,lemma,(( ! [V0is__ord_27:$i] : (mem(V0is__ord_27,arr(ty_2EordinalNotation_2Eosyntax,bool)) => ((( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(V0is__ord_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k))))) & ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2e))) & (p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V2e))) & ((~~ (V2e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3k))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V4t))) & (p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V4t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V4t))),inj__ty_2EordinalNotation_2Eosyntax(V2e))))))))) => p(ap(V0is__ord_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2e)),inj__ty_2Enum_2Enum(V3k)),inj__ty_2EordinalNotation_2Eosyntax(V4t))))))))) => ( ! [V5a0:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V5a0))) => p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V5a0)))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__cases,lemma,(( ! [V0a0:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0a0))) <=> ((? [V1k:tp__ty_2Enum_2Enum] : (V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k))))) | (? [V2e:tp__ty_2EordinalNotation_2Eosyntax] : (? [V3k:tp__ty_2Enum_2Enum] : (? [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2e)),inj__ty_2Enum_2Enum(V3k)),inj__ty_2EordinalNotation_2Eosyntax(V4t)))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2e))) & ((~~ (V2e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3k))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V4t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V4t))),inj__ty_2EordinalNotation_2Eosyntax(V2e)))))))))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__strong__ind,lemma,(( ! [V0is__ord_27:$i] : (mem(V0is__ord_27,arr(ty_2EordinalNotation_2Eosyntax,bool)) => ((( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(V0is__ord_27,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1k))))) & ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2e))) & (p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V2e))) & ((~~ (V2e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V3k))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V4t))) & (p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V4t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V4t))),inj__ty_2EordinalNotation_2Eosyntax(V2e))))))))) => p(ap(V0is__ord_27,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V2e)),inj__ty_2Enum_2Enum(V3k)),inj__ty_2EordinalNotation_2Eosyntax(V4t))))))))) => ( ! [V5a0:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V5a0))) => p(ap(V0is__ord_27,inj__ty_2EordinalNotation_2Eosyntax(V5a0)))))))))).
tff(conj_thm_2EordinalNotation_2Edecompose__plus,lemma,(( ! [V0e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V0e)),inj__ty_2Enum_2Enum(V1k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) => (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0e))) & ((~~ (V0e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1k))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V2t))),inj__ty_2EordinalNotation_2Eosyntax(V0e))))))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__equations,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0k)))) <=> $true) & (p(ap(c_2EordinalNotation_2Eis__ord,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1e)),inj__ty_2Enum_2Enum(V0k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) <=> (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1e))) & ((~~ (V1e = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0k))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2t))) & p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V2t))),inj__ty_2EordinalNotation_2Eosyntax(V1e)))))))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__expt__closed,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) => p(ap(c_2EordinalNotation_2Eis__ord,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V0x)))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__tail__closed,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ p(ap(c_2EordinalNotation_2Efinp,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) & p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) => p(ap(c_2EordinalNotation_2Eis__ord,ap(c_2EordinalNotation_2Etail,inj__ty_2EordinalNotation_2Eosyntax(V0x)))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__downclosed,lemma,(( ! [V0w:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V0w)),inj__ty_2Enum_2Enum(V1k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) => (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0w))) & p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2t)))))))))).
tff(conj_thm_2EordinalNotation_2Eis__ord__coeff__pos,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ p(ap(c_2EordinalNotation_2Efinp,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) & p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2EordinalNotation_2Ecoeff,inj__ty_2EordinalNotation_2Eosyntax(V0x)))))))).
tff(conj_thm_2EordinalNotation_2Erank__expt,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) & (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))))) => (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) = V1n)))))).
tff(conj_thm_2EordinalNotation_2Eoless__antirefl,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) => (~~ p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0x)),inj__ty_2EordinalNotation_2Eosyntax(V0x)))))))).
tff(conj_thm_2EordinalNotation_2Eoless__antisym,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1y))) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0x)),inj__ty_2EordinalNotation_2Eosyntax(V1y))))) => (~~ p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V1y)),inj__ty_2EordinalNotation_2Eosyntax(V0x))))))))).
tff(conj_thm_2EordinalNotation_2Erank__less__imp__oless,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1y))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x))),ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V1y)))))) => p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0x)),inj__ty_2EordinalNotation_2Eosyntax(V1y)))))))).
tff(conj_thm_2EordinalNotation_2Eoless__imp__rank__leq,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1y))) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0x)),inj__ty_2EordinalNotation_2Eosyntax(V1y))))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x))),ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V1y))))))))).
tff(conj_thm_2EordinalNotation_2Erank__0__End,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x))) = fo__c_2Enum_2E0) <=> (? [V1n:tp__ty_2Enum_2Enum] : (V0x = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2EordinalNotation_2Erank__finp,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x))) = fo__c_2Enum_2E0) <=> p(ap(c_2EordinalNotation_2Efinp,inj__ty_2EordinalNotation_2Eosyntax(V0x))))))).
tff(conj_thm_2EordinalNotation_2Erank__positive__exists,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) <=> (? [V1e:tp__ty_2EordinalNotation_2Eosyntax] : (? [V2c:tp__ty_2Enum_2Enum] : (? [V3t:tp__ty_2EordinalNotation_2Eosyntax] : (V0x = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V1e)),inj__ty_2Enum_2Enum(V2c)),inj__ty_2EordinalNotation_2Eosyntax(V3t))))))))))).
tff(conj_thm_2EordinalNotation_2Erank__positive,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) <=> (V0x = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V0x))),ap(c_2EordinalNotation_2Ecoeff,inj__ty_2EordinalNotation_2Eosyntax(V0x))),ap(c_2EordinalNotation_2Etail,inj__ty_2EordinalNotation_2Eosyntax(V0x))))))))).
tff(conj_thm_2EordinalNotation_2Erank__positive__expt,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V0x))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) => (surj__ty_2Enum_2Enum(ap(c_2EordinalNotation_2Erank,ap(c_2EordinalNotation_2Eexpt,inj__ty_2EordinalNotation_2Eosyntax(V0x)))) = V1n)))))).
tff(conj_thm_2EordinalNotation_2Eoless__expt,lemma,(( ! [V0e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V0e)),inj__ty_2Enum_2Enum(V1k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) => p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0e)),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V0e)),inj__ty_2Enum_2Enum(V1k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))))))))).
tff(conj_thm_2EordinalNotation_2Eoless__tail,lemma,(( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) & (~~ p(ap(c_2EordinalNotation_2Efinp,inj__ty_2EordinalNotation_2Eosyntax(V0x))))) => p(ap(ap(c_2EordinalNotation_2Eoless,ap(c_2EordinalNotation_2Etail,inj__ty_2EordinalNotation_2Eosyntax(V0x))),inj__ty_2EordinalNotation_2Eosyntax(V0x))))))).
tff(conj_thm_2EordinalNotation_2Elemma,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1P:$i] : (mem(V1P,arr(ty_2EordinalNotation_2Eosyntax,bool)) => ((? [V2x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2x))) & (p(ap(V1P,inj__ty_2EordinalNotation_2Eosyntax(V2x))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V2x))),inj__ty_2Enum_2Enum(V0n)))))) => (? [V3m:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V3m))) & (p(ap(V1P,inj__ty_2EordinalNotation_2Eosyntax(V3m))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V3m))),inj__ty_2Enum_2Enum(V0n))) & ( ! [V4y:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V4y))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2EordinalNotation_2Erank,inj__ty_2EordinalNotation_2Eosyntax(V4y))),inj__ty_2Enum_2Enum(V0n))) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V4y)),inj__ty_2EordinalNotation_2Eosyntax(V3m))))) => (~~ p(ap(V1P,inj__ty_2EordinalNotation_2Eosyntax(V4y)))))))))))))))).
tff(conj_thm_2EordinalNotation_2Emain__lemma,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2EordinalNotation_2Eosyntax,bool)) => ((? [V1x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V1x))) & p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1x))))) => (? [V2x:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V2x))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V2x))) & ( ! [V3y:tp__ty_2EordinalNotation_2Eosyntax] : ((p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V3y))) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V3y)),inj__ty_2EordinalNotation_2Eosyntax(V2x)))) => (~~ p(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V3y)))))))))))))).
tff(ax_thm_2EordinalNotation_2Eord__less__def,axiom,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : (p(ap(ap(c_2EordinalNotation_2Eord__less,inj__ty_2EordinalNotation_2Eosyntax(V0x)),inj__ty_2EordinalNotation_2Eosyntax(V1y))) <=> (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V0x))) & (p(ap(c_2EordinalNotation_2Eis__ord,inj__ty_2EordinalNotation_2Eosyntax(V1y))) & p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V0x)),inj__ty_2EordinalNotation_2Eosyntax(V1y))))))))).
tff(conj_thm_2EordinalNotation_2EWF__ord__less,lemma,(p(ap(c_2Erelation_2EWF(ty_2EordinalNotation_2Eosyntax),c_2EordinalNotation_2Eord__less)))).
tff(conj_thm_2EordinalNotation_2Ee0__INDUCTION,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2EordinalNotation_2Eosyntax)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2EordinalNotation_2Eord__less,ap(V1f,V3y)),ap(V1f,V2x))) => p(ap(V0P,V3y))))) => p(ap(V0P,V2x))))) => ( ! [V4x:$i] : (mem(V4x,A_27a) => p(ap(V0P,V4x)))))))))))).
tff(conj_thm_2EordinalNotation_2Ee0__RECURSION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0M:$i] : (mem(V0M,arr(arr(A_27a,A_27b),arr(A_27a,A_27b))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2EordinalNotation_2Eosyntax)) => p(ap(c_2Ebool_2E_3F_21(arr(A_27a,A_27b)),f2802(A_27b,A_27a,V0M,V1f))))))))))).
tff(conj_thm_2EordinalNotation_2Eord__add__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool))) => ((( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1m))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2n)))))) & (( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k:tp__ty_2Enum_2Enum] : ( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0P,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3m))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V4p)),inj__ty_2Enum_2Enum(V5k)),inj__ty_2EordinalNotation_2Eosyntax(V6t)))))))) & (( ! [V7e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10m:tp__ty_2Enum_2Enum] : (p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V9t)),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V10m)))) => p(ap(ap(V0P,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V7e)),inj__ty_2Enum_2Enum(V8k)),inj__ty_2EordinalNotation_2Eosyntax(V9t))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V10m))))))))) & ( ! [V11e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k1:tp__ty_2Enum_2Enum] : ( ! [V13t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15k2:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2EordinalNotation_2Eosyntax] : ((((~~ p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V11e1)),inj__ty_2EordinalNotation_2Eosyntax(V14e2)))) & (~~ (V11e1 = V14e2))) => p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V13t1)),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V15k2)),inj__ty_2EordinalNotation_2Eosyntax(V16t2))))) => p(ap(ap(V0P,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V11e1)),inj__ty_2Enum_2Enum(V12k1)),inj__ty_2EordinalNotation_2Eosyntax(V13t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V15k2)),inj__ty_2EordinalNotation_2Eosyntax(V16t2)))))))))))))) => ( ! [V17v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V18v1:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V17v)),inj__ty_2EordinalNotation_2Eosyntax(V18v1)))))))))).
tff(conj_thm_2EordinalNotation_2Eord__add__def,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__add,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1m))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))))) & (( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4m:tp__ty_2Enum_2Enum] : ( ! [V5k:tp__ty_2Enum_2Enum] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__add,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V4m))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V3p)),inj__ty_2Enum_2Enum(V5k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V3p)),inj__ty_2Enum_2Enum(V5k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))))))) & (( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7m:tp__ty_2Enum_2Enum] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9e:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__add,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V9e)),inj__ty_2Enum_2Enum(V8k)),inj__ty_2EordinalNotation_2Eosyntax(V6t))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V7m)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V9e)),inj__ty_2Enum_2Enum(V8k)),ap(ap(c_2EordinalNotation_2Eord__add,inj__ty_2EordinalNotation_2Eosyntax(V6t)),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V7m)))))))))) & ( ! [V10t2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k2:tp__ty_2Enum_2Enum] : ( ! [V13k1:tp__ty_2Enum_2Enum] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15e1:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__add,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2Enum_2Enum(V13k1)),inj__ty_2EordinalNotation_2Eosyntax(V11t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V12k2)),inj__ty_2EordinalNotation_2Eosyntax(V10t2)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2EordinalNotation_2Eosyntax(V14e2))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V12k2)),inj__ty_2EordinalNotation_2Eosyntax(V10t2))),ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2Emin_2E_3D(ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2EordinalNotation_2Eosyntax(V14e2))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V13k1)),inj__ty_2Enum_2Enum(V12k2))),inj__ty_2EordinalNotation_2Eosyntax(V10t2))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2Enum_2Enum(V13k1)),ap(ap(c_2EordinalNotation_2Eord__add,inj__ty_2EordinalNotation_2Eosyntax(V11t1)),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V12k2)),inj__ty_2EordinalNotation_2Eosyntax(V10t2))))))))))))))))))).
tff(conj_thm_2EordinalNotation_2Eord__sub__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool))) => ((( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1m))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V2n)))))) & (( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k:tp__ty_2Enum_2Enum] : ( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0P,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V3m))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V4p)),inj__ty_2Enum_2Enum(V5k)),inj__ty_2EordinalNotation_2Eosyntax(V6t)))))))) & (( ! [V7e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10m:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V7e)),inj__ty_2Enum_2Enum(V8k)),inj__ty_2EordinalNotation_2Eosyntax(V9t))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V10m)))))))) & ( ! [V11e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k1:tp__ty_2Enum_2Enum] : ( ! [V13t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15k2:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2EordinalNotation_2Eosyntax] : ((((~~ p(ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V11e1)),inj__ty_2EordinalNotation_2Eosyntax(V14e2)))) & ((V11e1 = V14e2) & ((~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V12k1)),inj__ty_2Enum_2Enum(V15k2)))) & (~~ p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V12k1)),inj__ty_2Enum_2Enum(V15k2))))))) => p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V13t1)),inj__ty_2EordinalNotation_2Eosyntax(V16t2)))) => p(ap(ap(V0P,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V11e1)),inj__ty_2Enum_2Enum(V12k1)),inj__ty_2EordinalNotation_2Eosyntax(V13t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V15k2)),inj__ty_2EordinalNotation_2Eosyntax(V16t2)))))))))))))) => ( ! [V17v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V18v1:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V17v)),inj__ty_2EordinalNotation_2Eosyntax(V18v1)))))))))).
tff(conj_thm_2EordinalNotation_2Eord__sub__def,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__sub,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V1m))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))))) & (( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4m:tp__ty_2Enum_2Enum] : ( ! [V5k:tp__ty_2Enum_2Enum] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__sub,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V4m))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V3p)),inj__ty_2Enum_2Enum(V5k)),inj__ty_2EordinalNotation_2Eosyntax(V2t)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))) & (( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7m:tp__ty_2Enum_2Enum] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9e:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__sub,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V9e)),inj__ty_2Enum_2Enum(V8k)),inj__ty_2EordinalNotation_2Eosyntax(V6t))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V7m)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V9e)),inj__ty_2Enum_2Enum(V8k)),inj__ty_2EordinalNotation_2Eosyntax(V6t)))))))) & ( ! [V10t2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k2:tp__ty_2Enum_2Enum] : ( ! [V13k1:tp__ty_2Enum_2Enum] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15e1:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__sub,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2Enum_2Enum(V13k1)),inj__ty_2EordinalNotation_2Eosyntax(V11t1))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V12k2)),inj__ty_2EordinalNotation_2Eosyntax(V10t2)))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2EordinalNotation_2Eoless,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2EordinalNotation_2Eosyntax(V14e2))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2Emin_2E_3D(ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2EordinalNotation_2Eosyntax(V14e2))),ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V13k1)),inj__ty_2Enum_2Enum(V12k2))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V13k1)),inj__ty_2Enum_2Enum(V12k2))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V13k1)),inj__ty_2Enum_2Enum(V12k2))),inj__ty_2EordinalNotation_2Eosyntax(V11t1))),ap(ap(c_2EordinalNotation_2Eord__sub,inj__ty_2EordinalNotation_2Eosyntax(V11t1)),inj__ty_2EordinalNotation_2Eosyntax(V10t2))))),ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V15e1)),inj__ty_2Enum_2Enum(V13k1)),inj__ty_2EordinalNotation_2Eosyntax(V11t1))))))))))))))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,type,(tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,type,(inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax : tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,type,(surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax : $i > tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax] : (surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax] : (mem(inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(X),ty_2Epair_2Eprod(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax)) => (X = inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(X)))))).
tff(conj_thm_2EordinalNotation_2Eord__mult__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2EordinalNotation_2Eosyntax,arr(ty_2EordinalNotation_2Eosyntax,bool))) => (( ! [V1x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2y:tp__ty_2EordinalNotation_2Eosyntax] : ((( ! [V3v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4v1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7k:tp__ty_2Enum_2Enum] : ( ! [V8t:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ ((V1x = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (V2y = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))) & ((surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(ap(ap(c_2Epair_2E_2C(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V1x)),inj__ty_2EordinalNotation_2Eosyntax(V2y))) = surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(ap(ap(c_2Epair_2E_2C(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V3v)),inj__ty_2EordinalNotation_2Eosyntax(V4v1)))) & ((V3v = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V5m)))) & (V4v1 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V6e)),inj__ty_2Enum_2Enum(V7k)),inj__ty_2EordinalNotation_2Eosyntax(V8t))))))) => p(ap(ap(V0P,ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(V5m))),inj__ty_2EordinalNotation_2Eosyntax(V8t)))))))))) & ( ! [V9v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10v1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11e_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k_27:tp__ty_2Enum_2Enum] : ( ! [V13t_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15k2:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ ((V1x = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (V2y = surj__ty_2EordinalNotation_2Eosyntax(ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))) & ((surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(ap(ap(c_2Epair_2E_2C(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V1x)),inj__ty_2EordinalNotation_2Eosyntax(V2y))) = surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax(ap(ap(c_2Epair_2E_2C(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V9v)),inj__ty_2EordinalNotation_2Eosyntax(V10v1)))) & ((V9v = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V11e_27)),inj__ty_2Enum_2Enum(V12k_27)),inj__ty_2EordinalNotation_2Eosyntax(V13t_27)))) & (V10v1 = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V14e2)),inj__ty_2Enum_2Enum(V15k2)),inj__ty_2EordinalNotation_2Eosyntax(V16t2))))))) => p(ap(ap(V0P,ap(ap(ap(c_2EordinalNotation_2EPlus,inj__ty_2EordinalNotation_2Eosyntax(V11e_27)),inj__ty_2Enum_2Enum(V12k_27)),inj__ty_2EordinalNotation_2Eosyntax(V13t_27))),inj__ty_2EordinalNotation_2Eosyntax(V16t2))))))))))))) => p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V1x)),inj__ty_2EordinalNotation_2Eosyntax(V2y)))))) => ( ! [V17v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V18v1:tp__ty_2EordinalNotation_2Eosyntax] : p(ap(ap(V0P,inj__ty_2EordinalNotation_2Eosyntax(V17v)),inj__ty_2EordinalNotation_2Eosyntax(V18v1)))))))))).
tff(conj_thm_2EordinalNotation_2Eord__mult__def,conjecture,(( ! [V0y:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1x:tp__ty_2EordinalNotation_2Eosyntax] : (surj__ty_2EordinalNotation_2Eosyntax(ap(ap(c_2EordinalNotation_2Eord__mult,inj__ty_2EordinalNotation_2Eosyntax(V1x)),inj__ty_2EordinalNotation_2Eosyntax(V0y))) = surj__ty_2EordinalNotation_2Eosyntax(ap(ap(ap(c_2Ebool_2ECOND(ty_2EordinalNotation_2Eosyntax),ap(ap(c_2Ebool_2E_5C_2F,ap(ap(c_2Emin_2E_3D(ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V1x)),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))),ap(ap(c_2Emin_2E_3D(ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V0y)),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))),ap(c_2EordinalNotation_2EEnd,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Epair_2Epair__CASE(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax),ap(ap(c_2Epair_2E_2C(ty_2EordinalNotation_2Eosyntax,ty_2EordinalNotation_2Eosyntax),inj__ty_2EordinalNotation_2Eosyntax(V1x)),inj__ty_2EordinalNotation_2Eosyntax(V0y))),f2816)))))))).
