include('Axioms/gcdset+2.ax').
fof(mem_c_2Eset__relation_2ERREFL__EXP,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2ERREFL__EXP(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(arr(A_27a,bool),arr(A_27a,arr(A_27a,bool))))) ) )).
fof(mem_c_2Eset__relation_2ERRUNIV,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2ERRUNIV(A_27a),arr(arr(A_27a,bool),arr(A_27a,arr(A_27a,bool)))) ) )).
fof(mem_c_2Eset__relation_2Eacyclic,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eacyclic(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) ) )).
fof(mem_c_2Eset__relation_2Eall__choices,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eall__choices(A_27a),arr(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Eantisym,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eantisym(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) ) )).
fof(mem_c_2Eset__relation_2Echain,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Echain(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Edomain,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eset__relation_2Edomain(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(A_27a,bool))) ) ) )).
fof(mem_c_2Eset__relation_2Efchains,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Efchains(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Efinite__prefixes,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(arr(A_27b,bool),bool))) ) ) )).
fof(mem_c_2Eset__relation_2Eget__min,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eget__min(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),ty_2Eoption_2Eoption(A_27a)))) ) )).
fof(mem_c_2Eset__relation_2Eirreflexive,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eirreflexive(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Elinear__order,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Elinear__order(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Emaximal__elements,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Emaximal__elements(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(A_27a,bool)))) ) )).
fof(mem_c_2Eset__relation_2Eminimal__elements,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eminimal__elements(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(A_27a,bool)))) ) )).
fof(mem_c_2Eset__relation_2Enth__min,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Enth__min(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),arr(ty_2Enum_2Enum,ty_2Eoption_2Eoption(A_27a))))) ) )).
fof(mem_c_2Eset__relation_2Enum__order,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Enum__order(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)))) ) )).
fof(mem_c_2Eset__relation_2Epartial__order,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Epartial__order(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Eper,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eper(A_27a),arr(arr(A_27a,bool),arr(arr(arr(A_27a,bool),bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Eper__restrict,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Eper__restrict(A_27a),arr(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),arr(arr(A_27a,bool),bool)))) ) )).
fof(mem_c_2Eset__relation_2Erange,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eset__relation_2Erange(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27b,A_27a),bool),arr(A_27a,bool))) ) ) )).
fof(mem_c_2Eset__relation_2Ercomp,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),arr(arr(ty_2Epair_2Eprod(A_27a,A_27c),bool),arr(arr(ty_2Epair_2Eprod(A_27c,A_27b),bool),arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)))) ) ) ) )).
fof(mem_c_2Eset__relation_2Ereflexive,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Ereflexive(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Erel__to__reln,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,bool)),arr(ty_2Epair_2Eprod(A_27a,A_27b),bool))) ) ) )).
fof(mem_c_2Eset__relation_2Ereln__to__rel,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(A_27a,arr(A_27b,bool)))) ) ) )).
fof(mem_c_2Eset__relation_2Errestrict,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Errestrict(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)))) ) )).
fof(mem_c_2Eset__relation_2Estrict,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Estrict(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))) ) )).
fof(mem_c_2Eset__relation_2Estrict__linear__order,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Estrict__linear__order(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Eset__relation_2Etc,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Etc(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))) ) )).
fof(mem_c_2Eset__relation_2Etransitive,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Etransitive(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) ) )).
fof(mem_c_2Eset__relation_2Euniv__reln,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eset__relation_2Euniv__reln(A_27a),arr(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))) ) )).
fof(mem_c_2Eset__relation_2Eupper__bounds,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eset__relation_2Eupper__bounds(A_27a,A_27b),arr(arr(A_27b,bool),arr(arr(ty_2Epair_2Eprod(A_27b,A_27a),bool),arr(A_27a,bool)))) ) ) )).
fof(conj_thm_2Eset__relation_2Erextension,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0s] : ( mem(V0s,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1t] : ( mem(V1t,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ( V0s = V1t ) <=> ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),V0s)) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),V1t)) ) ) ) ) ) ))))).
fof(ax_thm_2Eset__relation_2Edomain__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V0r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f318(A_27b,A_27a,V0r)) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Erange__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => ( ap(c_2Eset__relation_2Erange(A_27a,A_27b),V0r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f320(A_27b,A_27a,V0r)) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Ein__domain,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V1r))) <=> ? [V2y] : ( mem(V2y,A_27b) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V2y)),V1r)) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Ein__range,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0y] : ( mem(V0y,A_27a) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0y),ap(c_2Eset__relation_2Erange(A_27a,A_27b),V1r))) <=> ? [V2x] : ( mem(V2x,A_27b) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V2x),V0y)),V1r)) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Ein__dom__rg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27b) => ! [V2r] : ( mem(V2r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y)),V2r)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V2r))) & p(ap(ap(c_2Ebool_2EIN(A_27b),V1y),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V2r))) ) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Edomain__mono,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1r_27] : ( mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V0r),V1r_27)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V0r)),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V1r_27))) ) ) ))))).
fof(conj_thm_2Eset__relation_2Erange__mono,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1r_27] : ( mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V0r),V1r_27)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V1r_27))) ) ) ))))).
fof(ax_thm_2Eset__relation_2Errestrict__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f322(A_27a,V1s,V0r))) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Ein__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2r] : ( mem(V2r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V3s] : ( mem(V3s,arr(A_27a,bool)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V2r),V3s))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),V2r)) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),V3s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V1y),V3s)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Ein__rrestrict__alt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Epair_2Eprod(A_27a,A_27a)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),V0x),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r),V2s))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),V0x),V1r)) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),ap(c_2Epair_2EFST(A_27a,A_27a),V0x)),V2s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),ap(c_2Epair_2ESND(A_27a,A_27a),V0x)),V2s)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Errestrict__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)),V0r)) ) )))).
fof(conj_thm_2Eset__relation_2Errestrict__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r1),V1r2)),V2s) = ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r1),V2s)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r2),V2s)) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Errestrict__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,arr(A_27a,bool)) => ! [V2y] : ( mem(V2y,arr(A_27a,bool)) => ( ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1x)),V2y) = ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),ap(ap(c_2Epred__set_2EINTER(A_27a),V1x),V2y)) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Edomain__rrestrict__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))),V1s)) ) )))).
fof(conj_thm_2Eset__relation_2Erange__rrestrict__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))),V1s)) ) )))).
fof(ax_thm_2Eset__relation_2Ercomp__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27c,A_27b),bool)) => ( ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),V0r1),V1r2) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),bool)),f325(A_27c,A_27a,A_27b,V0r1,V1r2))) ) ) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Estrict__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(c_2Eset__relation_2Estrict(A_27a),V0r) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f327(A_27a,V0r))) ) ) ) )).
fof(conj_thm_2Eset__relation_2Estrict__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ap(c_2Eset__relation_2Estrict(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)) = ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r)),V1s) ) ) )))).
fof(ax_thm_2Eset__relation_2Euniv__reln__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0xs] : ( mem(V0xs,arr(A_27a,bool)) => ( ap(c_2Eset__relation_2Euniv__reln(A_27a),V0xs) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f329(A_27a,V0xs))) ) ) ) )).
fof(ax_thm_2Eset__relation_2Efinite__prefixes__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1s] : ( mem(V1s,arr(A_27b,bool)) => ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) <=> ! [V2e] : ( mem(V2e,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V2e),V1s)) => p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f330(A_27b,A_27a,V0r,V2e)))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__subset__s,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1s] : ( mem(V1s,arr(A_27b,bool)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27b,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V2s_27),V1s)) ) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V2s_27)) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__subset__r,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1r_27] : ( mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V2s] : ( mem(V2s,arr(A_27b,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V2s)) & p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V1r_27),V0r)) ) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V1r_27),V2s)) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__subset__rs,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1s] : ( mem(V1s,arr(A_27b,bool)) => ! [V2r_27] : ( mem(V2r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V3s_27] : ( mem(V3s_27,arr(A_27b,bool)) => ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V2r_27),V0r)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V3s_27),V1s)) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V2r_27),V3s_27)) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27a,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2s_27),V1s)) ) => ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V0r),V2s_27)) & p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V2s_27)),V2s_27)) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__union,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V2s1] : ( mem(V2s1,arr(A_27b,bool)) => ! [V3s2] : ( mem(V3s2,arr(A_27b,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r1),V2s1)) & p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V1r2),V3s2)) ) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27b)),V0r1),V1r2)),ap(ap(c_2Epred__set_2EINTER(A_27b),V2s1),V3s2))) ) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__comp,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27b,A_27c),bool)) => ! [V2s1] : ( mem(V2s1,arr(A_27b,bool)) => ! [V3s2] : ( mem(V3s2,arr(A_27c,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r1),V2s1)) & ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27b,A_27c),V1r2),V3s2)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),ap(c_2Epred__set_2EGSPEC(A_27b,A_27b),f332(A_27c,A_27b,V1r2,V3s2))),V2s1)) ) ) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27c),ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27c,A_27b),V0r1),V1r2)),V3s2)) ) ) ) ) )))))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__inj__image,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( ( ( ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27a) => ( ( ap(V0f,V3x) = ap(V0f,V4y) ) => ( V3x = V4y ) ) ) ) ) & p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V1r),V2s)) ) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27b,A_27b),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27b,A_27b),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27b,A_27b),bool)),f334(A_27b,A_27a,V0f,V1r)))),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),V2s))) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Efinite__prefixes__range,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1s] : ( mem(V1s,arr(A_27b,bool)) => ! [V2t] : ( mem(V2t,arr(A_27b,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27b),V2t),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V0r))) ) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),ap(ap(c_2Epred__set_2EUNION(A_27b),V1s),V2t))) ) ) ) ))))).
fof(ax_thm_2Eset__relation_2Etc__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Eset__relation_2Etc(A_27a) = f343(A_27a) ) ) )).
fof(conj_thm_2Eset__relation_2Etc__rules,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) ) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27a) => ( ( ? [V5z] : ( mem(V5z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V5z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V5z),V4y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V4y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__cases,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) | ? [V3z] : ( mem(V3z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3z),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ? [V6z] : ( mem(V6z,A_27a) & ( p(ap(ap(V1tc_27,V4x),V6z)) & p(ap(ap(V1tc_27,V6z),V5y)) ) ) ) => p(ap(ap(V1tc_27,V4x),V5y)) ) ) ) ) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__closure,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),ap(c_2Eset__relation_2Etc(A_27a),V1s))) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Eset__relation_2Etc(A_27a),V0r)),ap(c_2Eset__relation_2Etc(A_27a),V1s))) ) ) )))).
fof(conj_thm_2Eset__relation_2Esubset__tc,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),ap(c_2Eset__relation_2Etc(A_27a),V0r))) )))).
fof(conj_thm_2Eset__relation_2Etc__idemp,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(c_2Eset__relation_2Etc(A_27a),ap(c_2Eset__relation_2Etc(A_27a),V0r)) = ap(c_2Eset__relation_2Etc(A_27a),V0r) ) )))).
fof(conj_thm_2Eset__relation_2Etc__mono,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),V1s)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Eset__relation_2Etc(A_27a),V0r)),ap(c_2Eset__relation_2Etc(A_27a),V1s))) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__strongind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ? [V6z] : ( mem(V6z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & ( p(ap(ap(V1tc_27,V4x),V6z)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(V1tc_27,V6z),V5y)) ) ) ) ) ) => p(ap(ap(V1tc_27,V4x),V5y)) ) ) ) ) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__cases__right,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) | ? [V3z] : ( mem(V3z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3z),V2y)),V0r)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__cases__left,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) | ? [V3z] : ( mem(V3z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),V0r)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3z),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__ind__left,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ? [V6z] : ( mem(V6z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),V0r)) & p(ap(ap(V1tc_27,V6z),V5y)) ) ) ) => p(ap(ap(V1tc_27,V4x),V5y)) ) ) ) ) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__strongind__left,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ? [V6z] : ( mem(V6z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),V0r)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(V1tc_27,V6z),V5y)) ) ) ) ) => p(ap(ap(V1tc_27,V4x),V5y)) ) ) ) ) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__ind__right,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ? [V6z] : ( mem(V6z,A_27a) & ( p(ap(ap(V1tc_27,V4x),V6z)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),V0r)) ) ) ) => p(ap(ap(V1tc_27,V4x),V5y)) ) ) ) ) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Ertc__ind__right,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r))) | p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))) ) => p(ap(ap(V1tc_27,V2x),V2x)) ) ) ) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27a) => ( ( ? [V5z] : ( mem(V5z,A_27a) & ( p(ap(ap(V1tc_27,V3x),V5z)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V5z),V4y)),V0r)) ) ) ) => p(ap(ap(V1tc_27,V3x),V4y)) ) ) ) ) => ! [V6x] : ( mem(V6x,A_27a) => ! [V7y] : ( mem(V7y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6x),V7y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V6x),V7y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__strongind__right,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1tc_27] : ( mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ? [V6z] : ( mem(V6z,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & ( p(ap(ap(V1tc_27,V4x),V6z)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),V0r)) ) ) ) ) => p(ap(ap(V1tc_27,V4x),V5y)) ) ) ) ) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8y] : ( mem(V8y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r1))) => ! [V3r2] : ( mem(V3r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r1),V3r2)))) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__implication,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r1)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V1r2)) ) ) ) ) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V0r1))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V1r2))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__empty,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Etc(A_27a),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))))) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__empty__eqn,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Eset__relation_2Etc(A_27a),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))) = c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a)) )))).
fof(conj_thm_2Eset__relation_2Etc__domain__range,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2y),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Errestrict__tc,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,arr(A_27a,bool)) => ! [V2e] : ( mem(V2e,A_27a) => ! [V3e_27] : ( mem(V3e_27,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2e),V3e_27)),ap(c_2Eset__relation_2Etc(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1x)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2e),V3e_27)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__SWAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(c_2Eset__relation_2Etc(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),V0r)) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),ap(c_2Eset__relation_2Etc(A_27a),V0r)) ) )))).
fof(ax_thm_2Eset__relation_2Eacyclic__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) <=> ! [V1x] : ( mem(V1x,A_27a) => ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V1x)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) ) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Eacyclic__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r1)) & p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V1r2),V0r1)) ) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r2)) ) ) )))).
fof(conj_thm_2Eset__relation_2Eacyclic__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))) ) ) )))).
fof(conj_thm_2Eset__relation_2Eacyclic__irreflexive,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) => ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V1x)),V0r)) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Eacyclic__SWAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),V0r))) <=> p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) ) )))).
fof(conj_thm_2Eset__relation_2Eacyclic__bigunion,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0rs] : ( mem(V0rs,arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) => ( ( ( ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2r_27] : ( mem(V2r_27,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(ap(c_2Ebool_2EIN(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),V1r),V0rs)) & ( p(ap(ap(c_2Ebool_2EIN(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),V2r_27),V0rs)) & ( ~~ ( V1r = V2r_27 ) ) ) ) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r))),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V2r_27)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V2r_27)))) ) ) ) ) & ! [V3r] : ( mem(V3r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Ebool_2EIN(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),V3r),V0rs)) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),V3r)) ) ) ) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(c_2Epred__set_2EBIGUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0rs))) ) )))).
fof(conj_thm_2Eset__relation_2Eacyclic__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r_27] : ( mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r_27)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r_27)))) & ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) & p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r_27)) ) ) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),V1r_27))) ) ) )))).
fof(ax_thm_2Eset__relation_2Ereflexive__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),V1s)) <=> ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0r)) ) ) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Eirreflexive__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V0r),V1s)) <=> ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0r)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Etransitive__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) <=> ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ! [V3z] : ( mem(V3z,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2y),V3z)),V0r)) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),V0r)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Etransitive__tc,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) => ( ap(c_2Eset__relation_2Etc(A_27a),V0r) = V0r ) ) )))).
fof(conj_thm_2Eset__relation_2Etc__transitive,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(c_2Eset__relation_2Etransitive(A_27a),ap(c_2Eset__relation_2Etc(A_27a),V0r))) )))).
fof(ax_thm_2Eset__relation_2Eantisym__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) <=> ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2y),V1x)),V0r)) ) => ( V1x = V2y ) ) ) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Epartial__order__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) <=> ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),V1s)) & ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)),V1s)) & ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & ( p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),V1s)) & p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Eantisym__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V0t)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V1s),V0t)) => p(ap(c_2Eset__relation_2Eantisym(A_27a),V1s)) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Epartial__order__dom__rng,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) & p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) ) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Epartial__order__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27a,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2s_27),V1s)) ) => p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V2s_27)),V2s_27)) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Estrict__partial__order,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))),V1s)) & ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))),V1s)) & ( p(ap(c_2Eset__relation_2Etransitive(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))) & p(ap(c_2Eset__relation_2Eantisym(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Estrict__partial__order__acyclic,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))) ) ) )))).
fof(ax_thm_2Eset__relation_2Elinear__order__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) <=> ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),V1s)) & ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)),V1s)) & ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) & ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s)) ) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V2x)),V0r)) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Elinear__order__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27a,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2s_27),V1s)) ) => p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V2s_27)),V2s_27)) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Epartial__order__linear__order,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) => p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) ) ) )))).
fof(ax_thm_2Eset__relation_2Estrict__linear__order__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),V1s)) <=> ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),V1s)) & ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)),V1s)) & ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & ( ( ! [V2x] : ( mem(V2x,A_27a) => ( ~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0r)) ) ) ) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4y),V1s)) & ( ~~ ( V3x = V4y ) ) ) ) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V4y)),V0r)) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4y),V3x)),V0r)) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Estrict__linear__order__dom__rng,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) & p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),V1s)) ) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s)) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Elinear__order__dom__rng,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) & p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) ) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s)) ) ) ) ) ) )))).
fof(ax_thm_2Eset__relation_2Ereln__to__rel__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r) = f344(A_27b,A_27a,V0r) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Erel__to__reln__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V0R) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),bool)),f346(A_27a,A_27b,V0R))) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2ERRUNIV__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( ap(c_2Eset__relation_2ERRUNIV(A_27a),V0s) = f348(A_27a,V0s) ) ) ) )).
fof(ax_thm_2Eset__relation_2ERREFL__EXP__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27a,bool))) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V0R),V1s) = ap(ap(c_2Erelation_2ERUNION(A_27a,A_27a),V0R),f350(A_27a,V1s)) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2ERREFL__EXP__RSUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27a,bool))) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Erelation_2ERSUBSET(A_27a,A_27a),V0R),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V0R),V1s))) ) )))).
fof(conj_thm_2Eset__relation_2ERREFL__EXP__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V0R),c_2Epred__set_2EUNIV(A_27a)) = V0R ) )))).
fof(conj_thm_2Eset__relation_2EREL__RESTRICT__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),V0R),c_2Epred__set_2EUNIV(A_27a)) = V0R ) )))).
fof(conj_thm_2Eset__relation_2Ein__rel__to__reln,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0xy] : ( mem(V0xy,ty_2Epair_2Eprod(A_27a,A_27b)) => ! [V1R] : ( mem(V1R,arr(A_27a,arr(A_27b,bool))) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),V0xy),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R))) <=> p(ap(ap(V1R,ap(c_2Epair_2EFST(A_27a,A_27b),V0xy)),ap(c_2Epair_2ESND(A_27a,A_27b),V0xy))) ) ) ))))).
fof(conj_thm_2Eset__relation_2Ereln__to__rel__app,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27b) => ( p(ap(ap(ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r),V1x),V2y)) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V2y)),V0r)) ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Erel__to__reln__IS__UNCURRY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( c_2Eset__relation_2Erel__to__reln(A_27a,A_27b) = c_2Epair_2EUNCURRY(A_27a,A_27b,bool) ))))).
fof(conj_thm_2Eset__relation_2Ereln__to__rel__IS__CURRY,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b) = c_2Epair_2ECURRY(A_27a,A_27b,bool) ))))).
fof(conj_thm_2Eset__relation_2Erel__to__reln__inv,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V0R)) = V0R ) ))))).
fof(conj_thm_2Eset__relation_2Ereln__to__rel__inv,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r)) = V0r ) ))))).
fof(conj_thm_2Eset__relation_2Ereln__to__rel__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ( ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r1) = ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V1r2) ) <=> ( V0r1 = V1r2 ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Erel__to__reln__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R1] : ( mem(V0R1,arr(A_27a,arr(A_27b,bool))) => ! [V1R2] : ( mem(V1R2,arr(A_27a,arr(A_27b,bool))) => ( ( ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V0R1) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R2) ) <=> ( V0R1 = V1R2 ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Erel__to__reln__swap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V1R] : ( mem(V1R,arr(A_27a,arr(A_27b,bool))) => ( ( V0r = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R) ) <=> ( ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r) = V1R ) ) ) ))))).
fof(conj_thm_2Eset__relation_2Edomain__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V0r) = ap(c_2Erelation_2ERDOM(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r)) ) ))))).
fof(conj_thm_2Eset__relation_2Erange__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => ( ap(c_2Eset__relation_2Erange(A_27a,A_27b),V0r) = ap(c_2Erelation_2ERRANGE(A_27b,A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27b,A_27a),V0r)) ) ))))).
fof(conj_thm_2Eset__relation_2Estrict__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(c_2Eset__relation_2Estrict(A_27a),V0r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ESTRORD(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Errestrict__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s)) ) ) )))).
fof(conj_thm_2Eset__relation_2Ercomp__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27c,A_27b),bool)) => ( ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),V0r1),V1r2) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(ap(c_2Erelation_2EO(A_27a,A_27c,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27c,A_27b),V1r2)),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27c),V0r1))) ) ) )))))).
fof(conj_thm_2Eset__relation_2Euniv__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( ap(c_2Eset__relation_2Euniv__reln(A_27a),V0s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Eset__relation_2ERRUNIV(A_27a),V0s)) ) )))).
fof(conj_thm_2Eset__relation_2Etc__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(c_2Eset__relation_2Etc(A_27a),V0r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Eacyclic__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)))) ) )))).
fof(conj_thm_2Eset__relation_2Eirreflexive__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V0r),V1s)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s))) ) ) )))).
fof(conj_thm_2Eset__relation_2Eirreflexive__reln__to__rel__conv__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Ereflexive__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),V1s)) <=> p(ap(c_2Erelation_2Ereflexive(A_27a),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s))) ) ) )))).
fof(conj_thm_2Eset__relation_2Ereflexive__reln__to__rel__conv__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2Ereflexive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Etransitive__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) <=> p(ap(c_2Erelation_2Etransitive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Eantisym__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) <=> p(ap(c_2Erelation_2Eantisymmetric(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Epartial__order__reln__to__rel__conv,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) <=> ( p(ap(ap(c_2Erelation_2ERSUBSET(A_27a,A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2ERRUNIV(A_27a),V1s))) & p(ap(c_2Erelation_2EWeakOrder(A_27a),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s))) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Epartial__order__reln__to__rel__conv__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Elinear__order__reln__to__rel__conv__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Estrict__linear__order__reln__to__rel__conv__UNIV,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) ) )))).
fof(conj_thm_2Eset__relation_2Ereln__rel__conv__thms,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0xy] : ( mem(V0xy,ty_2Epair_2Eprod(A_27a,A_27b)) => ! [V1R] : ( mem(V1R,arr(A_27a,arr(A_27b,bool))) => ! [V2r] : ( mem(V2r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27b) => ! [V5r1] : ( mem(V5r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V6r2] : ( mem(V6r2,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ! [V7R1] : ( mem(V7R1,arr(A_27a,arr(A_27b,bool))) => ! [V8R2] : ( mem(V8R2,arr(A_27a,arr(A_27b,bool))) => ! [V9R] : ( mem(V9R,arr(A_27a,arr(A_27a,bool))) => ! [V10r] : ( mem(V10r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => ! [V11r] : ( mem(V11r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V12s] : ( mem(V12s,arr(A_27a,bool)) => ! [V13r1] : ( mem(V13r1,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ! [V14r2] : ( mem(V14r2,arr(ty_2Epair_2Eprod(A_27c,A_27b),bool)) => ( ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),V0xy),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R))) <=> p(ap(ap(V1R,ap(c_2Epair_2EFST(A_27a,A_27b),V0xy)),ap(c_2Epair_2ESND(A_27a,A_27b),V0xy))) ) & ( ( p(ap(ap(ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V2r),V3x),V4y)) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V4y)),V2r)) ) & ( ( ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R)) = V1R ) & ( ( ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V2r)) = V2r ) & ( ( ( ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V5r1) = ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V6r2) ) <=> ( V5r1 = V6r2 ) ) & ( ( ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V7R1) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V8R2) ) <=> ( V7R1 = V8R2 ) ) ) ) ) ) ) & ( ( ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V9R),c_2Epred__set_2EUNIV(A_27a)) = V9R ) & ( ( ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),V9R),c_2Epred__set_2EUNIV(A_27a)) = V9R ) & ( ( ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V2r) = ap(c_2Erelation_2ERDOM(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V2r)) ) & ( ( ap(c_2Eset__relation_2Erange(A_27a,A_27b),V10r) = ap(c_2Erelation_2ERRANGE(A_27b,A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27b,A_27a),V10r)) ) & ( ( ap(c_2Eset__relation_2Estrict(A_27a),V11r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ESTRORD(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) & ( ( ap(ap(c_2Eset__relation_2Errestrict(A_27a),V11r),V12s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)),V12s)) ) & ( ( ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),V13r1),V14r2) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(ap(c_2Erelation_2EO(A_27a,A_27c,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27c,A_27b),V14r2)),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27c),V13r1))) ) & ( ( ap(c_2Eset__relation_2Euniv__reln(A_27a),V12s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Eset__relation_2ERRUNIV(A_27a),V12s)) ) & ( ( ap(c_2Eset__relation_2Etc(A_27a),V11r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) & ( ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V11r)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) ) & ( ( p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V11r),V12s)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)),V12s))) ) & ( ( p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V11r),V12s)) <=> p(ap(c_2Erelation_2Ereflexive(A_27a),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)),V12s))) ) & ( ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V11r)) <=> p(ap(c_2Erelation_2Etransitive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) & ( ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V11r)) <=> p(ap(c_2Erelation_2Eantisymmetric(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) & ( ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V11r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) & ( ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V11r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) & ( p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V11r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )))))).
fof(conj_thm_2Eset__relation_2Eacyclic__WF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) & ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),V0s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r)),V0s)) ) ) ) => p(ap(c_2Erelation_2EWF(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V1r))) ) ) )))).
fof(ax_thm_2Eset__relation_2Emaximal__elements__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0xs] : ( mem(V0xs,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0xs),V1r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f352(A_27a,V0xs,V1r)) ) ) ) ) )).
fof(ax_thm_2Eset__relation_2Eminimal__elements__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0xs] : ( mem(V0xs,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),V1r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f354(A_27a,V0xs,V1r)) ) ) ) ) )).
fof(conj_thm_2Eset__relation_2Eminimal__elements__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1lo] : ( mem(V1lo,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1lo)),V0s)) ) )))).
fof(conj_thm_2Eset__relation_2Eminimal__elements__SWAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0xs] : ( mem(V0xs,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),V1r)) = ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0xs),V1r) ) ) )))).
fof(conj_thm_2Eset__relation_2Emaximal__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2r1] : ( mem(V2r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V3r2] : ( mem(V3r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V1s),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V2r1),V3r2)))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V1s),V2r1))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V1s),V3r2))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Eminimal__union,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2r1] : ( mem(V2r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V3r2] : ( mem(V3r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V1s),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V2r1),V3r2)))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V1s),V2r1))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V1s),V3r2))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Eminimal__elements__mono,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r_27] : ( mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2xs] : ( mem(V2xs,arr(A_27a,bool)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),V1r_27)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V2xs),V1r_27)),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V2xs),V0r))) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Eminimal__elements__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0xs] : ( mem(V0xs,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r),V0xs)) = ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),V1r) ) ) )))).
fof(conj_thm_2Eset__relation_2EWF__has__minimal__path,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( p(ap(c_2Erelation_2EWF(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V2s)) => ? [V3y] : ( mem(V3y,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V2s),V0r))) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V1x)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) | ( V3y = V1x ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Efinite__acyclic__has__maximal,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ( ( ~~ ( V0s = c_2Epred__set_2EEMPTY(A_27a) ) ) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) => ? [V2x] : ( mem(V2x,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),V1r))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Efinite__acyclic__has__minimal,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ( ( ~~ ( V0s = c_2Epred__set_2EEMPTY(A_27a) ) ) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) => ? [V2x] : ( mem(V2x,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Emaximal__TC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),V0s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r)),V0s)) ) => ( ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),ap(c_2Eset__relation_2Etc(A_27a),V1r)) = ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),V1r) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Eminimal__TC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),V0s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r)),V0s)) ) => ( ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),ap(c_2Eset__relation_2Etc(A_27a),V1r)) = ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Efinite__acyclic__has__minimal__path,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s)) & ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r))) ) ) ) ) => ? [V3y] : ( mem(V3y,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V2x)),ap(c_2Eset__relation_2Etc(A_27a),V1r))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Efinite__acyclic__has__maximal__path,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & ( p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s)) & ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),V1r))) ) ) ) ) => ? [V3y] : ( mem(V3y,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),V1r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),ap(c_2Eset__relation_2Etc(A_27a),V1r))) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Efinite__prefix__po__has__minimal__path,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3s_27] : ( mem(V3s_27,arr(A_27a,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) & ( p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V0r),V1s)) & ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V3s_27),V0r))) ) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V3s_27)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V3s_27),V1s)) ) ) ) ) => ? [V4x_27] : ( mem(V4x_27,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x_27),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V3s_27),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x_27),V2x)),V0r)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Eempty__strict__linear__order,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),c_2Epred__set_2EEMPTY(A_27a))) <=> ( V0r = c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a)) ) ) )))).
fof(conj_thm_2Eset__relation_2Eempty__linear__order,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),c_2Epred__set_2EEMPTY(A_27a))) <=> ( V0r = c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a)) ) ) )))).
fof(conj_thm_2Eset__relation_2Elinear__order__restrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V1r),V0s)) => p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r),V2s_27)),ap(ap(c_2Epred__set_2EINTER(A_27a),V0s),V2s_27))) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Estrict__linear__order__restrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V2s_27] : ( mem(V2s_27,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V1r),V0s)) => p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r),V2s_27)),ap(ap(c_2Epred__set_2EINTER(A_27a),V0s),V2s_27))) ) ) ) )))).
fof(conj_thm_2Eset__relation_2Elinear__order__dom__rg,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0lo] : ( mem(V0lo,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1X] : ( mem(V1X,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0lo),V1X)) => ( ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0lo)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0lo)) = V1X ) ) ) )))).
fof(conj_thm_2Eset__relation_2Elinear__order__refl,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0lo] : ( mem(V0lo,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1X] : ( mem(V1X,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0lo),V1X)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1X)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0lo)) ) ) ) ) )))).
