--- a/Solvable.agda	Mon Aug 17 12:56:53 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 13:50:38 2020 +0900
@@ -56,6 +56,34 @@
      f
    ∎ where open EqReasoning (Algebra.Group.setoid G)
 
+data MP  : Carrier → Set (Level.suc n) where
+    am  : (x : Carrier )   →  MP  x
+    _o_ : {x y : Carrier } →  MP  x →  MP  y → MP  ( x ∙ y )
+
+mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
+mpf {x} (am x) y = x ∙ y
+mpf (m o m₁) y = mpf m ( mpf m₁ y )
+
+mp-flatten : {x : Carrier } → (m : MP x ) → Carrier 
+mp-flatten {x} m = mpf {x} m ε 
+
+∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
+∙-flatten {x} (am x) = gsym (proj₂ identity _)
+∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
+∙-flatten {w} (_o_ {x} {y} p q ) = lemma8 w x y _≡_.refl where
+   lemma8 : (w x y : Carrier  ) → w ≡ x ∙ y  → x ∙ y  ≈ mpf p (mpf q ε)
+   lemma8 w x y refl with  ∙-flatten p | ∙-flatten q
+   ... | eq | eq1 = {!!}
+   
+--      x ∙ y ∙ z                  ≈⟨ assoc _ _ _ ⟩
+--      x ∙ ({!!} ∙ ?)                  ≈⟨ ∙-cong grefl (
+--                             ?   ≈⟨ {!!} ⟩
+--      x ∙ ( mpf q (mpf r ε ))    ≈⟨ {!!} ⟩
+--      mpf p (mpf q (mpf r ε))    ≈⟨ grefl ⟩
+--      mp-flatten ((p o q) o r)
+--    ∎ where open EqReasoning (Algebra.Group.setoid G)
+
+
 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
 lemma5 f g = begin
      g ⁻¹ ∙ f ⁻¹                              ≈⟨ gsym (proj₂ identity _) ⟩