Step * 5 1 1 1 1 1 1 1 of Lemma monad-from_wf


1. Mnd Monad
2. λx,z. (M-bind(Mnd) x.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. Type
4. M-map(Mnd) (M-map(Mnd) (M-map(Mnd) X))
5. (M-bind(Mnd) (M-bind(Mnd) x.x)) x.x)) (M-bind(Mnd) x.(M-bind(Mnd) ((λx.x) x) x.x)))) ∈ (M-map(Mnd) X)
6. (M-bind(Mnd) (M-bind(Mnd) x.(M-return(Mnd) (M-bind(Mnd) x.x))))) x.x))
(M-bind(Mnd) x.(M-bind(Mnd) ((λx.(M-return(Mnd) (M-bind(Mnd) x.x)))) x) x.x))))
∈ (M-map(Mnd) X)
7. x1 M-map(Mnd) (M-map(Mnd) X)
8. (M-bind(Mnd) (M-return(Mnd) (M-bind(Mnd) x1 x.x))) x.x)) ((λx.x) (M-bind(Mnd) x1 x.x))) ∈ (M-map(Mnd) X)
⊢ (M-bind(Mnd) x1 x.x)) (M-bind(Mnd) (M-return(Mnd) (M-bind(Mnd) x1 x.x))) x.x)) ∈ (M-map(Mnd) X)
BY
(Reduce -1 THEN Eq) }


Latex:


Latex:

1.  Mnd  :  Monad
2.  \mlambda{}x,z.  (M-bind(Mnd)  z  (\mlambda{}x.x))  \mmember{}  A:Type  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  A))  {}\mrightarrow{}  (M-map(Mnd)  A)
3.  X  :  Type
4.  x  :  M-map(Mnd)  (M-map(Mnd)  (M-map(Mnd)  X))
5.  (M-bind(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.x))  (\mlambda{}x.x))
=  (M-bind(Mnd)  x  (\mlambda{}x.(M-bind(Mnd)  ((\mlambda{}x.x)  x)  (\mlambda{}x.x))))
6.  (M-bind(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.(M-return(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.x)))))  (\mlambda{}x.x))
=  (M-bind(Mnd)  x  (\mlambda{}x.(M-bind(Mnd)  ((\mlambda{}x.(M-return(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.x))))  x)  (\mlambda{}x.x))))
7.  x1  :  M-map(Mnd)  (M-map(Mnd)  X)
8.  (M-bind(Mnd)  (M-return(Mnd)  (M-bind(Mnd)  x1  (\mlambda{}x.x)))  (\mlambda{}x.x))  =  ((\mlambda{}x.x)  (M-bind(Mnd)  x1  (\mlambda{}x.x)))
\mvdash{}  (M-bind(Mnd)  x1  (\mlambda{}x.x))  =  (M-bind(Mnd)  (M-return(Mnd)  (M-bind(Mnd)  x1  (\mlambda{}x.x)))  (\mlambda{}x.x))


By


Latex:
(Reduce  -1  THEN  Eq)




Home Index