---

Step * 5 1 of Lemma monad-from_wf

.....subterm..... T:t
3:n
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (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 (λx.x)) (λx.x)) = (M-bind(Mnd) x (λx.(M-bind(Mnd) ((λx.x) x) (λx.x)))) ∈ (M-map(Mnd) X)
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.x))))) (λx.x))
= (M-bind(Mnd) x (λx.(M-bind(Mnd) ((λx.x) x) (λx.x))))
∈ (M-map(Mnd) X)
BY
{ (InstLemma `M-associative` [⌜Mnd⌝;⌜M-map(Mnd) (M-map(Mnd) X)⌝;⌜M-map(Mnd) X⌝;⌜X⌝;⌜x⌝;⌜λx.(M-return(Mnd) 
                                                                                            (M-bind(Mnd) x (λx.x)))⌝;
   ⌜λx.x⌝]⋅
   THEN Auto
   ) }

1
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (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 (λx.x)) (λx.x)) = (M-bind(Mnd) x (λx.(M-bind(Mnd) ((λx.x) x) (λx.x)))) ∈ (M-map(Mnd) X)
6. (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.x))))) (λx.x))
= (M-bind(Mnd) x (λx.(M-bind(Mnd) ((λx.(M-return(Mnd) (M-bind(Mnd) x (λx.x)))) x) (λx.x))))
∈ (M-map(Mnd) X)
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.x))))) (λx.x))
= (M-bind(Mnd) x (λx.(M-bind(Mnd) ((λx.x) x) (λx.x))))
∈ (M-map(Mnd) X)

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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))))
\mvdash{}  (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.x)  x)  (\mlambda{}x.x))))


By

---

Latex:
(InstLemma  `M-associative`  [\mkleeneopen{}Mnd\mkleeneclose{};\mkleeneopen{}M-map(Mnd)  (M-map(Mnd)  X)\mkleeneclose{};\mkleeneopen{}M-map(Mnd)  X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};
  \mkleeneopen{}\mlambda{}x.(M-return(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.x)))\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index