include('Axioms/listRange_2.ax').
tff(tp_c_2EerrorStateMonad_2EBIND,type,(c_2EerrorStateMonad_2EBIND:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EBIND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EerrorStateMonad_2EBIND(A_27a,A_27b,A_27c),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))),arr(arr(A_27b,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a)))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a)))))))))).
tff(tp_c_2EerrorStateMonad_2EES__APPLY,type,(c_2EerrorStateMonad_2EES__APPLY:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EES__APPLY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EerrorStateMonad_2EES__APPLY(A_27a,A_27b,A_27c),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(arr(A_27c,A_27b),A_27a))),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))))))))).
tff(tp_c_2EerrorStateMonad_2EES__CHOICE,type,(c_2EerrorStateMonad_2EES__CHOICE:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EES__CHOICE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EerrorStateMonad_2EES__CHOICE(A_27a,A_27b),arr(arr(A_27b,ty_2Eoption_2Eoption(A_27a)),arr(arr(A_27b,ty_2Eoption_2Eoption(A_27a)),arr(A_27b,ty_2Eoption_2Eoption(A_27a)))))))).
tff(tp_c_2EerrorStateMonad_2EES__FAIL,type,(c_2EerrorStateMonad_2EES__FAIL:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EES__FAIL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EerrorStateMonad_2EES__FAIL(A_27a,A_27b),arr(A_27b,ty_2Eoption_2Eoption(A_27a)))))).
tff(tp_c_2EerrorStateMonad_2EES__GUARD,type,(c_2EerrorStateMonad_2EES__GUARD:del > $i)).
tff(mem_c_2EerrorStateMonad_2EES__GUARD,axiom,( ! [A_27a:del] : mem(c_2EerrorStateMonad_2EES__GUARD(A_27a),arr(bool,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27a))))))).
tff(tp_c_2EerrorStateMonad_2EES__LIFT2,type,(c_2EerrorStateMonad_2EES__LIFT2:(del * del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EES__LIFT2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : ( ! [A_27d:del] : mem(c_2EerrorStateMonad_2EES__LIFT2(A_27a,A_27b,A_27c,A_27d),arr(arr(A_27c,arr(A_27d,A_27b)),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27a))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))))))))))).
tff(tp_c_2EerrorStateMonad_2EEXT,type,(c_2EerrorStateMonad_2EEXT:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EEXT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EerrorStateMonad_2EEXT(A_27a,A_27b,A_27c),arr(arr(A_27c,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))))))))).
tff(tp_c_2EerrorStateMonad_2EFOR,type,(c_2EerrorStateMonad_2EFOR:del > $i)).
tff(mem_c_2EerrorStateMonad_2EFOR,axiom,( ! [A_27state:del] : mem(c_2EerrorStateMonad_2EFOR(A_27state),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))))).
tff(tp_c_2EerrorStateMonad_2EFOREACH,type,(c_2EerrorStateMonad_2EFOREACH:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EFOREACH,axiom,( ! [A_27a:del] : ( ! [A_27state:del] : mem(c_2EerrorStateMonad_2EFOREACH(A_27a,A_27state),arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))))).
tff(tp_c_2EerrorStateMonad_2EIGNORE__BIND,type,(c_2EerrorStateMonad_2EIGNORE__BIND:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EIGNORE__BIND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EerrorStateMonad_2EIGNORE__BIND(A_27a,A_27b,A_27c),arr(arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,A_27b))),arr(arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))),arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b)))))))))).
tff(tp_c_2EerrorStateMonad_2EJOIN,type,(c_2EerrorStateMonad_2EJOIN:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EJOIN,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EerrorStateMonad_2EJOIN(A_27a,A_27b),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))),A_27a))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))))))).
tff(tp_c_2EerrorStateMonad_2EMCOMP,type,(c_2EerrorStateMonad_2EMCOMP:(del * del * del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EMCOMP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : ( ! [A_27d:del] : ( ! [A_27e:del] : mem(c_2EerrorStateMonad_2EMCOMP(A_27a,A_27b,A_27c,A_27d,A_27e),arr(arr(A_27d,arr(A_27e,ty_2Eoption_2Eoption(A_27c))),arr(arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27e)))),arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(A_27c)))))))))))).
tff(tp_c_2EerrorStateMonad_2EMMAP,type,(c_2EerrorStateMonad_2EMMAP:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EMMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EerrorStateMonad_2EMMAP(A_27a,A_27b,A_27c),arr(arr(A_27c,A_27b),arr(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))))))))).
tff(tp_c_2EerrorStateMonad_2ENARROW,type,(c_2EerrorStateMonad_2ENARROW:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2ENARROW,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27state:del] : mem(c_2EerrorStateMonad_2ENARROW(A_27a,A_27b,A_27state),arr(A_27b,arr(arr(ty_2Epair_2Eprod(A_27b,A_27state),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27state)))),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,A_27state)))))))))).
tff(tp_c_2EerrorStateMonad_2EREAD,type,(c_2EerrorStateMonad_2EREAD:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EREAD,axiom,( ! [A_27a:del] : ( ! [A_27state:del] : mem(c_2EerrorStateMonad_2EREAD(A_27a,A_27state),arr(arr(A_27state,A_27a),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,A_27state)))))))).
tff(tp_c_2EerrorStateMonad_2EUNIT,type,(c_2EerrorStateMonad_2EUNIT:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EUNIT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EerrorStateMonad_2EUNIT(A_27a,A_27b),arr(A_27b,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))))))).
tff(tp_c_2EerrorStateMonad_2EWIDEN,type,(c_2EerrorStateMonad_2EWIDEN:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EWIDEN,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27state:del] : mem(c_2EerrorStateMonad_2EWIDEN(A_27a,A_27b,A_27state),arr(arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,A_27state))),arr(ty_2Epair_2Eprod(A_27b,A_27state),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27state)))))))))).
tff(tp_c_2EerrorStateMonad_2EWRITE,type,(c_2EerrorStateMonad_2EWRITE:del > $i)).
tff(mem_c_2EerrorStateMonad_2EWRITE,axiom,( ! [A_27state:del] : mem(c_2EerrorStateMonad_2EWRITE(A_27state),arr(arr(A_27state,A_27state),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))))).
tff(tp_c_2EerrorStateMonad_2EmapM,type,(c_2EerrorStateMonad_2EmapM:(del * del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2EmapM,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2EerrorStateMonad_2EmapM(A_27a,A_27b,A_27c),arr(arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b)))),arr(ty_2Elist_2Elist(A_27a),arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27c),A_27b)))))))))).
tff(tp_c_2EerrorStateMonad_2Esequence,type,(c_2EerrorStateMonad_2Esequence:(del * del) > $i)).
tff(mem_c_2EerrorStateMonad_2Esequence,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EerrorStateMonad_2Esequence(A_27a,A_27b),arr(ty_2Elist_2Elist(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27b),A_27a)))))))).
tff(ax_thm_2EerrorStateMonad_2EUNIT__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27b) => (ap(c_2EerrorStateMonad_2EUNIT(A_27a,A_27b),V0x) = f536(A_27b,A_27a,V0x))))))).
tff(ax_thm_2EerrorStateMonad_2EBIND__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))))) => ( ! [V2s0:$i] : (mem(V2s0,A_27a) => (ap(ap(ap(c_2EerrorStateMonad_2EBIND(A_27a,A_27b,A_27c),V0g),V1f),V2s0) = ap(ap(ap(c_2Eoption_2Eoption__CASE(ty_2Epair_2Eprod(A_27b,A_27a),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),ap(V0g,V2s0)),c_2Eoption_2ENONE(ty_2Epair_2Eprod(A_27c,A_27a))),f539(A_27b,A_27c,A_27a,V1f))))))))))))).
tff(ax_thm_2EerrorStateMonad_2EIGNORE__BIND__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,A_27b)))) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b)))) => (ap(ap(c_2EerrorStateMonad_2EIGNORE__BIND(A_27a,A_27b,A_27c),V0f),V1g) = ap(ap(c_2EerrorStateMonad_2EBIND(A_27b,A_27a,A_27c),V0f),k(A_27a,V1g))))))))))).
tff(ax_thm_2EerrorStateMonad_2EMMAP__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27c,A_27b)) => ( ! [V1m:$i] : (mem(V1m,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a)))) => (ap(ap(c_2EerrorStateMonad_2EMMAP(A_27a,A_27b,A_27c),V0f),V1m) = ap(ap(c_2EerrorStateMonad_2EBIND(A_27a,A_27c,A_27b),V1m),ap(ap(c_2Ecombin_2Eo(A_27c,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))),A_27b),c_2EerrorStateMonad_2EUNIT(A_27a,A_27b)),V0f))))))))))).
tff(ax_thm_2EerrorStateMonad_2EJOIN__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0z:$i] : (mem(V0z,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))),A_27a)))) => (ap(c_2EerrorStateMonad_2EJOIN(A_27a,A_27b),V0z) = ap(ap(c_2EerrorStateMonad_2EBIND(A_27a,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))),A_27b),V0z),c_2Ecombin_2EI(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))))))))))).
tff(ax_thm_2EerrorStateMonad_2EEXT__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27c,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))))) => ( ! [V1m:$i] : (mem(V1m,arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a)))) => (ap(ap(c_2EerrorStateMonad_2EEXT(A_27a,A_27b,A_27c),V0g),V1m) = ap(ap(c_2EerrorStateMonad_2EBIND(A_27a,A_27c,A_27b),V1m),V0g)))))))))).
tff(ax_thm_2EerrorStateMonad_2EMCOMP__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27d,arr(A_27e,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27e))))) => (ap(ap(c_2EerrorStateMonad_2EMCOMP(A_27a,A_27b,A_27c,A_27d,A_27e),V0g),V1f) = ap(c_2Epair_2ECURRY(A_27a,A_27b,ty_2Eoption_2Eoption(A_27c)),ap(ap(c_2Eoption_2EOPTION__MCOMP(A_27c,ty_2Epair_2Eprod(A_27d,A_27e),ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27d,A_27e,ty_2Eoption_2Eoption(A_27c)),V0g)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27e))),V1f)))))))))))))).
tff(ax_thm_2EerrorStateMonad_2EFOR__primitive__def,axiom,( ! [A_27state:del]: (c_2EerrorStateMonad_2EFOR(A_27state) = ap(ap(c_2Erelation_2EWFREC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))),ap(c_2Emin_2E_40(arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),bool))),f543(A_27state))),f549(A_27state))))).
tff(conj_thm_2EerrorStateMonad_2EFOR__ind,lemma,(( ! [A_27state:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),bool)) => (( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3a:$i] : (mem(V3a,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => (((~~ (V1i = V2j)) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V2j))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),inj__ty_2Enum_2Enum(V2j)),V3a))))) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),inj__ty_2Enum_2Enum(V1i)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),inj__ty_2Enum_2Enum(V2j)),V3a))))))))) => ( ! [V4v:tp__ty_2Enum_2Enum] : ( ! [V5v1:tp__ty_2Enum_2Enum] : ( ! [V6v2:$i] : (mem(V6v2,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),inj__ty_2Enum_2Enum(V4v)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),inj__ty_2Enum_2Enum(V5v1)),V6v2)))))))))))))).
tff(conj_thm_2EerrorStateMonad_2EFOR__def,lemma,(( ! [A_27state:del]: ( ! [V0j:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => (ap(c_2EerrorStateMonad_2EFOR(A_27state),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),inj__ty_2Enum_2Enum(V1i)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),inj__ty_2Enum_2Enum(V0j)),V2a))) = ap(ap(ap(c_2Ebool_2ECOND(arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V0j))),ap(V2a,inj__ty_2Enum_2Enum(V1i))),ap(ap(c_2EerrorStateMonad_2EBIND(A_27state,ty_2Eone_2Eone,ty_2Eone_2Eone),ap(V2a,inj__ty_2Enum_2Enum(V1i))),k(ty_2Eone_2Eone,ap(c_2EerrorStateMonad_2EFOR(A_27state),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V0j))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),inj__ty_2Enum_2Enum(V0j)),V2a)))))))))))))).
tff(ax_thm_2EerrorStateMonad_2EFOREACH__primitive__def,axiom,( ! [A_27a:del]: ( ! [A_27state:del]: (c_2EerrorStateMonad_2EFOREACH(A_27a,A_27state) = ap(ap(c_2Erelation_2EWFREC(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state)))),ap(c_2Emin_2E_40(arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),bool))),f553(A_27state,A_27a))),f559(A_27a,A_27state)))))).
tff(conj_thm_2EerrorStateMonad_2EFOREACH__ind,lemma,(( ! [A_27a:del]: ( ! [A_27state:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),bool)) => ((( ! [V1a:$i] : (mem(V1a,arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),c_2Elist_2ENIL(A_27a)),V1a))))) & ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3t:$i] : (mem(V3t,ty_2Elist_2Elist(A_27a)) => ( ! [V4a:$i] : (mem(V4a,arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => (p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),V3t),V4a))) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3t)),V4a))))))))))) => ( ! [V5v:$i] : (mem(V5v,ty_2Elist_2Elist(A_27a)) => ( ! [V6v1:$i] : (mem(V6v1,arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => p(ap(V0P,ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),V5v),V6v1)))))))))))))).
tff(conj_thm_2EerrorStateMonad_2EFOREACH__def,lemma,(( ! [A_27a:del]: ( ! [A_27state:del]: (( ! [V0a:$i] : (mem(V0a,arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => (ap(c_2EerrorStateMonad_2EFOREACH(A_27a,A_27state),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),c_2Elist_2ENIL(A_27a)),V0a)) = ap(c_2EerrorStateMonad_2EUNIT(A_27state,ty_2Eone_2Eone),inj__ty_2Eone_2Eone(fo__c_2Eone_2Eone))))) & ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3a:$i] : (mem(V3a,arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))) => (ap(c_2EerrorStateMonad_2EFOREACH(A_27a,A_27state),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V1t)),V3a)) = ap(ap(c_2EerrorStateMonad_2EBIND(A_27state,ty_2Eone_2Eone,ty_2Eone_2Eone),ap(V3a,V2h)),k(ty_2Eone_2Eone,ap(c_2EerrorStateMonad_2EFOREACH(A_27a,A_27state),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Eone_2Eone,A_27state))))),V1t),V3a)))))))))))))))).
tff(ax_thm_2EerrorStateMonad_2EREAD__def,axiom,( ! [A_27a:del]: ( ! [A_27state:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27state,A_27a)) => (ap(c_2EerrorStateMonad_2EREAD(A_27a,A_27state),V0f) = f560(A_27a,A_27state,V0f))))))).
tff(ax_thm_2EerrorStateMonad_2EWRITE__def,axiom,( ! [A_27state:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27state,A_27state)) => (ap(c_2EerrorStateMonad_2EWRITE(A_27state),V0f) = f561(A_27state,V0f)))))).
tff(ax_thm_2EerrorStateMonad_2ENARROW__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27state:del]: ( ! [V0v:$i] : (mem(V0v,A_27b) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Epair_2Eprod(A_27b,A_27state),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27state))))) => (ap(ap(c_2EerrorStateMonad_2ENARROW(A_27a,A_27b,A_27state),V0v),V1f) = f565(A_27b,A_27state,A_27a,V1f,V0v)))))))))).
tff(ax_thm_2EerrorStateMonad_2EWIDEN__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27state:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,A_27state)))) => (ap(c_2EerrorStateMonad_2EWIDEN(A_27a,A_27b,A_27state),V0f) = ap(c_2Epair_2EUNCURRY(A_27b,A_27state,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27a,ty_2Epair_2Eprod(A_27b,A_27state)))),f570(A_27a,A_27b,A_27state,V0f))))))))).
tff(ax_thm_2EerrorStateMonad_2Esequence__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (c_2EerrorStateMonad_2Esequence(A_27a,A_27b) = ap(ap(c_2Elist_2EFOLDR(arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27b,A_27a))),arr(A_27a,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27b),A_27a)))),f574(A_27a,A_27b)),ap(c_2EerrorStateMonad_2EUNIT(A_27a,ty_2Elist_2Elist(A_27b)),c_2Elist_2ENIL(A_27b))))))).
tff(ax_thm_2EerrorStateMonad_2EmapM__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))))) => (ap(c_2EerrorStateMonad_2EmapM(A_27a,A_27b,A_27c),V0f) = ap(ap(c_2Ecombin_2Eo(ty_2Elist_2Elist(A_27a),arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27c),A_27b))),ty_2Elist_2Elist(arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))))),c_2EerrorStateMonad_2Esequence(A_27b,A_27c)),ap(c_2Elist_2EMAP(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b)))),V0f))))))))).
tff(conj_thm_2EerrorStateMonad_2EBIND__LEFT__UNIT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0k:$i] : (mem(V0k,arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (ap(ap(c_2EerrorStateMonad_2EBIND(A_27b,A_27a,A_27c),ap(c_2EerrorStateMonad_2EUNIT(A_27b,A_27a),V1x)),V0k) = ap(V0k,V1x))))))))))).
tff(conj_thm_2EerrorStateMonad_2EMCOMP__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27d,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27b))))) => (ap(ap(c_2EerrorStateMonad_2EMCOMP(A_27a,A_27b,ty_2Epair_2Eprod(A_27c,A_27b),A_27d,A_27b),V0g),V1f) = ap(ap(c_2Ecombin_2Eo(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))),arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27b)))),ap(c_2EerrorStateMonad_2EEXT(A_27b,A_27c,A_27d),V0g)),V1f)))))))))))).
tff(conj_thm_2EerrorStateMonad_2EMCOMP__ASSOC,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [A_27f:del]: ( ! [A_27g:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27d,arr(A_27e,ty_2Eoption_2Eoption(A_27c)))) => ( ! [V1g:$i] : (mem(V1g,arr(A_27f,arr(A_27g,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27d,A_27e))))) => ( ! [V2h:$i] : (mem(V2h,arr(A_27a,arr(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27f,A_27g))))) => (ap(ap(c_2EerrorStateMonad_2EMCOMP(A_27a,A_27b,A_27c,A_27d,A_27e),V0f),ap(ap(c_2EerrorStateMonad_2EMCOMP(A_27a,A_27b,ty_2Epair_2Eprod(A_27d,A_27e),A_27f,A_27g),V1g),V2h)) = ap(ap(c_2EerrorStateMonad_2EMCOMP(A_27a,A_27b,A_27c,A_27f,A_27g),ap(ap(c_2EerrorStateMonad_2EMCOMP(A_27f,A_27g,A_27c,A_27d,A_27e),V0f),V1g)),V2h))))))))))))))))).