---

Step * 4 1 2 1 of Lemma monad-from_wf


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. A : Type@i'
4. B : Type@i'
5. g : A ⟶ B@i
6. x : M-map(Mnd) (M-map(Mnd) A)
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.x)) (λx.(M-return(Mnd) (g x))))
= (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (g x))))))) (λx.x))
∈ (M-map(Mnd) B)
BY
{ ((InstLemma `M-associative` [⌜Mnd⌝;⌜M-map(Mnd) A⌝;⌜M-map(Mnd) B⌝;⌜B⌝;⌜x⌝;⌜λx.(M-return(Mnd) 
                                                                                (M-bind(Mnd) x 
                                                                                 (λx.(M-return(Mnd) (g x)))))⌝;⌜λx.x⌝]⋅
    THENA (Auto THEN (Assert M-bind(Mnd) ∈ (M-map(Mnd) A) ⟶ (A ⟶ (M-map(Mnd) B)) ⟶ (M-map(Mnd) B) BY Auto) THEN Auto)
    )
   THEN Reduce -1
   ) }

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. A : Type@i'
4. B : Type@i'
5. g : A ⟶ B@i
6. x : M-map(Mnd) (M-map(Mnd) A)
7. (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (g x))))))) (λx.x))
= (M-bind(Mnd) x (λx.(M-bind(Mnd) (M-return(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (g x))))) (λx.x))))
∈ (M-map(Mnd) B)
⊢ (M-bind(Mnd) (M-bind(Mnd) x (λx.x)) (λx.(M-return(Mnd) (g x))))
= (M-bind(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (M-bind(Mnd) x (λx.(M-return(Mnd) (g x))))))) (λx.x))
∈ (M-map(Mnd) B)

---

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.  A  :  Type@i'
4.  B  :  Type@i'
5.  g  :  A  {}\mrightarrow{}  B@i
6.  x  :  M-map(Mnd)  (M-map(Mnd)  A)
\mvdash{}  (M-bind(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.x))  (\mlambda{}x.(M-return(Mnd)  (g  x))))
=  (M-bind(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.(M-return(Mnd)  (M-bind(Mnd)  x  (\mlambda{}x.(M-return(Mnd)  (g  x))))))) 
      (\mlambda{}x.x))


By

---

Latex:
((InstLemma  `M-associative`  [\mkleeneopen{}Mnd\mkleeneclose{};\mkleeneopen{}M-map(Mnd)  A\mkleeneclose{};\mkleeneopen{}M-map(Mnd)  B\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(M-return(Mnd) 
                                                                                                                                                            (M-bind(Mnd)  x 
                                                                                                                                                              (\mlambda{}x.(M-return(Mnd) 
                                                                                                                                                                        (g  x)))))\mkleeneclose{};
    \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{}
    THENA  (Auto
                  THEN  (Assert  M-bind(Mnd)  \mmember{}  (M-map(Mnd)  A)  {}\mrightarrow{}  (A  {}\mrightarrow{}  (M-map(Mnd)  B))  {}\mrightarrow{}  (M-map(Mnd)  B)  BY
                                          Auto)
                  THEN  Auto)
    )
  THEN  Reduce  -1
  )

---

Home Index