# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597640524 -32400
# Node ID 04f40fc4eb69b03e86b70f2d9b452edc335233b5
# Parent  6bbd861e9ae882ba52c708da47ca0861d1152066
...

diff -r 6bbd861e9ae8 -r 04f40fc4eb69 Solvable.agda
--- a/Solvable.agda	Mon Aug 17 13:50:38 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 14:02:04 2020 +0900
@@ -70,18 +70,12 @@
 ∙-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)
+∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) with ∙-flatten (p o q )   -- t : x ∙ y ≈ mpf p (mpf q ε)
+... | t = begin
+     x ∙ y ∙ z                    ≈⟨ ∙-cong t grefl  ⟩
+     mpf p (mpf q ε) ∙ z          ≈⟨ {!!} ⟩
+     mpf p (mpf q (mpf r ε))
+   ∎ where open EqReasoning (Algebra.Group.setoid G)
 
 
 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹