include('Axioms/sum_num^2.ax').
thf(tp_c_2Esorting_2EPART,type,(c_2Esorting_2EPART:(del>$i))).
thf(mem_c_2Esorting_2EPART,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EPART@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))))).
thf(tp_c_2Esorting_2EPART3,type,(c_2Esorting_2EPART3:(del>$i))).
thf(mem_c_2Esorting_2EPART3,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EPART3@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@A_27a@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))))).
thf(tp_c_2Esorting_2EPARTITION,type,(c_2Esorting_2EPARTITION:(del>$i))).
thf(mem_c_2Esorting_2EPARTITION,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EPARTITION@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Esorting_2EPERM,type,(c_2Esorting_2EPERM:(del>$i))).
thf(mem_c_2Esorting_2EPERM,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EPERM@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Esorting_2EPERM__SINGLE__SWAP,type,(c_2Esorting_2EPERM__SINGLE__SWAP:(del>$i))).
thf(mem_c_2Esorting_2EPERM__SINGLE__SWAP,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Esorting_2EQSORT,type,(c_2Esorting_2EQSORT:(del>$i))).
thf(mem_c_2Esorting_2EQSORT,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EQSORT@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Esorting_2EQSORT3,type,(c_2Esorting_2EQSORT3:(del>$i))).
thf(mem_c_2Esorting_2EQSORT3,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2EQSORT3@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Esorting_2ESORTED,type,(c_2Esorting_2ESORTED:(del>$i))).
thf(mem_c_2Esorting_2ESORTED,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2ESORTED@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Esorting_2ESORTS,type,(c_2Esorting_2ESORTS:(del>$i))).
thf(mem_c_2Esorting_2ESORTS,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2ESORTS@A_27a)@(arr@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(arr@(arr@A_27a@(arr@A_27a@bool))@bool))))).
thf(tp_c_2Esorting_2ESTABLE,type,(c_2Esorting_2ESTABLE:(del>$i))).
thf(mem_c_2Esorting_2ESTABLE,axiom,( ! [A_27a:del] : (mem@(c_2Esorting_2ESTABLE@A_27a)@(arr@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(arr@(arr@A_27a@(arr@A_27a@bool))@bool))))).
thf(ax_thm_2Esorting_2EPERM__DEF,axiom,( ! [A_27a:del]: ( ! [V0L1:$i] : ((mem@V0L1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1L2:$i] : ((mem@V1L2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0L1)@V1L2)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V2x))@V0L1) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V2x))@V1L2))))))))))).
thf(conj_thm_2Esorting_2EPERM__REFL,lemma,( ! [A_27a:del]: ( ! [V0L:$i] : ((mem@V0L@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0L)@V0L)))))).
thf(conj_thm_2Esorting_2EPERM__INTRO,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Elist_2Elist@A_27a)) => ( ! [V1y:$i] : ((mem@V1y@(ty_2Elist_2Elist@A_27a)) => ((V0x = V1y) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0x)@V1y))))))))).
thf(conj_thm_2Esorting_2EPERM__transitive,lemma,( ! [A_27a:del]: (p@(ap@(c_2Erelation_2Etransitive@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM@A_27a))))).
thf(conj_thm_2Esorting_2EPERM__TRANS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Elist_2Elist@A_27a)) => ( ! [V1y:$i] : ((mem@V1y@(ty_2Elist_2Elist@A_27a)) => ( ! [V2z:$i] : ((mem@V2z@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0x)@V1y)) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1y)@V2z))) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0x)@V2z))))))))))).
thf(conj_thm_2Esorting_2EPERM__SYM,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l2)@V0l1))))))))).
thf(conj_thm_2Esorting_2EPERM__CONG,lemma,( ! [A_27a:del]: ( ! [V0L1:$i] : ((mem@V0L1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1L2:$i] : ((mem@V1L2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2L3:$i] : ((mem@V2L3@(ty_2Elist_2Elist@A_27a)) => ( ! [V3L4:$i] : ((mem@V3L4@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0L1)@V2L3)) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1L2)@V3L4))) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0L1)@V1L2))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2L3)@V3L4)))))))))))))).
thf(conj_thm_2Esorting_2EPERM__MONO,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V0l1))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1l2)))))))))))).
thf(conj_thm_2Esorting_2EPERM__CONS__IFF,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2l1))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l2))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l1)@V1l2))))))))))).
thf(conj_thm_2Esorting_2EPERM__NIL,lemma,( ! [A_27a:del]: ( ! [V0L:$i] : ((mem@V0L@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0L)@(c_2Elist_2ENIL@A_27a))) <=> (V0L = (c_2Elist_2ENIL@A_27a))) & ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(c_2Elist_2ENIL@A_27a))@V0L)) <=> (V0L = (c_2Elist_2ENIL@A_27a)))))))).
thf(conj_thm_2Esorting_2EPERM__SING,lemma,( ! [A_27a:del]: ( ! [V0L:$i] : ((mem@V0L@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0L)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a)))) <=> (V0L = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a)))) & ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a)))@V0L)) <=> (V0L = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a))))))))))).
thf(conj_thm_2Esorting_2EPERM__CONS__EQ__APPEND,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Elist_2Elist@A_27a)) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2h)@V0t))@V1L)) <=> (? [V3M:$i] : ((mem@V3M@(ty_2Elist_2Elist@A_27a)) & (? [V4N:$i] : ((mem@V4N@(ty_2Elist_2Elist@A_27a)) & ((V1L = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V3M)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2h)@V4N))) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0t)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V3M)@V4N))))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V0l1))))))))).
thf(conj_thm_2Esorting_2ECONS__PERM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2M:$i] : ((mem@V2M@(ty_2Elist_2Elist@A_27a)) => ( ! [V3N:$i] : ((mem@V3N@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1L)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2M)@V3N))) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1L))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2M)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V3N))))))))))))))).
thf(conj_thm_2Esorting_2EAPPEND__PERM__SYM,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(ty_2Elist_2Elist@A_27a)) => ( ! [V1B:$i] : ((mem@V1B@(ty_2Elist_2Elist@A_27a)) => ( ! [V2C:$i] : ((mem@V2C@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0A)@V1B))@V2C)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1B)@V0A))@V2C))))))))))).
thf(conj_thm_2Esorting_2EPERM__SPLIT__IF,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Emin_2E_3D@bool)@(ap@V0P@V3x))@(ap@c_2Ebool_2E_7E@(ap@V1Q@V3x))))))@V2l)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V2l))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1Q)@V2l))))))))))))).
thf(conj_thm_2Esorting_2EPERM__SPLIT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V1l))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@bool@bool)@c_2Ebool_2E_7E)@V0P))@V1l)))))))))).
thf(conj_thm_2Esorting_2EFILTER__EQ__REP,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l) = (ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l)))@V0x)))))))).
thf(conj_thm_2Esorting_2EFILTER__EQ__LENGTHS__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => (((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l1))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V2l2)))) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l1) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V2l2))))))))))).
thf(conj_thm_2Esorting_2EPERM__alt,lemma,( ! [A_27a:del]: ( ! [V0L1:$i] : ((mem@V0L1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1L2:$i] : ((mem@V1L2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0L1)@V1L2)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V2x))@V0L1))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V2x))@V1L2))))))))))))).
thf(conj_thm_2Esorting_2EPERM__IND,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool))) => (((p@(ap@(ap@V0P@(c_2Elist_2ENIL@A_27a))@(c_2Elist_2ENIL@A_27a))) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@V0P@V2l1)@V3l2)) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V2l1))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V3l2)))))))))) & (( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => ( ! [V6l1:$i] : ((mem@V6l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V7l2:$i] : ((mem@V7l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@V0P@V6l1)@V7l2)) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5y)@V6l1)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5y)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@V7l2))))))))))))) & ( ! [V8l1:$i] : ((mem@V8l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V9l2:$i] : ((mem@V9l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V10l3:$i] : ((mem@V10l3@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@V0P@V8l1)@V9l2)) & (p@(ap@(ap@V0P@V9l2)@V10l3))) => (p@(ap@(ap@V0P@V8l1)@V10l3)))))))))))) => ( ! [V11l1:$i] : ((mem@V11l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V12l2:$i] : ((mem@V12l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V11l1)@V12l2)) => (p@(ap@(ap@V0P@V11l1)@V12l2)))))))))))).
thf(conj_thm_2Esorting_2EPERM__SWAP__AT__FRONT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1y)@V2l1)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1y)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V3l2)))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l1)@V3l2))))))))))))).
thf(conj_thm_2Esorting_2EPERM__SWAP__L__AT__FRONT,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@(ty_2Elist_2Elist@A_27a)) => ( ! [V3y:$i] : ((mem@V3y@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2x)@V3y))@V0l1))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V3y)@V2x))@V1l2))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2))))))))))))).
thf(conj_thm_2Esorting_2EPERM__STRONG__IND,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool))) => (((p@(ap@(ap@V0P@(c_2Elist_2ENIL@A_27a))@(c_2Elist_2ENIL@A_27a))) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l1)@V3l2)) & (p@(ap@(ap@V0P@V2l1)@V3l2))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V2l1))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V3l2)))))))))) & (( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => ( ! [V6l1:$i] : ((mem@V6l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V7l2:$i] : ((mem@V7l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V6l1)@V7l2)) & (p@(ap@(ap@V0P@V6l1)@V7l2))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5y)@V6l1)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5y)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@V7l2))))))))))))) & ( ! [V8l1:$i] : ((mem@V8l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V9l2:$i] : ((mem@V9l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V10l3:$i] : ((mem@V10l3@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V8l1)@V9l2)) & ((p@(ap@(ap@V0P@V8l1)@V9l2)) & ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V9l2)@V10l3)) & (p@(ap@(ap@V0P@V9l2)@V10l3))))) => (p@(ap@(ap@V0P@V8l1)@V10l3)))))))))))) => ( ! [V11l1:$i] : ((mem@V11l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V12l2:$i] : ((mem@V12l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V11l1)@V12l2)) => (p@(ap@(ap@V0P@V11l1)@V12l2)))))))))))).
thf(conj_thm_2Esorting_2EPERM__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V0l1)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V1l2)))))))))).
thf(conj_thm_2Esorting_2EPERM__MEM__EQ,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0l1))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l2))))))))))))).
thf(conj_thm_2Esorting_2EPERM__LIST__TO__SET,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) => ((ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0l1) = (ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l2))))))))).
thf(conj_thm_2Esorting_2ESORTED__IND,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@bool))) => ((( ! [V1R:$i] : ((mem@V1R@(arr@A_27a@(arr@A_27a@bool))) => (p@(ap@(ap@V0P@V1R)@(c_2Elist_2ENIL@A_27a))))) & (( ! [V2R:$i] : ((mem@V2R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => (p@(ap@(ap@V0P@V2R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3x)@(c_2Elist_2ENIL@A_27a)))))))) & ( ! [V4R:$i] : ((mem@V4R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V5x:$i] : ((mem@V5x@A_27a) => ( ! [V6y:$i] : ((mem@V6y@A_27a) => ( ! [V7rst:$i] : ((mem@V7rst@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@V0P@V4R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V6y)@V7rst))) => (p@(ap@(ap@V0P@V4R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V6y)@V7rst))))))))))))))) => ( ! [V8v:$i] : ((mem@V8v@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V9v1:$i] : ((mem@V9v1@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@V0P@V8v)@V9v1))))))))))).
thf(conj_thm_2Esorting_2ESORTED__DEF,lemma,( ! [A_27a:del]: (( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(c_2Elist_2ENIL@A_27a))) <=> $true))) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2R:$i] : ((mem@V2R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V2R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a)))) <=> $true))))) & ( ! [V3y:$i] : ((mem@V3y@A_27a) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5rst:$i] : ((mem@V5rst@(ty_2Elist_2Elist@A_27a)) => ( ! [V6R:$i] : ((mem@V6R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V6R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3y)@V5rst)))) <=> ((p@(ap@(ap@V6R@V4x)@V3y)) & (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V6R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3y)@V5rst))))))))))))))))).
thf(ax_thm_2Esorting_2ESORTS__DEF,axiom,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))) => ( ! [V1R:$i] : ((mem@V1R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Esorting_2ESORTS@A_27a)@V0f)@V1R)) <=> ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l)@(ap@(ap@V0f@V1R)@V2l))) & (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V1R)@(ap@(ap@V0f@V1R)@V2l))))))))))))).
thf(conj_thm_2Esorting_2ESORTED__EQ,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1L))) <=> ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1L)) & ( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1L))) => (p@(ap@(ap@V0R@V2x)@V3y)))))))))))))))).
thf(conj_thm_2Esorting_2ESORTED__APPEND,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1L1:$i] : ((mem@V1L1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2L2:$i] : ((mem@V2L2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1L1)) & ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V2L2)) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1L1))) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4y)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2L2)))) => (p@(ap@(ap@V0R@V3x)@V4y)))))))))) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1L1)@V2L2)))))))))))).
thf(ax_thm_2Esorting_2EPART__DEF,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V0P)@(c_2Elist_2ENIL@A_27a))@V1l1)@V2l2) = (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V1l1)@V2l2)))))))) & ( ! [V3P:$i] : ((mem@V3P@(arr@A_27a@bool)) => ( ! [V4h:$i] : ((mem@V4h@A_27a) => ( ! [V5rst:$i] : ((mem@V5rst@(ty_2Elist_2Elist@A_27a)) => ( ! [V6l1:$i] : ((mem@V6l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V7l2:$i] : ((mem@V7l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V3P)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4h)@V5rst))@V6l1)@V7l2) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ap@V3P@V4h))@(ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V3P)@V5rst)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4h)@V6l1))@V7l2))@(ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V3P)@V5rst)@V6l1)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4h)@V7l2))))))))))))))))).
thf(conj_thm_2Esorting_2EPART__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4p:$i] : ((mem@V4p@(ty_2Elist_2Elist@A_27a)) => ( ! [V5q:$i] : ((mem@V5q@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V4p)@V5q) = (ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V0P)@V1L)@V2l1)@V3l2)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Elist_2ELENGTH@A_27a)@V1L))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l1)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V3l2))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Elist_2ELENGTH@A_27a)@V4p))@(ap@(c_2Elist_2ELENGTH@A_27a)@V5q))))))))))))))))))).
thf(conj_thm_2Esorting_2EPART__LENGTH__LEM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4p:$i] : ((mem@V4p@(ty_2Elist_2Elist@A_27a)) => ( ! [V5q:$i] : ((mem@V5q@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V4p)@V5q) = (ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V0P)@V1L)@V2l1)@V3l2)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V4p))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Elist_2ELENGTH@A_27a)@V1L))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l1)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V3l2)))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V5q))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Elist_2ELENGTH@A_27a)@V1L))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l1)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V3l2)))))))))))))))))))).
thf(conj_thm_2Esorting_2EPARTs__HAVE__PROP,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2A:$i] : ((mem@V2A@(ty_2Elist_2Elist@A_27a)) => ( ! [V3B:$i] : ((mem@V3B@(ty_2Elist_2Elist@A_27a)) => ( ! [V4l1:$i] : ((mem@V4l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V5l2:$i] : ((mem@V5l2@(ty_2Elist_2Elist@A_27a)) => ((((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V2A)@V3B) = (ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V0P)@V1L)@V4l1)@V5l2)) & (( ! [V6x:$i] : ((mem@V6x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V4l1))) => (p@(ap@V0P@V6x))))) & ( ! [V7x:$i] : ((mem@V7x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V7x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V5l2))) => (~~ (p@(ap@V0P@V7x)))))))) => (( ! [V8z:$i] : ((mem@V8z@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V8z)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2A))) => (p@(ap@V0P@V8z))))) & ( ! [V9z:$i] : ((mem@V9z@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V9z)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V3B))) => (~~ (p@(ap@V0P@V9z)))))))))))))))))))))).
thf(conj_thm_2Esorting_2EPART__MEM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2a1:$i] : ((mem@V2a1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3a2:$i] : ((mem@V3a2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4l1:$i] : ((mem@V4l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V5l2:$i] : ((mem@V5l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V2a1)@V3a2) = (ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V0P)@V1L)@V4l1)@V5l2)) => ( ! [V6x:$i] : ((mem@V6x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1L)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4l1)@V5l2))))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2a1)@V3a2)))))))))))))))))))))).
thf(ax_thm_2Esorting_2EPARTITION__DEF,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Esorting_2EPARTITION@A_27a)@V0P)@V1l) = (ap@(ap@(ap@(ap@(c_2Esorting_2EPART@A_27a)@V0P)@V1l)@(c_2Elist_2ENIL@A_27a))@(c_2Elist_2ENIL@A_27a))))))))).
thf(conj_thm_2Esorting_2EQSORT__IND,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@bool))) => ((( ! [V1ord:$i] : ((mem@V1ord@(arr@A_27a@(arr@A_27a@bool))) => (p@(ap@(ap@V0P@V1ord)@(c_2Elist_2ENIL@A_27a))))) & ( ! [V2ord:$i] : ((mem@V2ord@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V3h:$i] : ((mem@V3h@A_27a) => ( ! [V4t:$i] : ((mem@V4t@(ty_2Elist_2Elist@A_27a)) => ((( ! [V5l1:$i] : ((mem@V5l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V6l2:$i] : ((mem@V6l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V5l1)@V6l2) = (ap@(ap@(c_2Esorting_2EPARTITION@A_27a)@(lam@A_27a@(^ [V7y:$i] : (ap@(ap@V2ord@V7y)@V3h))))@V4t)) => (p@(ap@(ap@V0P@V2ord)@V6l2))))))) & ( ! [V8l1:$i] : ((mem@V8l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V9l2:$i] : ((mem@V9l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V8l1)@V9l2) = (ap@(ap@(c_2Esorting_2EPARTITION@A_27a)@(lam@A_27a@(^ [V10y:$i] : (ap@(ap@V2ord@V10y)@V3h))))@V4t)) => (p@(ap@(ap@V0P@V2ord)@V8l1)))))))) => (p@(ap@(ap@V0P@V2ord)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3h)@V4t))))))))))) => ( ! [V11v:$i] : ((mem@V11v@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V12v1:$i] : ((mem@V12v1@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@V0P@V11v)@V12v1))))))))))).
thf(conj_thm_2Esorting_2EQSORT__DEF,lemma,( ! [A_27a:del]: (( ! [V0ord:$i] : ((mem@V0ord@(arr@A_27a@(arr@A_27a@bool))) => ((ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V0ord)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27a)))) & ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ( ! [V2ord:$i] : ((mem@V2ord@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V3h:$i] : ((mem@V3h@A_27a) => ((ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V2ord)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3h)@V1t)) = (ap@(ap@(c_2Ebool_2ELET@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Epair_2EUNCURRY@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V4l1:$i] : (lam@(ty_2Elist_2Elist@A_27a)@(^ [V5l2:$i] : (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V2ord)@V4l1))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3h)@(c_2Elist_2ENIL@A_27a))))@(ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V2ord)@V5l2))))))))@(ap@(ap@(c_2Esorting_2EPARTITION@A_27a)@(lam@A_27a@(^ [V6y:$i] : (ap@(ap@V2ord@V6y)@V3h))))@V1t)))))))))))).
thf(conj_thm_2Esorting_2EQSORT__MEM,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V0R)@V1L)))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1L)))))))))))).
thf(conj_thm_2Esorting_2EQSORT__PERM,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1L)@(ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V0R)@V1L))))))))).
thf(conj_thm_2Esorting_2EQSORT__SORTED,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1L:$i] : ((mem@V1L@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Etotal@A_27a)@V0R))) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V0R)@V1L)))))))))).
thf(conj_thm_2Esorting_2EQSORT__SORTS,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Etotal@A_27a)@V0R))) => (p@(ap@(ap@(c_2Esorting_2ESORTS@A_27a)@(c_2Esorting_2EQSORT@A_27a))@V0R))))))).
thf(conj_thm_2Esorting_2EPERM__APPEND__IFF,lemma,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V1l1))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V2l2))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V2l2))))))))) & ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ( ! [V4l1:$i] : ((mem@V4l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V5l2:$i] : ((mem@V5l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4l1)@V3l))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V5l2)@V3l))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V4l1)@V5l2)))))))))))).
thf(ax_thm_2Esorting_2EPERM__SINGLE__SWAP__DEF,axiom,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@V0l1)@V1l2)) <=> (? [V2x1:$i] : ((mem@V2x1@(ty_2Elist_2Elist@A_27a)) & (? [V3x2:$i] : ((mem@V3x2@(ty_2Elist_2Elist@A_27a)) & (? [V4x3:$i] : ((mem@V4x3@(ty_2Elist_2Elist@A_27a)) & ((V0l1 = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2x1)@V3x2))@V4x3)) & (V1l2 = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2x1)@V4x3))@V3x2)))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__SINGLE__SWAP__SYM,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@V0l1)@V1l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@V1l2)@V0l1))))))))).
thf(conj_thm_2Esorting_2EPERM__SINGLE__SWAP__I,lemma,( ! [A_27a:del]: ( ! [V0x1:$i] : ((mem@V0x1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x2:$i] : ((mem@V1x2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x3:$i] : ((mem@V2x3@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0x1)@V1x2))@V2x3))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0x1)@V2x3))@V1x2))))))))))).
thf(conj_thm_2Esorting_2EPERM__SINGLE__SWAP__APPEND,lemma,( ! [A_27a:del]: ( ! [V0x2:$i] : ((mem@V0x2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x3:$i] : ((mem@V1x3@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0x2)@V1x3))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x3)@V0x2))))))))).
thf(conj_thm_2Esorting_2EPERM__SINGLE__SWAP__REFL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@V0l)@V0l)))))).
thf(conj_thm_2Esorting_2EPERM__SINGLE__SWAP__CONS,lemma,( ! [A_27a:del]: ( ! [V0M:$i] : ((mem@V0M@(ty_2Elist_2Elist@A_27a)) => ( ! [V1N:$i] : ((mem@V1N@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@V0M)@V1N)) => (p@(ap@(ap@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V0M))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1N)))))))))))).
thf(conj_thm_2Esorting_2EPERM__SINGLE__SWAP__TC__CONS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1M:$i] : ((mem@V1M@(ty_2Elist_2Elist@A_27a)) => ( ! [V2N:$i] : ((mem@V2N@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(ap@(c_2Erelation_2ETC@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a))@V1M)@V2N)) => (p@(ap@(ap@(ap@(c_2Erelation_2ETC@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1M))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2N)))))))))))).
thf(conj_thm_2Esorting_2EPERM__TC,lemma,( ! [A_27a:del]: ((c_2Esorting_2EPERM@A_27a) = (ap@(c_2Erelation_2ETC@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a))))).
thf(conj_thm_2Esorting_2EPERM__RTC,lemma,( ! [A_27a:del]: ((c_2Esorting_2EPERM@A_27a) = (ap@(c_2Erelation_2ERTC@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a))))).
thf(conj_thm_2Esorting_2EPERM__EQC,lemma,( ! [A_27a:del]: ((c_2Esorting_2EPERM@A_27a) = (ap@(c_2Erelation_2EEQC@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM__SINGLE__SWAP@A_27a))))).
thf(conj_thm_2Esorting_2EPERM__lifts__transitive__relations,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@(ty_2Elist_2Elist@A_27a)@A_27b)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27b@(arr@A_27b@bool))) => ((( ! [V2x1:$i] : ((mem@V2x1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3x2:$i] : ((mem@V3x2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4x3:$i] : ((mem@V4x3@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@V1Q@(ap@V0f@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2x1)@V3x2))@V4x3)))@(ap@V0f@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2x1)@V4x3))@V3x2)))))))))) & (p@(ap@(c_2Erelation_2Etransitive@A_27b)@V1Q))) => ( ! [V5x:$i] : ((mem@V5x@(ty_2Elist_2Elist@A_27a)) => ( ! [V6y:$i] : ((mem@V6y@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V5x)@V6y)) => (p@(ap@(ap@V1Q@(ap@V0f@V5x))@(ap@V0f@V6y)))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__lifts__equalities,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@(ty_2Elist_2Elist@A_27a)@A_27b)) => (( ! [V1x1:$i] : ((mem@V1x1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x2:$i] : ((mem@V2x2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3x3:$i] : ((mem@V3x3@(ty_2Elist_2Elist@A_27a)) => ((ap@V0f@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x1)@V2x2))@V3x3)) = (ap@V0f@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x1)@V3x3))@V2x2))))))))) => ( ! [V4x:$i] : ((mem@V4x@(ty_2Elist_2Elist@A_27a)) => ( ! [V5y:$i] : ((mem@V5y@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V4x)@V5y)) => ((ap@V0f@V4x) = (ap@V0f@V5y))))))))))))).
thf(conj_thm_2Esorting_2EPERM__lifts__invariants,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@A_27a)@bool)) => (( ! [V1x1:$i] : ((mem@V1x1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x2:$i] : ((mem@V2x2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3x3:$i] : ((mem@V3x3@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@V0P@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x1)@V2x2))@V3x3))) => (p@(ap@V0P@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x1)@V3x3))@V2x2)))))))))) => ( ! [V4x:$i] : ((mem@V4x@(ty_2Elist_2Elist@A_27a)) => ( ! [V5y:$i] : ((mem@V5y@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@V0P@V4x)) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V4x)@V5y))) => (p@(ap@V0P@V5y)))))))))))).
thf(conj_thm_2Esorting_2EPERM__lifts__monotonicities,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))) => (( ! [V1x1:$i] : ((mem@V1x1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x2:$i] : ((mem@V2x2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3x3:$i] : ((mem@V3x3@(ty_2Elist_2Elist@A_27a)) => (? [V4x1_27:$i] : ((mem@V4x1_27@(ty_2Elist_2Elist@A_27b)) & (? [V5x2_27:$i] : ((mem@V5x2_27@(ty_2Elist_2Elist@A_27b)) & (? [V6x3_27:$i] : ((mem@V6x3_27@(ty_2Elist_2Elist@A_27b)) & (((ap@V0f@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x1)@V2x2))@V3x3)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27b)@(ap@(ap@(c_2Elist_2EAPPEND@A_27b)@V4x1_27)@V5x2_27))@V6x3_27)) & ((ap@V0f@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1x1)@V3x3))@V2x2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27b)@(ap@(ap@(c_2Elist_2EAPPEND@A_27b)@V4x1_27)@V6x3_27))@V5x2_27))))))))))))))) => ( ! [V7x:$i] : ((mem@V7x@(ty_2Elist_2Elist@A_27a)) => ( ! [V8y:$i] : ((mem@V8y@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V7x)@V8y)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27b)@(ap@V0f@V7x))@(ap@V0f@V8y)))))))))))))).
thf(conj_thm_2Esorting_2EPERM__EQUIVALENCE,lemma,( ! [A_27a:del]: (p@(ap@(c_2Erelation_2Eequivalence@(ty_2Elist_2Elist@A_27a))@(c_2Esorting_2EPERM@A_27a))))).
thf(conj_thm_2Esorting_2EPERM__EQUIVALENCE__ALT__DEF,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Elist_2Elist@A_27a)) => ( ! [V1y:$i] : ((mem@V1y@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0x)@V1y)) <=> ((ap@(c_2Esorting_2EPERM@A_27a)@V0x) = (ap@(c_2Esorting_2EPERM@A_27a)@V1y))))))))).
thf(conj_thm_2Esorting_2EALL__DISTINCT__PERM,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) => ((p@(ap@(c_2Elist_2EALL__DISTINCT@A_27a)@V0l1)) <=> (p@(ap@(c_2Elist_2EALL__DISTINCT@A_27a)@V1l2)))))))))).
thf(conj_thm_2Esorting_2EPERM__ALL__DISTINCT,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(c_2Elist_2EALL__DISTINCT@A_27a)@V0l1)) & ((p@(ap@(c_2Elist_2EALL__DISTINCT@A_27a)@V1l2)) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0l1))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l2)))))))) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2))))))))).
thf(conj_thm_2Esorting_2EALL__DISTINCT__PERM__LIST__TO__SET__TO__LIST,lemma,( ! [A_27a:del]: ( ! [V0ls:$i] : ((mem@V0ls@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(c_2Elist_2EALL__DISTINCT@A_27a)@V0ls)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0ls)@(ap@(c_2Elist_2ESET__TO__LIST@A_27a)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0ls))))))))).
thf(conj_thm_2Esorting_2EPERM__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V2l2)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27b)@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@V1l1))@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@V2l2))))))))))))).
thf(conj_thm_2Esorting_2EPERM__SUM,lemma,( ! [V0l1:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ( ! [V1l2:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Esorting_2EPERM@ty_2Enum_2Enum)@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l1))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V1l2))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Elist_2ESUM@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l1))) = (surj__ty_2Enum_2Enum @ (ap@c_2Elist_2ESUM@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V1l2)))))))).
thf(conj_thm_2Esorting_2EPERM__FILTER,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V2l2)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V1l1))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V2l2)))))))))))).
thf(conj_thm_2Esorting_2EPERM__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0ls:$i] : ((mem@V0ls@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0ls)@(ap@(c_2Elist_2EREVERSE@A_27a)@V0ls))))))).
thf(conj_thm_2Esorting_2EPERM__REVERSE__EQ,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(c_2Elist_2EREVERSE@A_27a)@V0l1))@V1l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2))) & ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l2))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)))))))))).
thf(conj_thm_2Esorting_2EFOLDR__PERM,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3e:$i] : ((mem@V3e@A_27a) => (((p@(ap@(c_2Ecombin_2EASSOC@A_27a)@V0f)) & (p@(ap@(c_2Ecombin_2ECOMM@A_27a@A_27a)@V0f))) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V2l2)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V3e)@V1l1) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V3e)@V2l2)))))))))))))).
thf(conj_thm_2Esorting_2EPERM__SET__TO__LIST__count__COUNT__LIST,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Esorting_2EPERM@ty_2Enum_2Enum)@(ap@(c_2Elist_2ESET__TO__LIST@ty_2Enum_2Enum)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n))))@(ap@c_2Erich__list_2ECOUNT__LIST@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Esorting_2ESUM__IMAGE__count__SUM__GENLIST,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@V0f)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Elist_2ESUM@(ap@(ap@(c_2Elist_2EGENLIST@ty_2Enum_2Enum)@V0f)@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Esorting_2ESUM__IMAGE__count__MULT,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V3k:tp__ty_2Enum_2Enum] : (( ! [V4m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4m))@(inj__ty_2Enum_2Enum @ V0n))) => ((surj__ty_2Enum_2Enum @ (ap@V1g@(inj__ty_2Enum_2Enum @ V4m))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5x:$i] : (ap@V2f@(ap@(ap@c_2Earithmetic_2E_2B@V5x)@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2Enum_2Enum @ V4m)))))))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V3k))))))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@V2f)@(ap@c_2Epred__set_2Ecount@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@V1g)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n))))))))))))).
thf(conj_thm_2Esorting_2Esum__of__sums,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))) => ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V3m:$i] : (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@(ap@V0f@V3m))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1a))))))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V2b)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V4m:$i] : (ap@(ap@V0f@(ap@(ap@c_2Earithmetic_2EDIV@V4m)@(inj__ty_2Enum_2Enum @ V1a)))@(ap@(ap@c_2Earithmetic_2EMOD@V4m)@(inj__ty_2Enum_2Enum @ V1a))))))@(ap@c_2Epred__set_2Ecount@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V1a))@(inj__ty_2Enum_2Enum @ V2b))))))))))).
thf(conj_thm_2Esorting_2ESORTED__NIL,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(c_2Elist_2ENIL@A_27a))))))).
thf(conj_thm_2Esorting_2ESORTED__SING,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a)))))))))).
thf(conj_thm_2Esorting_2ESORTED__TL,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2xs:$i] : ((mem@V2xs@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V2xs))) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V2xs))))))))))).
thf(conj_thm_2Esorting_2ESORTED__EL__SUC,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1ls:$i] : ((mem@V1ls@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1ls)) <=> ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1ls))) => (p@(ap@(ap@V0R@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1ls))@(ap@(ap@(c_2Elist_2EEL@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))@V1ls)))))))))))).
thf(conj_thm_2Esorting_2ESORTED__EL__LESS,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) => ( ! [V1ls:$i] : ((mem@V1ls@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1ls)) <=> ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3n))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1ls)))) => (p@(ap@(ap@V0R@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V1ls))@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V3n))@V1ls)))))))))))))).
thf(conj_thm_2Esorting_2ESORTED__APPEND__IFF,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1L1:$i] : ((mem@V1L1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2L2:$i] : ((mem@V2L2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1L1)@V2L2))) <=> ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1L1)) & ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V2L2)) & ((V1L1 = (c_2Elist_2ENIL@A_27a)) | ((V2L2 = (c_2Elist_2ENIL@A_27a)) | (p@(ap@(ap@V0R@(ap@(c_2Elist_2ELAST@A_27a)@V1L1))@(ap@(c_2Elist_2EHD@A_27a)@V2L2)))))))))))))))).
thf(conj_thm_2Esorting_2EMEM__PERM,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l2)) => ( ! [V2a:$i] : ((mem@V2a@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2a)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0l1))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2a)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l2))))))))))))).
thf(conj_thm_2Esorting_2ESORTED__PERM__EQ,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Eantisymmetric@A_27a)@V0R))) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1l1)) & ((p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V2l2)) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V2l2)))) => (V1l1 = V2l2))))))))))).
thf(conj_thm_2Esorting_2EQSORT__eq__if__PERM,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (((p@(ap@(c_2Erelation_2Etotal@A_27a)@V0R)) & ((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Eantisymmetric@A_27a)@V0R)))) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V0R)@V1l1) = (ap@(ap@(c_2Esorting_2EQSORT@A_27a)@V0R)@V2l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V2l2)))))))))))).
thf(conj_thm_2Esorting_2ESORTED__FILTER,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1ls:$i] : ((mem@V1ls@(ty_2Elist_2Elist@A_27a)) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V1ls))) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V2P)@V1ls)))))))))))).
thf(conj_thm_2Esorting_2EALL__DISTINCT__SORTED__WEAKEN,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1R_27:$i] : ((mem@V1R_27@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V2ls:$i] : ((mem@V2ls@(ty_2Elist_2Elist@A_27a)) => ((( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2ls))) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4y)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2ls))) & (~~ (V3x = V4y)))) => ((p@(ap@(ap@V0R@V3x)@V4y)) <=> (p@(ap@(ap@V1R_27@V3x)@V4y)))))))) & ((p@(ap@(c_2Elist_2EALL__DISTINCT@A_27a)@V2ls)) & (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V0R)@V2ls)))) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V1R_27)@V2ls))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__APPEND__C,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1_27:$i] : ((mem@V1l1_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2_27:$i] : ((mem@V3l2_27@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V0l1) = (ap@(c_2Esorting_2EPERM@A_27a)@V1l1_27)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V2l2) = (ap@(c_2Esorting_2EPERM@A_27a)@V3l2_27)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V2l2)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1_27)@V3l2_27))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1_27:$i] : ((mem@V2l1_27@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@V2l1_27)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2l1_27)))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__APPEND__CONS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2l2))) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l1))@V2l2))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__SWAP__AT__FRONT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1y)@V2l))) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1y)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2l)))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONS__11__SWAP__AT__FRONT,lemma,( ! [A_27a:del]: ( ! [V0y:$i] : ((mem@V0y@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l2))) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0y)@V1l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0y)@V3l2))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONS__11__APPEND,lemma,( ! [A_27a:del]: ( ! [V0y:$i] : ((mem@V0y@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l3:$i] : ((mem@V3l3@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l2)@V3l3))) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0y)@V1l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l2)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0y)@V3l3))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONS__APPEND__1,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l2))) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V0l)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V3l2)@V0l))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONS__APPEND__2,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l2))) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V1l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V3l2))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__APPEND__APPEND__1,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l3:$i] : ((mem@V2l3@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l4:$i] : ((mem@V3l4@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V0l1) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V2l3))) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V3l4)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l3)@V3l4))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__APPEND__APPEND__2,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l3:$i] : ((mem@V2l3@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l4:$i] : ((mem@V3l4@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V0l1) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V2l3))) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V3l4)@V0l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V3l4)@V2l3))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V0l1))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONS__IFF,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@V2l2)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2l2)))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__APPEND__IFF,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V1l1) = (ap@(c_2Esorting_2EPERM@A_27a)@V2l2)) => ((ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V1l1)) = (ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V2l2)))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__CONG,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1_27:$i] : ((mem@V1l1_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2_27:$i] : ((mem@V3l2_27@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V0l1) = (ap@(c_2Esorting_2EPERM@A_27a)@V1l1_27)) => (((ap@(c_2Esorting_2EPERM@A_27a)@V2l2) = (ap@(c_2Esorting_2EPERM@A_27a)@V3l2_27)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V2l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1_27)@V3l2_27))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__CONG__2,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1_27:$i] : ((mem@V1l1_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2_27:$i] : ((mem@V3l2_27@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V1l1_27)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l2)@V3l2_27)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V2l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1_27)@V3l2_27))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__CONG__APPEND__IFF,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1_27:$i] : ((mem@V2l1_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4l2_27:$i] : ((mem@V4l2_27@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V2l1_27))) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V3l2)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V4l2_27))) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1)@V3l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l1_27)@V4l2_27))))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__CONG__APPEND__IFF2,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1_27:$i] : ((mem@V1l1_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1_27_27:$i] : ((mem@V2l1_27_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4l2_27:$i] : ((mem@V4l2_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V5l2_27_27:$i] : ((mem@V5l2_27_27@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1_27)@V2l1_27_27))) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V3l2)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4l2_27)@V5l2_27_27))) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l1_27)@V4l2_27)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l1)@V3l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l1_27_27)@V5l2_27_27)))))))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__FUN__SPLIT,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1_27:$i] : ((mem@V2l1_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V3l2))) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V2l1_27)@V1l1)) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1_27)@V3l2))))))))))))))).
thf(conj_thm_2Esorting_2EPERM__REWR,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1r:$i] : ((mem@V1r@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l)@V1r)) => ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@V2l1))@V3l2)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1r)@V2l1))@V3l2)))))))))))))).
thf(conj_thm_2Esorting_2EPERM__TO__APPEND__SIMPS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2r1:$i] : ((mem@V2r1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3r2:$i] : ((mem@V3r2@(ty_2Elist_2Elist@A_27a)) => ( ! [V4xs:$i] : ((mem@V4xs@(ty_2Elist_2Elist@A_27a)) => ( ! [V5ys:$i] : ((mem@V5ys@(ty_2Elist_2Elist@A_27a)) => ( ! [V6zs:$i] : ((mem@V6zs@(ty_2Elist_2Elist@A_27a)) => ( ! [V7r:$i] : ((mem@V7r@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V2r1))@V3r2))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2r1)@V3r2)))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2r1)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V3r2)))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2r1)@V3r2)))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@V5ys))@V6zs))@V7r)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V5ys)@V6zs)))@V7r))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V5ys))@V6zs))@V7r)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V5ys)@V6zs)))@V7r))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(c_2Elist_2ENIL@A_27a))@V1l))@V7r)) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@V7r))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@V1l))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@V2r1))@V3r2))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2r1)@V3r2)))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@V1l))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2r1)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@V3r2)))) <=> (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2r1)@V3r2)))) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27b)@(c_2Elist_2ENIL@A_27b))@(ap@(ap@(c_2Elist_2EAPPEND@A_27b)@(c_2Elist_2ENIL@A_27b))@(c_2Elist_2ENIL@A_27b)))) <=> $true) & (((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V4xs)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@(c_2Elist_2ENIL@A_27a)))@(c_2Elist_2ENIL@A_27a)))) <=> $true) & ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V4xs)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(c_2Elist_2ENIL@A_27a))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4xs)@(c_2Elist_2ENIL@A_27a))))) <=> $true))))))))))))))))))))))))))))).
thf(ax_thm_2Esorting_2ESTABLE__DEF,axiom,( ! [A_27a:del]: ( ! [V0sort:$i] : ((mem@V0sort@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))) => ( ! [V1r:$i] : ((mem@V1r@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Esorting_2ESTABLE@A_27a)@V0sort)@V1r)) <=> ((p@(ap@(ap@(c_2Esorting_2ESORTS@A_27a)@V0sort)@V1r)) & ( ! [V2p:$i] : ((mem@V2p@(arr@A_27a@bool)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((p@(ap@V2p@V3x)) & (p@(ap@V2p@V4y))) => (p@(ap@(ap@V1r@V3x)@V4y))))))) => ( ! [V5l:$i] : ((mem@V5l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V2p)@V5l) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@V2p)@(ap@(ap@V0sort@V1r)@V5l)))))))))))))))).
thf(ax_thm_2Esorting_2EPART3__DEF,axiom,( ! [A_27a:del]: (( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1h:$i] : ((mem@V1h@A_27a) => ((ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V0R)@V1h)@(c_2Elist_2ENIL@A_27a)) = (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(c_2Elist_2ENIL@A_27a))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))@(c_2Elist_2ENIL@A_27a)))))))) & ( ! [V2R:$i] : ((mem@V2R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V3h:$i] : ((mem@V3h@A_27a) => ( ! [V4hd:$i] : ((mem@V4hd@A_27a) => ( ! [V5tl:$i] : ((mem@V5tl@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V2R)@V3h)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4hd)@V5tl)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V2R@V3h)@V4hd))@(ap@(ap@V2R@V4hd)@V3h)))@(ap@(ap@(ap@(c_2Epair_2E_23_23@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27a)))@(ap@(ap@(c_2Epair_2E_23_23@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Elist_2ECONS@A_27a)@V4hd))@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27a))))@(ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V2R)@V3h)@V5tl)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))@(ap@(ap@V2R@V4hd)@V3h))@(ap@(ap@(ap@(c_2Epair_2E_23_23@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ap@(c_2Elist_2ECONS@A_27a)@V4hd))@(ap@(ap@(c_2Epair_2E_23_23@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27a)))@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27a))))@(ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V2R)@V3h)@V5tl)))@(ap@(ap@(ap@(c_2Epair_2E_23_23@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27a)))@(ap@(ap@(c_2Epair_2E_23_23@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Ecombin_2EI@(ty_2Elist_2Elist@A_27a)))@(ap@(c_2Elist_2ECONS@A_27a)@V4hd)))@(ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V2R)@V3h)@V5tl)))))))))))))))).
thf(conj_thm_2Esorting_2EPART3__FILTER,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1tl:$i] : ((mem@V1tl@(ty_2Elist_2Elist@A_27a)) => ( ! [V2hd:$i] : ((mem@V2hd@A_27a) => ((ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V0R)@V2hd)@V1tl) = (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V0R@V3x)@V2hd))@(ap@c_2Ebool_2E_7E@(ap@(ap@V0R@V2hd)@V3x))))))@V1tl))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V0R@V4x)@V2hd))@(ap@(ap@V0R@V2hd)@V4x)))))@V1tl))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@V0R@V5x)@V2hd)))))@V1tl)))))))))))).
thf(conj_thm_2Esorting_2EQSORT3__IND,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(ty_2Elist_2Elist@A_27a)@bool))) => ((( ! [V1R:$i] : ((mem@V1R@(arr@A_27a@(arr@A_27a@bool))) => (p@(ap@(ap@V0P@V1R)@(c_2Elist_2ENIL@A_27a))))) & ( ! [V2R:$i] : ((mem@V2R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V3hd:$i] : ((mem@V3hd@A_27a) => ( ! [V4tl:$i] : ((mem@V4tl@(ty_2Elist_2Elist@A_27a)) => ((( ! [V5lo:$i] : ((mem@V5lo@(ty_2Elist_2Elist@A_27a)) => ( ! [V6eq:$i] : ((mem@V6eq@(ty_2Elist_2Elist@A_27a)) => ( ! [V7hi:$i] : ((mem@V7hi@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@V5lo)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V6eq)@V7hi)) = (ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V2R)@V3hd)@V4tl)) => (p@(ap@(ap@V0P@V2R)@V7hi))))))))) & ( ! [V8lo:$i] : ((mem@V8lo@(ty_2Elist_2Elist@A_27a)) => ( ! [V9eq:$i] : ((mem@V9eq@(ty_2Elist_2Elist@A_27a)) => ( ! [V10hi:$i] : ((mem@V10hi@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@V8lo)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V9eq)@V10hi)) = (ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V2R)@V3hd)@V4tl)) => (p@(ap@(ap@V0P@V2R)@V8lo)))))))))) => (p@(ap@(ap@V0P@V2R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3hd)@V4tl))))))))))) => ( ! [V11v:$i] : ((mem@V11v@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V12v1:$i] : ((mem@V12v1@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@V0P@V11v)@V12v1))))))))))).
thf(conj_thm_2Esorting_2EQSORT3__DEF,lemma,( ! [A_27a:del]: (( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ((ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V0R)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27a)))) & ( ! [V1tl:$i] : ((mem@V1tl@(ty_2Elist_2Elist@A_27a)) => ( ! [V2hd:$i] : ((mem@V2hd@A_27a) => ( ! [V3R:$i] : ((mem@V3R@(arr@A_27a@(arr@A_27a@bool))) => ((ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V3R)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2hd)@V1tl)) = (ap@(ap@(c_2Ebool_2ELET@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Epair_2EUNCURRY@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V4lo:$i] : (ap@(c_2Epair_2EUNCURRY@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V5eq:$i] : (lam@(ty_2Elist_2Elist@A_27a)@(^ [V6hi:$i] : (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V3R)@V4lo))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2hd)@V5eq)))@(ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V3R)@V6hi)))))))))))@(ap@(ap@(ap@(c_2Esorting_2EPART3@A_27a)@V3R)@V2hd)@V1tl)))))))))))).
thf(conj_thm_2Esorting_2EPERM3,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Elist_2Elist@A_27a)) => ( ! [V1a:$i] : ((mem@V1a@(ty_2Elist_2Elist@A_27a)) => ( ! [V2a_27:$i] : ((mem@V2a_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V3b:$i] : ((mem@V3b@(ty_2Elist_2Elist@A_27a)) => ( ! [V4b_27:$i] : ((mem@V4b_27@(ty_2Elist_2Elist@A_27a)) => ( ! [V5c:$i] : ((mem@V5c@(ty_2Elist_2Elist@A_27a)) => ( ! [V6c_27:$i] : ((mem@V6c_27@(ty_2Elist_2Elist@A_27a)) => ((((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1a)@V2a_27)) & ((p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V3b)@V4b_27)) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V5c)@V6c_27)))) & (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0x)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1a)@V3b))@V5c)))) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0x)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2a_27)@V4b_27))@V6c_27)))))))))))))))))))).
thf(conj_thm_2Esorting_2EPERM3__FILTER,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V1l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V0R@V3x)@V2h))@(ap@c_2Ebool_2E_7E@(ap@(ap@V0R@V2h)@V3x))))))@V1l))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V0R@V4x)@V2h))@(ap@(ap@V0R@V2h)@V4x)))))@V1l)))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@V0R@V5x)@V2h)))))@V1l)))))))))))).
thf(conj_thm_2Esorting_2EPERM__QSORT3,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1R:$i] : ((mem@V1R@(arr@A_27a@(arr@A_27a@bool))) => (p@(ap@(ap@(c_2Esorting_2EPERM@A_27a)@V0l)@(ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V1R)@V0l))))))))).
thf(conj_thm_2Esorting_2ESORTED__EQ__PART,lemma,( ! [A_27a:del]: ( ! [V0hd:$i] : ((mem@V0hd@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2R:$i] : ((mem@V2R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V2R)) => (p@(ap@(ap@(c_2Esorting_2ESORTED@A_27a)@V2R)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V2R@V3x)@V0hd))@(ap@(ap@V2R@V0hd)@V3x)))))@V1l)))))))))))).
thf(conj_thm_2Esorting_2EQSORT3__SORTS,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Etotal@A_27a)@V0R))) => (p@(ap@(ap@(c_2Esorting_2ESORTS@A_27a)@(c_2Esorting_2EQSORT3@A_27a))@V0R))))))).
thf(conj_thm_2Esorting_2EQSORT3__SPLIT,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Etotal@A_27a)@V0R))) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V0R)@V1l) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V0R)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V0R@V3x)@V2e))@(ap@c_2Ebool_2E_7E@(ap@(ap@V0R@V2e)@V3x))))))@V1l)))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@V0R@V4x)@V2e))@(ap@(ap@V0R@V2e)@V4x)))))@V1l)))@(ap@(ap@(c_2Esorting_2EQSORT3@A_27a)@V0R)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@c_2Ebool_2E_7E@(ap@(ap@V0R@V5x)@V2e)))))@V1l))))))))))))).
thf(conj_thm_2Esorting_2EQSORT3__STABLE,conjecture,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => (((p@(ap@(c_2Erelation_2Etransitive@A_27a)@V0R)) & (p@(ap@(c_2Erelation_2Etotal@A_27a)@V0R))) => (p@(ap@(ap@(c_2Esorting_2ESTABLE@A_27a)@(c_2Esorting_2EQSORT3@A_27a))@V0R))))))).
