include('Axioms/bft+2.ax').
fof(ne_ty_2Epath_2Epath,axiom,( ! [A0] : ( ne(A0) => ( ! [A1] : ( ne(A1) => ne(ty_2Epath_2Epath(A0,A1)) ) ) ) )).
fof(mem_c_2Epath_2EPL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2EPL(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Enum_2Enum,bool))) ) ) )).
fof(mem_c_2Epath_2ESN,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2ESN(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,arr(A_27a,bool))),bool)) ) ) )).
fof(mem_c_2Epath_2Edrop,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Edrop(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Epath_2Eel,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eel(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),A_27a))) ) ) )).
fof(mem_c_2Epath_2Eevery,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eevery(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))) ) ) )).
fof(mem_c_2Epath_2Eexists,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eexists(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))) ) ) )).
fof(mem_c_2Epath_2Efilter,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Efilter(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Epath_2Efinite,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Efinite(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) ) ) )).
fof(mem_c_2Epath_2Efirst,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Efirst(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),A_27a)) ) ) )).
fof(mem_c_2Epath_2EfirstP__at,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2EfirstP__at(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Enum_2Enum,bool)))) ) ) )).
fof(mem_c_2Epath_2Efirst__label,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Efirst__label(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),A_27b)) ) ) )).
fof(mem_c_2Epath_2EfromPath,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2EfromPath(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))))) ) ) )).
fof(mem_c_2Epath_2Eis__stopped,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eis__stopped(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) ) ) )).
fof(mem_c_2Epath_2Elabels,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Elabels(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Ellist_2Ellist(A_27b))) ) ) )).
fof(mem_c_2Epath_2Elast,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Elast(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),A_27a)) ) ) )).
fof(mem_c_2Epath_2Elength,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Elength(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Eoption_2Eoption(ty_2Enum_2Enum))) ) ) )).
fof(mem_c_2Epath_2Emem,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Emem(A_27a,A_27b),arr(A_27a,arr(ty_2Epath_2Epath(A_27a,A_27b),bool))) ) ) )).
fof(mem_c_2Epath_2Enth__label,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Enth__label(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27b,A_27a),A_27a))) ) ) )).
fof(mem_c_2Epath_2Eokpath,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eokpath(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,arr(A_27a,bool))),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))) ) ) )).
fof(mem_c_2Epath_2Eokpath__f,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eokpath__f(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,arr(A_27a,bool))),arr(arr(ty_2Epath_2Epath(A_27a,A_27b),bool),arr(ty_2Epath_2Epath(A_27a,A_27b),bool)))) ) ) )).
fof(mem_c_2Epath_2Eparallel__comp,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [A_27d] : ( ne(A_27d) => ! [A_27e] : ( ne(A_27e) => mem(c_2Epath_2Eparallel__comp(A_27a,A_27b,A_27c,A_27d,A_27e),arr(arr(A_27a,arr(A_27b,arr(A_27c,bool))),arr(arr(A_27d,arr(A_27b,arr(A_27e,bool))),arr(ty_2Epair_2Eprod(A_27a,A_27d),arr(A_27b,arr(ty_2Epair_2Eprod(A_27c,A_27e),bool)))))) ) ) ) ) ) )).
fof(mem_c_2Epath_2Epconcat,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Epconcat(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(A_27b,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Epath_2Epcons,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Epcons(A_27a,A_27b),arr(A_27a,arr(A_27b,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Epath_2Epgenerate,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Epgenerate(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,A_27a),arr(arr(ty_2Enum_2Enum,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Epath_2Eplink,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eplink(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Epath_2Epmap,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [A_27d] : ( ne(A_27d) => mem(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),arr(arr(A_27a,A_27c),arr(arr(A_27b,A_27d),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27c,A_27d))))) ) ) ) ) )).
fof(mem_c_2Epath_2Eseg,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Eseg(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))) ) ) )).
fof(mem_c_2Epath_2Estopped__at,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Estopped__at(A_27a,A_27b),arr(A_27a,ty_2Epath_2Epath(A_27a,A_27b))) ) ) )).
fof(mem_c_2Epath_2Etail,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Etail(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))) ) ) )).
fof(mem_c_2Epath_2Etake,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2Etake(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Epath_2EtoPath,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Epath_2EtoPath(A_27a,A_27b),arr(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ty_2Epath_2Epath(A_27a,A_27b))) ) ) )).
fof(mem_c_2Epath_2Etrace__machine,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Epath_2Etrace__machine(A_27a),arr(arr(ty_2Elist_2Elist(A_27a),bool),arr(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),bool))))) ) )).
fof(mem_c_2Epath_2Eunfold,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Epath_2Eunfold(A_27a,A_27b,A_27c),arr(arr(A_27c,A_27a),arr(arr(A_27c,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))),arr(A_27c,ty_2Epath_2Epath(A_27a,A_27b))))) ) ) ) )).
fof(ax_thm_2Epath_2Epath__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ? [V0rep] : ( mem(V0rep,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ty_2Epath_2Epath(A_27a,A_27b)),k(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),c_2Ebool_2ET)),V0rep)) ) ) ) )).
fof(ax_thm_2Epath_2Epath__absrep__bijections,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0a] : ( mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ( p(ap(k(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),c_2Ebool_2ET),V1r)) <=> ( ap(c_2Epath_2EfromPath(A_27a,A_27b),ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r)) = V1r ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Epath__rep__bijections__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0a] : ( mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ( ap(c_2Epath_2EfromPath(A_27a,A_27b),ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r)) = V1r ) ) ))))).
fof(conj_thm_2Epath_2EtoPath__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ! [V1r_27] : ( mem(V1r_27,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ( ( ap(c_2Epath_2EtoPath(A_27a,A_27b),V0r) = ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r_27) ) <=> ( V0r = V1r_27 ) ) ) ))))).
fof(conj_thm_2Epath_2EfromPath__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0a] : ( mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1a_27] : ( mem(V1a_27,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ap(c_2Epath_2EfromPath(A_27a,A_27b),V0a) = ap(c_2Epath_2EfromPath(A_27a,A_27b),V1a_27) ) <=> ( V0a = V1a_27 ) ) ) ))))).
fof(conj_thm_2Epath_2EfromPath__onto,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ? [V1a] : ( mem(V1a,ty_2Epath_2Epath(A_27a,A_27b)) & ( V0r = ap(c_2Epath_2EfromPath(A_27a,A_27b),V1a) ) ) ))))).
fof(conj_thm_2Epath_2EtoPath__onto,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0a] : ( mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => ? [V1r] : ( mem(V1r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) & ( V0a = ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r) ) ) ))))).
fof(ax_thm_2Epath_2Efirst__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Efirst(A_27a,A_27b),V0p) = ap(c_2Epair_2EFST(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0p)) ) ) ) ) )).
fof(ax_thm_2Epath_2Estopped__at__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) = ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),V0x),c_2Ellist_2ELNIL(ty_2Epair_2Eprod(A_27b,A_27a)))) ) ) ) ) )).
fof(ax_thm_2Epath_2Epcons__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,A_27b) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) = ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),V0x),ap(ap(c_2Ellist_2ELCONS(ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V1r),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p))),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V2p))))) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Estopped__at__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( ( ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1y) ) <=> ( V0x = V1y ) ) ) ))))).
fof(conj_thm_2Epath_2Epcons__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,A_27b) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V3y] : ( mem(V3y,A_27a) => ! [V4s] : ( mem(V4s,A_27b) => ! [V5q] : ( mem(V5q,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3y),V4s),V5q) ) <=> ( ( V0x = V3y ) & ( ( V1r = V4s ) & ( V2p = V5q ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Estopped__at__not__pcons,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2r] : ( mem(V2r,A_27b) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ~~ ( ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1y),V2r),V3p) ) ) & ( ~~ ( ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1y),V2r),V3p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Epath__cases,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ? [V1x] : ( mem(V1x,A_27a) & ( V0p = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x) ) ) ) | ? [V2x] : ( mem(V2x,A_27a) & ? [V3r] : ( mem(V3r,A_27b) & ? [V4q] : ( mem(V4q,ty_2Epath_2Epath(A_27a,A_27b)) & ( V0p = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),V4q) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2EFORALL__path,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ( ( ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => p(ap(V0P,V1p)) ) ) <=> ( ( ! [V2x] : ( mem(V2x,A_27a) => p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))) ) ) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,A_27b) => ! [V5p] : ( mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) => p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2EEXISTS__path,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ( ( ? [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) & p(ap(V0P,V1p)) ) ) <=> ( ( ? [V2x] : ( mem(V2x,A_27a) & p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))) ) ) | ? [V3x] : ( mem(V3x,A_27a) & ? [V4r] : ( mem(V4r,A_27b) & ? [V5p] : ( mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) & p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Efirst__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2Efirst(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = V0x ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2r] : ( mem(V2r,A_27b) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p)) = V1x ) ) ) ) ))))).
fof(ax_thm_2Epath_2Efinite__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0sigma] : ( mem(V0sigma,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0sigma)) <=> p(ap(c_2Ellist_2ELFINITE(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0sigma)))) ) ) ) ) )).
fof(conj_thm_2Epath_2Efinite__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) <=> $true ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2r] : ( mem(V2r,A_27b) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p))) <=> p(ap(c_2Epath_2Efinite(A_27a,A_27b),V3p)) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Elast__thm,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2Elast(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = V0x ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2r] : ( mem(V2r,A_27b) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Elast(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p)) = ap(c_2Epath_2Elast(A_27a,A_27b),V3p) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Epath__bisimulation,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p1] : ( mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1p2] : ( mem(V1p2,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( V0p1 = V1p2 ) <=> ? [V2R] : ( mem(V2R,arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))) & ( p(ap(ap(V2R,V0p1),V1p2)) & ! [V3q1] : ( mem(V3q1,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V4q2] : ( mem(V4q2,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(V2R,V3q1),V4q2)) => ( ( ? [V5x] : ( mem(V5x,A_27a) & ( ( V3q1 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V5x) ) & ( V4q2 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V5x) ) ) ) ) | ? [V6x] : ( mem(V6x,A_27a) & ? [V7r] : ( mem(V7r,A_27b) & ? [V8q1_27] : ( mem(V8q1_27,ty_2Epath_2Epath(A_27a,A_27b)) & ? [V9q2_27] : ( mem(V9q2_27,ty_2Epath_2Epath(A_27a,A_27b)) & ( ( V3q1 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V6x),V7r),V8q1_27) ) & ( ( V4q2 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V6x),V7r),V9q2_27) ) & p(ap(ap(V2R,V8q1_27),V9q2_27)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Efinite__path__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ( ( ( ! [V1x] : ( mem(V1x,A_27a) => p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))) ) ) & ! [V2x] : ( mem(V2x,A_27a) => ! [V3r] : ( mem(V3r,A_27b) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),V4p)) & p(ap(V0P,V4p)) ) => p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),V4p))) ) ) ) ) ) => ! [V5q] : ( mem(V5q,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),V5q)) => p(ap(V0P,V5q)) ) ) ) ))))).
fof(ax_thm_2Epath_2Epmap__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => ! [A_27d] : ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27b,A_27d)) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p) = ap(c_2Epath_2EtoPath(A_27c,A_27d),ap(ap(ap(c_2Epair_2E_23_23(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)),A_27c,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27d,A_27c))),V0f),ap(c_2Ellist_2ELMAP(ty_2Epair_2Eprod(A_27b,A_27a),ty_2Epair_2Eprod(A_27d,A_27c)),ap(ap(c_2Epair_2E_23_23(A_27b,A_27a,A_27d,A_27c),V1g),V0f))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V2p))) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Epmap__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,arr(A_27d,A_27c)) => ( ( ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27d,A_27b,A_27c),V0f),V1g),ap(c_2Epath_2Estopped__at(A_27a,A_27d),V2x)) = ap(c_2Epath_2Estopped__at(A_27b,A_27c),ap(V0f,V2x)) ) ) ) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,A_27d) => ! [V5p] : ( mem(V5p,ty_2Epath_2Epath(A_27a,A_27d)) => ( ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27d,A_27b,A_27c),V0f),V1g),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27d),V3x),V4r),V5p)) = ap(ap(ap(c_2Epath_2Epcons(A_27b,A_27c),ap(V0f,V3x)),ap(V1g,V4r)),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27d,A_27b,A_27c),V0f),V1g),V5p)) ) ) ) ) ) ) ))))))).
fof(conj_thm_2Epath_2Efirst__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27b,A_27d)) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Efirst(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p)) = ap(V0f,ap(c_2Epath_2Efirst(A_27a,A_27b),V2p)) ) ) ) ))))))).
fof(conj_thm_2Epath_2Elast__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27b,A_27d)) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),V2p)) => ( ap(c_2Epath_2Elast(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p)) = ap(V0f,ap(c_2Epath_2Elast(A_27a,A_27b),V2p)) ) ) ) ) ))))))).
fof(conj_thm_2Epath_2Efinite__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27b,A_27d)) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Efinite(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p))) <=> p(ap(c_2Epath_2Efinite(A_27a,A_27b),V2p)) ) ) ) ))))))).
fof(ax_thm_2Epath_2Etail__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,A_27b) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Etail(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p)) = V2p ) ) ) ) ) ) )).
fof(ax_thm_2Epath_2Efirst__label__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,A_27b) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Efirst__label(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p)) = V1r ) ) ) ) ) ) )).
fof(ax_thm_2Epath_2Elength__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Elength(A_27a,A_27b),V0p) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Enum_2Enum)),ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)),ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Eoption_2ETHE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Ellist_2EtoList(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0p)))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2Eoption_2ENONE(ty_2Enum_2Enum)) ) ) ) ) )).
fof(conj_thm_2Epath_2Elength__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2Elength(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ! [V1x] : ( mem(V1x,A_27c) => ! [V2r] : ( mem(V2r,A_27d) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27c,A_27d)) => ( ap(c_2Epath_2Elength(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V1x),V2r),V3p)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Enum_2Enum)),ap(c_2Epath_2Efinite(A_27c,A_27d),V3p)),ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Eoption_2ETHE(ty_2Enum_2Enum),ap(c_2Epath_2Elength(A_27c,A_27d),V3p))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),c_2Eoption_2ENONE(ty_2Enum_2Enum)) ) ) ) ) ))))))).
fof(conj_thm_2Epath_2Ealt__length__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2Elength(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ! [V1x] : ( mem(V1x,A_27c) => ! [V2r] : ( mem(V2r,A_27d) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27c,A_27d)) => ( ap(c_2Epath_2Elength(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V1x),V2r),V3p)) = ap(ap(c_2Eoption_2EOPTION__MAP(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Epath_2Elength(A_27c,A_27d),V3p)) ) ) ) ) ))))))).
fof(conj_thm_2Epath_2Elength__never__zero,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ~~ ( ap(c_2Epath_2Elength(A_27a,A_27b),V0p) = ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),c_2Enum_2E0) ) ) ))))).
fof(conj_thm_2Epath_2Efinite__length,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)) <=> ? [V1n] : ( mem(V1n,ty_2Enum_2Enum) & ( ap(c_2Epath_2Elength(A_27a,A_27b),V0p) = ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),V1n) ) ) ) & ( ( ~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)) ) <=> ( ap(c_2Epath_2Elength(A_27a,A_27b),V0p) = c_2Eoption_2ENONE(ty_2Enum_2Enum) ) ) ) ))))).
fof(conj_thm_2Epath_2Elength__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1g] : ( mem(V1g,arr(A_27c,A_27d)) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27c)) => ( ap(c_2Epath_2Elength(A_27b,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27c,A_27b,A_27d),V0f),V1g),V2p)) = ap(c_2Epath_2Elength(A_27a,A_27c),V2p) ) ) ) ))))))).
fof(ax_thm_2Epath_2Eel__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),c_2Enum_2E0),V0p) = ap(c_2Epath_2Efirst(A_27a,A_27b),V0p) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Enum_2ESUC,V1n)),V2p) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),V1n),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Eel__def__compute,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),c_2Enum_2E0),V0p) = ap(c_2Epath_2Efirst(A_27a,A_27b),V0p) ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),V2p) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n))),V4p) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(c_2Epath_2Etail(A_27a,A_27b),V4p)) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Enth__label__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27b,A_27a)) => ( ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),c_2Enum_2E0),V0p) = ap(c_2Epath_2Efirst__label(A_27b,A_27a),V0p) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27b,A_27a)) => ( ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Enum_2ESUC,V1n)),V2p) = ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),V1n),ap(c_2Epath_2Etail(A_27b,A_27a),V2p)) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Enth__label__def__compute,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27b,A_27a)) => ( ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),c_2Enum_2E0),V0p) = ap(c_2Epath_2Efirst__label(A_27b,A_27a),V0p) ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27b,A_27a)) => ( ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),V2p) = ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Epath_2Etail(A_27b,A_27a),V2p)) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27b,A_27a)) => ( ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n))),V4p) = ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(c_2Epath_2Etail(A_27b,A_27a),V4p)) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Epath__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Epair_2Eprod(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))))) => ? [V1g] : ( mem(V1g,arr(A_27a,ty_2Epath_2Epath(A_27b,A_27c))) & ! [V2x] : ( mem(V2x,A_27a) => ( ap(V1g,V2x) = ap(ap(c_2Epair_2Epair__CASE(ty_2Epath_2Epath(A_27b,A_27c),A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),ap(V0f,V2x)),f1683(A_27a,A_27b,A_27c,V1g)) ) ) ) )))))).
fof(ax_thm_2Epath_2Epconcat__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0p1] : ( mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1lab] : ( mem(V1lab,A_27b) => ! [V2p2] : ( mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2) = ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2Efirst(A_27a,A_27b),V0p1)),ap(ap(c_2Ellist_2ELAPPEND(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0p1))),ap(ap(c_2Ellist_2ELCONS(ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V1lab),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p2))),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V2p2)))))) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Epconcat__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ! [V1lab] : ( mem(V1lab,A_27b) => ! [V2p2] : ( mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)),V1lab),V2p2) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1lab),V2p2) ) ) ) ) ) & ! [V3x] : ( mem(V3x,A_27c) => ! [V4r] : ( mem(V4r,A_27d) => ! [V5p] : ( mem(V5p,ty_2Epath_2Epath(A_27c,A_27d)) => ! [V6lab] : ( mem(V6lab,A_27d) => ! [V7p2] : ( mem(V7p2,ty_2Epath_2Epath(A_27c,A_27d)) => ( ap(ap(ap(c_2Epath_2Epconcat(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V3x),V4r),V5p)),V6lab),V7p2) = ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V3x),V4r),ap(ap(ap(c_2Epath_2Epconcat(A_27c,A_27d),V5p),V6lab),V7p2)) ) ) ) ) ) ) ))))))).
fof(conj_thm_2Epath_2Epconcat__eq__stopped,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p1] : ( mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1lab] : ( mem(V1lab,A_27b) => ! [V2p2] : ( mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V3x] : ( mem(V3x,A_27a) => ( ( ~~ ( ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V3x) ) ) & ( ~~ ( ap(c_2Epath_2Estopped__at(A_27a,A_27b),V3x) = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Epconcat__eq__pcons,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,A_27b) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V3p1] : ( mem(V3p1,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V4lab] : ( mem(V4lab,A_27b) => ! [V5p2] : ( mem(V5p2,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ( ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V3p1),V4lab),V5p2) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) ) <=> ( ( ( V4lab = V1r ) & ( ( V3p1 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) ) & ( V2p = V5p2 ) ) ) | ? [V6p1_27] : ( mem(V6p1_27,ty_2Epath_2Epath(A_27a,A_27b)) & ( ( V3p1 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V6p1_27) ) & ( V2p = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V6p1_27),V4lab),V5p2) ) ) ) ) ) & ( ( ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V3p1),V4lab),V5p2) ) <=> ( ( ( V4lab = V1r ) & ( ( V3p1 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) ) & ( V2p = V5p2 ) ) ) | ? [V7p1_27] : ( mem(V7p1_27,ty_2Epath_2Epath(A_27a,A_27b)) & ( ( V3p1 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V7p1_27) ) & ( V2p = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V7p1_27),V4lab),V5p2) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Efinite__pconcat,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p1] : ( mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1lab] : ( mem(V1lab,A_27b) => ! [V2p2] : ( mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2))) <=> ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p1)) & p(ap(c_2Epath_2Efinite(A_27a,A_27b),V2p2)) ) ) ) ) ))))).
fof(ax_thm_2Epath_2EPL__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2EPL(A_27a,A_27b),V0p) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f1684(A_27b,A_27a,V0p)) ) ) ) ) )).
fof(conj_thm_2Epath_2Einfinite__PL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)) ) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1i),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) ) ) ))))).
fof(conj_thm_2Epath_2EPL__pcons,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1r] : ( mem(V1r,A_27b) => ! [V2q] : ( mem(V2q,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2q)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),c_2Enum_2E0),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Epath_2EPL(A_27a,A_27b),V2q))) ) ) ) ))))).
fof(conj_thm_2Epath_2EPL__stopped__at,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),c_2Enum_2E0),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) ) ))))).
fof(conj_thm_2Epath_2EPL__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),c_2Enum_2E0),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2r] : ( mem(V2r,A_27b) => ! [V3q] : ( mem(V3q,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3q)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),c_2Enum_2E0),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Epath_2EPL(A_27a,A_27b),V3q))) ) ) ) ) ))))).
fof(conj_thm_2Epath_2EPL__0,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),c_2Enum_2E0),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) ))))).
fof(conj_thm_2Epath_2EPL__downward__closed,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2j),V0i)) => p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2j),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) ) ) ) ) ))))).
fof(conj_thm_2Epath_2EPL__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27c,A_27a)) => ! [V1g] : ( mem(V1g,arr(A_27d,A_27b)) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27c,A_27d)) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epmap(A_27c,A_27d,A_27a,A_27b),V0f),V1g),V2p)) = ap(c_2Epath_2EPL(A_27c,A_27d),V2p) ) ) ) ))))))).
fof(conj_thm_2Epath_2Eel__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27b,A_27d)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2i),ap(c_2Epath_2EPL(A_27a,A_27b),V3p))) => ( ap(ap(c_2Epath_2Eel(A_27c,A_27d),V2i),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V3p)) = ap(V0f,ap(ap(c_2Epath_2Eel(A_27a,A_27b),V2i),V3p)) ) ) ) ) ) ))))))).
fof(conj_thm_2Epath_2Enth__label__pmap,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27d)) => ! [V1g] : ( mem(V1g,arr(A_27b,A_27c)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(c_2Enum_2ESUC,V2i)),ap(c_2Epath_2EPL(A_27a,A_27b),V3p))) => ( ap(ap(c_2Epath_2Enth__label(A_27c,A_27d),V2i),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27d,A_27c),V0f),V1g),V3p)) = ap(V1g,ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V2i),V3p)) ) ) ) ) ) ))))))).
fof(ax_thm_2Epath_2EfirstP__at__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),V2i)) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) & ( p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),V2i),V1p))) & ! [V3j] : ( mem(V3j,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3j),V2i)) => ( ~~ p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),V3j),V1p))) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2EfirstP__at__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x)),V2n)) <=> ( ( V2n = c_2Enum_2E0 ) & p(ap(V0P,V1x)) ) ) ) ) ) ) & ! [V3P] : ( mem(V3P,arr(A_27a,bool)) => ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6r] : ( mem(V6r,A_27b) => ! [V7p] : ( mem(V7p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V3P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V5x),V6r),V7p)),V4n)) <=> ( ( ( V4n = c_2Enum_2E0 ) & p(ap(V3P,V5x)) ) | ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V4n)) & ( ( ~~ p(ap(V3P,V5x)) ) & p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V3P),V7p),ap(ap(c_2Earithmetic_2E_2D,V4n),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2EfirstP__at__zero,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),c_2Enum_2E0)) <=> p(ap(V0P,ap(c_2Epath_2Efirst(A_27a,A_27b),V1p))) ) ) ))))).
fof(ax_thm_2Epath_2Eexists__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) <=> ? [V2i] : ( mem(V2i,ty_2Enum_2Enum) & p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),V2i)) ) ) ) ) ) ) )).
fof(ax_thm_2Epath_2Eevery__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),V1p)) <=> ( ~~ p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1p)) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Eexists__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ( ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))) <=> p(ap(V0P,V1x)) ) ) ) & ! [V2x] : ( mem(V2x,A_27a) => ! [V3r] : ( mem(V3r,A_27c) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27c)) => ( p(ap(ap(c_2Epath_2Eexists(A_27a,A_27c),V0P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27c),V2x),V3r),V4p))) <=> ( p(ap(V0P,V2x)) | p(ap(ap(c_2Epath_2Eexists(A_27a,A_27c),V0P),V4p)) ) ) ) ) ) ) )))))).
fof(conj_thm_2Epath_2Eevery__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ( ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))) <=> p(ap(V0P,V1x)) ) ) ) & ! [V2x] : ( mem(V2x,A_27a) => ! [V3r] : ( mem(V3r,A_27c) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27c)) => ( p(ap(ap(c_2Epath_2Eevery(A_27a,A_27c),V0P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27c),V2x),V3r),V4p))) <=> ( p(ap(V0P,V2x)) & p(ap(ap(c_2Epath_2Eevery(A_27a,A_27c),V0P),V4p)) ) ) ) ) ) ) )))))).
fof(conj_thm_2Epath_2Enot__every,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ~~ p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),V1p)) ) <=> p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1p)) ) ) ))))).
fof(conj_thm_2Epath_2Enot__exists,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ~~ p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) ) <=> p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1p)) ) ) ))))).
fof(conj_thm_2Epath_2Eexists__el,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) <=> ? [V2i] : ( mem(V2i,ty_2Enum_2Enum) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) & p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),V2i),V1p))) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Eevery__el,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),V1p)) <=> ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),V2i),V1p))) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Eevery__coinduction,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ! [V1Q] : ( mem(V1Q,arr(A_27a,bool)) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))) => p(ap(V1Q,V2x)) ) ) ) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,A_27b) => ! [V5p] : ( mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))) => ( p(ap(V1Q,V3x)) & p(ap(V0P,V5p)) ) ) ) ) ) ) => ! [V6p] : ( mem(V6p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(V0P,V6p)) => p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V1Q),V6p)) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Eexists__induction,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0Q] : ( mem(V0Q,arr(A_27a,bool)) => ! [V1P] : ( mem(V1P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ( ( ( ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(V0Q,V2x)) => p(ap(V1P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))) ) ) ) & ( ( ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,A_27b) => ! [V5p] : ( mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(V0Q,V3x)) => p(ap(V1P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))) ) ) ) ) ) & ! [V6x] : ( mem(V6x,A_27a) => ! [V7r] : ( mem(V7r,A_27b) => ! [V8p] : ( mem(V8p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(V1P,V8p)) => p(ap(V1P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V6x),V7r),V8p))) ) ) ) ) ) ) => ! [V9p] : ( mem(V9p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0Q),V9p)) => p(ap(V1P,V9p)) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Emem__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0s] : ( mem(V0s,A_27a) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Emem(A_27a,A_27b),V0s),V1p)) <=> ? [V2i] : ( mem(V2i,ty_2Enum_2Enum) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) & ( V0s = ap(ap(c_2Epath_2Eel(A_27a,A_27b),V2i),V1p) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Emem__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ! [V1s] : ( mem(V1s,A_27a) => ( p(ap(ap(c_2Epath_2Emem(A_27a,A_27b),V1s),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) <=> ( V1s = V0x ) ) ) ) ) & ! [V2x] : ( mem(V2x,A_27c) => ! [V3r] : ( mem(V3r,A_27d) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27c,A_27d)) => ! [V5s] : ( mem(V5s,A_27c) => ( p(ap(ap(c_2Epath_2Emem(A_27c,A_27d),V5s),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V2x),V3r),V4p))) <=> ( ( V5s = V2x ) | p(ap(ap(c_2Epath_2Emem(A_27c,A_27d),V5s),V4p)) ) ) ) ) ) ) ))))))).
fof(ax_thm_2Epath_2Edrop__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),c_2Enum_2E0),V0p) = V0p ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Enum_2ESUC,V1n)),V2p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V1n),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Edrop__def__compute,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),c_2Enum_2E0),V0p) = V0p ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),V2p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n))),V4p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(c_2Epath_2Etail(A_27a,A_27b),V4p)) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Enumeral__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n))),V1p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Epath_2Etail(A_27a,A_27b),V1p)) ) ) ) ) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V2n))),V3p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V2n))),ap(c_2Epath_2Etail(A_27a,A_27b),V3p)) ) ) ) ))))).
fof(conj_thm_2Epath_2Efinite__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1n),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => ( p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V1n),V0p))) <=> p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)) ) ) ) ))))).
fof(conj_thm_2Epath_2Elength__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1n),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => ( ap(c_2Epath_2Elength(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V1n),V0p)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),ap(c_2Epath_2Elength(A_27a,A_27b),V0p)),c_2Eoption_2ENONE(ty_2Enum_2Enum)),f1685(V1n)) ) ) ) ))))).
fof(conj_thm_2Epath_2EPL__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1i),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V1i),V0p)) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f1686(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p)) ) ) ) ))))).
fof(conj_thm_2Epath_2EIN__PL__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0i),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1j),ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V0i),V2p)))) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,V0i),V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Efirst__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ( ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V0i),V1p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0i),V1p) ) ) ) ))))).
fof(conj_thm_2Epath_2Efirst__label__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ( ap(c_2Epath_2Efirst__label(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V0i),V1p)) = ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V0i),V1p) ) ) ) ))))).
fof(conj_thm_2Epath_2Etail__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,V0i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ( ap(c_2Epath_2Etail(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V0i),V1p)) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2B,V0i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V1p) ) ) ) ))))).
fof(conj_thm_2Epath_2Eel__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,V0i),V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0i),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V1j),V2p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2B,V0i),V1j)),V2p) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Enth__label__drop,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,V0i),V1j))),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) => ( ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V0i),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V1j),V2p)) = ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),ap(ap(c_2Earithmetic_2E_2B,V0i),V1j)),V2p) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Etake__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Etake(A_27a,A_27b),c_2Enum_2E0),V0p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V0p)) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Enum_2ESUC,V1n)),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p)),ap(c_2Epath_2Efirst__label(A_27a,A_27b),V2p)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V1n),ap(c_2Epath_2Etail(A_27a,A_27b),V2p))) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Etake__def__compute,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Etake(A_27a,A_27b),c_2Enum_2E0),V0p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V0p)) ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p)),ap(c_2Epath_2Efirst__label(A_27a,A_27b),V2p)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Epath_2Etail(A_27a,A_27b),V2p))) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n))),V4p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V4p)),ap(c_2Epath_2Efirst__label(A_27a,A_27b),V4p)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(c_2Epath_2Etail(A_27a,A_27b),V4p))) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Efirst__take,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V1i),V0p)) = ap(c_2Epath_2Efirst(A_27a,A_27b),V0p) ) ) ))))).
fof(conj_thm_2Epath_2Efinite__take,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1i),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V1i),V0p))) ) ) ))))).
fof(conj_thm_2Epath_2Elength__take,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1i),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => ( ap(c_2Epath_2Elength(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V1i),V0p)) = ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,V1i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ) ) ) ))))).
fof(conj_thm_2Epath_2EPL__take,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1i),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V1i),V0p)) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f1687(V1i)) ) ) ) ))))).
fof(conj_thm_2Epath_2Elast__take,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ( ap(c_2Epath_2Elast(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V0i),V1p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0i),V1p) ) ) ) ))))).
fof(conj_thm_2Epath_2Enth__label__take,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V2i),V0n)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0n),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) ) => ( ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V2i),ap(ap(c_2Epath_2Etake(A_27a,A_27b),V0n),V1p)) = ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V2i),V1p) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Eseg__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V0i),V1j),V2p) = ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,V1j),V0i)),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),V0i),V2p)) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Esingleton__seg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V0i),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ( ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V0i),V0i),V1p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0i),V1p)) ) ) ) ))))).
fof(conj_thm_2Epath_2Erecursive__seg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( p(ap(ap(c_2Eprim__rec_2E_3C,V0i),V1j)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1j),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) ) => ( ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V0i),V1j),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0i),V2p)),ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V0i),V2p)),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2B,V0i),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V1j),V2p)) ) ) ) ) ))))).
fof(conj_thm_2Epath_2EPL__seg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0i),V1j)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1j),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) ) => ( ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V0i),V1j),V2p)) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f1688(V1j,V0i)) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Efinite__seg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V1i] : ( mem(V1i,ty_2Enum_2Enum) => ! [V2j] : ( mem(V2j,ty_2Enum_2Enum) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1i),V2j)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V2j),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) ) => p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V1i),V2j),V0p))) ) ) ) ))))).
fof(conj_thm_2Epath_2Efirst__seg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0i),V1j)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1j),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) ) => ( ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V0i),V1j),V2p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0i),V2p) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Elast__seg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ! [V2p] : ( mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0i),V1j)) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1j),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) ) => ( ap(c_2Epath_2Elast(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),V0i),V1j),V2p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),V1j),V2p) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Elabels__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Epath_2Elabels(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = c_2Ellist_2ELNIL(A_27b) ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2r] : ( mem(V2r,A_27b) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(c_2Epath_2Elabels(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p)) = ap(ap(c_2Ellist_2ELCONS(A_27b),V2r),ap(c_2Epath_2Elabels(A_27a,A_27b),V3p)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2EfirstP__at__unique,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),V2n)) => ! [V3m] : ( mem(V3m,ty_2Enum_2Enum) => ( p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),V3m)) <=> ( V3m = V2n ) ) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Eis__stopped__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(c_2Epath_2Eis__stopped(A_27a,A_27b),V0p)) <=> ? [V1x] : ( mem(V1x,A_27a) & ( V0p = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Eis__stopped__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( p(ap(c_2Epath_2Eis__stopped(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) <=> $true ) ) ) & ! [V1x] : ( mem(V1x,A_27c) => ! [V2r] : ( mem(V2r,A_27d) => ! [V3p] : ( mem(V3p,ty_2Epath_2Epath(A_27c,A_27d)) => ( p(ap(c_2Epath_2Eis__stopped(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V1x),V2r),V3p))) <=> $false ) ) ) ) ))))))).
fof(ax_thm_2Epath_2Efilter__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ( ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(V0P,V1x)) => ( ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x)) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x) ) ) ) ) & ! [V2x] : ( mem(V2x,A_27a) => ! [V3r] : ( mem(V3r,A_27b) => ! [V4p] : ( mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),V4p)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epath_2Epath(A_27a,A_27b)),ap(V0P,V2x)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epath_2Epath(A_27a,A_27b)),ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V4p)),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),V4p))),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))),ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),V4p)) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Efilter__every,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1p] : ( mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) => p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),V1p))) ) ) ))))).
fof(ax_thm_2Epath_2Epgenerate__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,A_27a)) => ! [V1g] : ( mem(V1g,arr(ty_2Enum_2Enum,A_27b)) => ( ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V0f),V1g) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(V0f,c_2Enum_2E0)),ap(V1g,c_2Enum_2E0)),ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,A_27a,ty_2Enum_2Enum),V0f),c_2Enum_2ESUC)),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,A_27b,ty_2Enum_2Enum),V1g),c_2Enum_2ESUC))) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Epgenerate__infinite,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,A_27a)) => ! [V1g] : ( mem(V1g,arr(ty_2Enum_2Enum,A_27b)) => ( ~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V0f),V1g))) ) ) ))))).
fof(conj_thm_2Epath_2Epgenerate__not__stopped,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Enum_2Enum,A_27a)) => ! [V1g] : ( mem(V1g,arr(ty_2Enum_2Enum,A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ( ~~ ( ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x) = ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V0f),V1g) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Eel__pgenerate,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => ! [V2g] : ( mem(V2g,arr(ty_2Enum_2Enum,A_27b)) => ( ap(ap(c_2Epath_2Eel(A_27a,A_27b),V0n),ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V1f),V2g)) = ap(V1f,V0n) ) ) ) ))))).
fof(conj_thm_2Epath_2Enth__label__pgenerate,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => ! [V2g] : ( mem(V2g,arr(ty_2Enum_2Enum,A_27b)) => ( ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),V0n),ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V1f),V2g)) = ap(V2g,V0n) ) ) ) ))))).
fof(conj_thm_2Epath_2Epgenerate__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,arr(ty_2Enum_2Enum,A_27a)) => ! [V1g1] : ( mem(V1g1,arr(ty_2Enum_2Enum,A_27b)) => ! [V2f2] : ( mem(V2f2,arr(ty_2Enum_2Enum,A_27a)) => ! [V3g2] : ( mem(V3g2,arr(ty_2Enum_2Enum,A_27b)) => ( ( ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V0f1),V1g1) = ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V2f2),V3g2) ) <=> ( ( V0f1 = V2f2 ) & ( V1g1 = V3g2 ) ) ) ) ) ) ))))).
fof(conj_thm_2Epath_2Epgenerate__onto,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0p] : ( mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ( ~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)) ) => ? [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,A_27a)) & ? [V2g] : ( mem(V2g,arr(ty_2Enum_2Enum,A_27b)) & ( V0p = ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V1f),V2g) ) ) ) ) ))))).
fof(ax_thm_2Epath_2Eokpath__f__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,arr(A_27a,bool)))) => ! [V1X] : ( mem(V1X,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ( ap(ap(c_2Epath_2Eokpath__f(A_27a,A_27b),V0R),V1X) = ap(ap(c_2Epred__set_2EUNION(ty_2Epath_2Epath(A_27a,A_27b)),ap(c_2Epred__set_2EGSPEC(ty_2Epath_2Epath(A_27a,A_27b),A_27a),f1689(A_27b,A_27a))),ap(c_2Epred__set_2EGSPEC(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,ty_2Epath_2Epath(A_27a,A_27b)))),ap(c_2Epair_2EUNCURRY(A_27a,ty_2Epair_2Eprod(A_27b,ty_2Epath_2Epath(A_27a,A_27b)),ty_2Epair_2Eprod(ty_2Epath_2Epath(A_27a,A_27b),bool)),f1692(A_27b,A_27a,V0R,V1X)))) ) ) ) ) ) )).
fof(conj_thm_2Epath_2Eokpath__monotone,conjecture,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,arr(A_27a,bool)))) => p(ap(c_2EfixedPoint_2Emonotone(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)),ap(c_2Epath_2Eokpath__f(A_27a,A_27b),V0R))) ))))).
