include('Axioms/mergesort_2.ax').
tff(stp_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum : tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(surj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum : $i > tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum(inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum] : (mem(inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum(X),ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(stp_iso_mem_c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Enum_2Enum)) => (X = inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum(surj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Estring__num_2En2nsum,type,(c_2Estring__num_2En2nsum:$i)).
tff(mem_c_2Estring__num_2En2nsum,axiom,mem(c_2Estring__num_2En2nsum,arr(ty_2Enum_2Enum,ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(tp_c_2Estring__num_2En2s,type,(c_2Estring__num_2En2s:$i)).
tff(mem_c_2Estring__num_2En2s,axiom,mem(c_2Estring__num_2En2s,arr(ty_2Enum_2Enum,ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(tp_c_2Estring__num_2Ensum2n,type,(c_2Estring__num_2Ensum2n:$i)).
tff(mem_c_2Estring__num_2Ensum2n,axiom,mem(c_2Estring__num_2Ensum2n,arr(ty_2Esum_2Esum(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(stp_fo_c_2Estring__num_2Ensum2n,type,(fo__c_2Estring__num_2Ensum2n:(tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Estring__num_2Ensum2n,axiom,( ! [X0:tp__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Estring__num_2Ensum2n(X0)) = ap(c_2Estring__num_2Ensum2n,inj__c_ty_2Esum_2Esum_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Estring__num_2Es2n,type,(c_2Estring__num_2Es2n:$i)).
tff(mem_c_2Estring__num_2Es2n,axiom,mem(c_2Estring__num_2Es2n,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Enum_2Enum))).
tff(stp_fo_c_2Estring__num_2Es2n,type,(fo__c_2Estring__num_2Es2n:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Estring__num_2Es2n,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (inj__ty_2Enum_2Enum(fo__c_2Estring__num_2Es2n(X0)) = ap(c_2Estring__num_2Es2n,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(X0))))).
tff(stp_c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
tff(stp_inj_c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : tp__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i)).
tff(stp_surj_c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar : $i > tp__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar)).
tff(stp_inj_surj_c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(inj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)) = X))).
tff(stp_inj_mem_c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem(inj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X),ty_2Esum_2Esum(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)))))).
tff(stp_iso_mem_c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : (mem(X,ty_2Esum_2Esum(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar))) => (X = inj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(surj__c_ty_2Esum_2Esum_c_ty_2Elist_2Elist_ty_2Estring_2Echar_c_ty_2Elist_2Elist_ty_2Estring_2Echar(X)))))).
tff(tp_c_2Estring__num_2Es2ssum,type,(c_2Estring__num_2Es2ssum:$i)).
tff(mem_c_2Estring__num_2Es2ssum,axiom,mem(c_2Estring__num_2Es2ssum,arr(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Esum_2Esum(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar))))).
tff(tp_c_2Estring__num_2Essum2s,type,(c_2Estring__num_2Essum2s:$i)).
tff(mem_c_2Estring__num_2Essum2s,axiom,mem(c_2Estring__num_2Essum2s,arr(ty_2Esum_2Esum(ty_2Elist_2Elist(ty_2Estring_2Echar),ty_2Elist_2Elist(ty_2Estring_2Echar)),ty_2Elist_2Elist(ty_2Estring_2Echar)))).
tff(ax_thm_2Estring__num_2En2s__primitive__def,axiom,(c_2Estring__num_2En2s = ap(ap(c_2Erelation_2EWFREC(ty_2Enum_2Enum,ty_2Elist_2Elist(ty_2Estring_2Echar)),ap(c_2Emin_2E_40(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),f1826)),f1831))).
tff(conj_thm_2Estring__num_2En2s__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => (( ! [V1n:tp__ty_2Enum_2Enum] : (( ! [V2r0:tp__ty_2Enum_2Enum] : ( ! [V3r:tp__ty_2Enum_2Enum] : (((~~ (V1n = fo__c_2Enum_2E0)) & ((V2r0 = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))) & (V3r = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2r0)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))),inj__ty_2Enum_2Enum(V2r0)))))) => p(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V3r))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))) => p(ap(V0P,inj__ty_2Enum_2Enum(V1n))))) => ( ! [V4v:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V4v))))))))).
tff(conj_thm_2Estring__num_2En2s__def,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring__num_2En2s,inj__ty_2Enum_2Enum(V0n))) = surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(ty_2Estring_2Echar)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),c_2Elist_2ENIL(ty_2Estring_2Echar)),ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Elist_2Elist(ty_2Estring_2Echar)),f1834(V0n)),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))))).
tff(ax_thm_2Estring__num_2Es2n__def,axiom,((surj__ty_2Enum_2Enum(ap(c_2Estring__num_2Es2n,c_2Elist_2ENIL(ty_2Estring_2Echar))) = fo__c_2Enum_2E0) & ( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__ty_2Enum_2Enum(ap(c_2Estring__num_2Es2n,ap(ap(c_2Elist_2ECONS(ty_2Estring_2Echar),inj__ty_2Estring_2Echar(V0c)),inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Estring__num_2Es2n,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V1s))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))),ap(c_2Estring_2EORD,inj__ty_2Estring_2Echar(V0c)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Estring__num_2Es2n__n2s,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Estring__num_2Es2n,ap(c_2Estring__num_2En2s,inj__ty_2Enum_2Enum(V0n)))) = V0n)))).
tff(conj_thm_2Estring__num_2En2s__s2n,conjecture,(( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(ap(c_2Estring__num_2En2s,ap(c_2Estring__num_2Es2n,inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar(V0s)))) = V0s)))).