include('Axioms/Temporal_Logic_2.ax').
tff(tp_c_2EreaderMonad_2EBIND,type,(c_2EreaderMonad_2EBIND:(del * del * del) > $i)).
tff(mem_c_2EreaderMonad_2EBIND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27s:del] : mem(c_2EreaderMonad_2EBIND(A_27a,A_27b,A_27s),arr(arr(A_27s,A_27a),arr(arr(A_27a,arr(A_27s,A_27b)),arr(A_27s,A_27b)))))))).
tff(tp_c_2EreaderMonad_2EFMAP,type,(c_2EreaderMonad_2EFMAP:(del * del * del) > $i)).
tff(mem_c_2EreaderMonad_2EFMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27s:del] : mem(c_2EreaderMonad_2EFMAP(A_27a,A_27b,A_27s),arr(arr(A_27a,A_27b),arr(arr(A_27s,A_27a),arr(A_27s,A_27b)))))))).
tff(tp_c_2EreaderMonad_2EJOIN,type,(c_2EreaderMonad_2EJOIN:(del * del) > $i)).
tff(mem_c_2EreaderMonad_2EJOIN,axiom,( ! [A_27a:del] : ( ! [A_27s:del] : mem(c_2EreaderMonad_2EJOIN(A_27a,A_27s),arr(arr(A_27s,arr(A_27s,A_27a)),arr(A_27s,A_27a)))))).
tff(tp_c_2EreaderMonad_2EMCOMPOSE,type,(c_2EreaderMonad_2EMCOMPOSE:(del * del * del * del) > $i)).
tff(mem_c_2EreaderMonad_2EMCOMPOSE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : ( ! [A_27s:del] : mem(c_2EreaderMonad_2EMCOMPOSE(A_27a,A_27b,A_27c,A_27s),arr(arr(A_27a,arr(A_27s,A_27b)),arr(arr(A_27b,arr(A_27s,A_27c)),arr(A_27a,arr(A_27s,A_27c)))))))))).
tff(tp_c_2EreaderMonad_2EUNIT,type,(c_2EreaderMonad_2EUNIT:(del * del) > $i)).
tff(mem_c_2EreaderMonad_2EUNIT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2EreaderMonad_2EUNIT(A_27a,A_27b),arr(A_27a,arr(A_27b,A_27a)))))).
tff(ax_thm_2EreaderMonad_2EBIND__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27s:del]: ( ! [V0M:$i] : (mem(V0M,arr(A_27s,A_27a)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,arr(A_27s,A_27b))) => ( ! [V2s:$i] : (mem(V2s,A_27s) => (ap(ap(ap(c_2EreaderMonad_2EBIND(A_27a,A_27b,A_27s),V0M),V1f),V2s) = ap(ap(V1f,ap(V0M,V2s)),V2s)))))))))))).
tff(ax_thm_2EreaderMonad_2EUNIT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1s:$i] : (mem(V1s,A_27b) => (ap(ap(c_2EreaderMonad_2EUNIT(A_27a,A_27b),V0x),V1s) = V0x)))))))).
tff(ax_thm_2EreaderMonad_2EMCOMPOSE__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27s:del]: ( ! [V0f1:$i] : (mem(V0f1,arr(A_27a,arr(A_27s,A_27b))) => ( ! [V1f2:$i] : (mem(V1f2,arr(A_27b,arr(A_27s,A_27c))) => ( ! [V2a:$i] : (mem(V2a,A_27a) => (ap(ap(ap(c_2EreaderMonad_2EMCOMPOSE(A_27a,A_27b,A_27c,A_27s),V0f1),V1f2),V2a) = ap(ap(c_2EreaderMonad_2EBIND(A_27b,A_27c,A_27s),ap(V0f1,V2a)),V1f2))))))))))))).
tff(conj_thm_2EreaderMonad_2EBIND__UNITR,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m:$i] : (mem(V0m,arr(A_27a,A_27b)) => (ap(ap(c_2EreaderMonad_2EBIND(A_27b,A_27b,A_27a),V0m),c_2EreaderMonad_2EUNIT(A_27b,A_27a)) = V0m))))))).
tff(conj_thm_2EreaderMonad_2EBIND__UNITL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0x:$i] : (mem(V0x,A_27c) => ( ! [V1f:$i] : (mem(V1f,arr(A_27c,arr(A_27a,A_27b))) => (ap(ap(c_2EreaderMonad_2EBIND(A_27c,A_27b,A_27a),ap(c_2EreaderMonad_2EUNIT(A_27c,A_27a),V0x)),V1f) = ap(V1f,V0x))))))))))).
tff(conj_thm_2EreaderMonad_2EMCOMPOSE__LEFT__ID,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0g:$i] : (mem(V0g,arr(A_27a,arr(A_27b,A_27c))) => (ap(ap(c_2EreaderMonad_2EMCOMPOSE(A_27a,A_27a,A_27c,A_27b),c_2EreaderMonad_2EUNIT(A_27a,A_27b)),V0g) = V0g)))))))).