--- a/Solvable.agda	Mon Aug 17 11:30:12 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 12:56:53 2020 +0900
@@ -38,6 +38,7 @@
 
 gsym = Algebra.Group.sym G
 grefl = Algebra.Group.refl G
+
 lemma3 : ε ≈ ε ⁻¹
 lemma3 = begin
      ε          ≈⟨ gsym (proj₁ inverse _) ⟩
@@ -45,43 +46,47 @@
      ε ⁻¹
    ∎ where open EqReasoning (Algebra.Group.setoid G)
 
-open import Data.List using ([] ; _∷_ ; List ; length )
-
-data Node (A : Set n) : Set (Level.suc n) where
-   leaf : A → Node A
-   node : Node A → Node A → Node A
-
-flatten : Node Carrier → List Carrier
-flatten x = flatten1 x [] where
-   flatten1 : Node Carrier → List Carrier → List Carrier
-   flatten1 (leaf x)  y = x ∷ y
-   flatten1 (node left right)  y = flatten1 left (flatten1 right y )
-
-gnode : Node Carrier → Carrier
-gnode (leaf x) = x
-gnode (node left right) = gnode left ∙ gnode right 
+lemma6 : {f : Carrier } →  ( f ⁻¹ ) ⁻¹  ≈ f
+lemma6 {f} = begin
+     ( f ⁻¹ ) ⁻¹   ≈⟨ gsym ( proj₁ identity _) ⟩
+      ε  ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
+     (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ assoc _ _ _ ⟩
+     f ∙ ( f ⁻¹  ∙ ( f ⁻¹ ) ⁻¹ )  ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
+     f ∙ ε  ≈⟨ proj₂ identity _ ⟩
+     f
+   ∎ where open EqReasoning (Algebra.Group.setoid G)
 
-glist : List Carrier → Carrier
-glist [] = ε
-glist (x ∷ []) = x
-glist (x ∷ y) = x ∙ glist y
+lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
+lemma5 f g = begin
+     g ⁻¹ ∙ f ⁻¹                              ≈⟨ gsym (proj₂ identity _) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ε                         ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )  ≈⟨ assoc _ _ _ ⟩
+     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g ∙ (f ∙ g) ⁻¹))     ≈⟨ ∙-cong grefl (gsym (assoc _ _ _)) ⟩
+     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g) ∙ (f ∙ g) ⁻¹)     ≈⟨ gsym ( assoc _ _ _) ⟩
+     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g)) ∙ (f ∙ g) ⁻¹     ≈⟨ ∙-cong (gsym (assoc _ _ _ )) grefl ⟩
+     (g ⁻¹ ∙ f ⁻¹)  ∙ (f ∙ g) ∙ (f ∙ g) ⁻¹    ≈⟨ ∙-cong (assoc _ _ _ ) grefl ⟩
+     (g ⁻¹ ∙ (f ⁻¹  ∙ (f ∙ g))) ∙ (f ∙ g) ⁻¹  ≈⟨ ∙-cong (∙-cong grefl (gsym (assoc _ _ _ )) ) grefl ⟩
+     (g ⁻¹ ∙ ((f ⁻¹  ∙ f) ∙ g)) ∙ (f ∙ g) ⁻¹  ≈⟨ ∙-cong (gsym (assoc _ _ _ )) grefl ⟩
+     (g ⁻¹ ∙ (f ⁻¹  ∙ f) ∙ g)  ∙ (f ∙ g) ⁻¹   ≈⟨ ∙-cong (assoc _ _ _) grefl ⟩
+     g ⁻¹ ∙ ((f ⁻¹  ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹    ≈⟨ ∙-cong (∙-cong grefl (∙-cong (proj₁ inverse _ ) grefl )) grefl ⟩
+     g ⁻¹ ∙ (ε  ∙ g) ∙ (f ∙ g) ⁻¹             ≈⟨ ∙-cong (∙-cong grefl ( proj₁ identity _) ) grefl ⟩
+     g ⁻¹ ∙ g ∙ (f ∙ g) ⁻¹                    ≈⟨ ∙-cong (proj₁ inverse _) grefl  ⟩
+     ε  ∙ (f ∙ g) ⁻¹                          ≈⟨ proj₁ identity _ ⟩
+     (f ∙ g) ⁻¹
+     ∎ where open EqReasoning (Algebra.Group.setoid G)
 
-gpattern : (p q : Node Carrier) → flatten p ≡ flatten q  → gnode p ≈ gnode q
-gpattern p q eq = gpattern1 p q (flatten p) _≡_.refl eq  where
-   gnot0 : ( left right : Node Carrier ) →  length (flatten (node left right) ) > 1
-   gnot0 (leaf x) (leaf x₁) = s≤s ( s≤s z≤n)
-   gnot0 (leaf x) (node q q₁) = {!!}
-   gnot0 (node p p₁) q = {!!}
-   gnot1 : (x : Carrier ) → ( left right : Node Carrier ) →  ¬ ( x ∷ [] ≡ flatten (node left right) )
-   gnot1 x p q eq0 = {!!}
-   gpattern1 : (p q : Node Carrier) → (r : List Carrier ) → flatten p ≡ r → r ≡ flatten q → gnode p ≈ gnode q
-   gpattern1 (leaf x) (leaf x) (x ∷ []) _≡_.refl _≡_.refl = grefl
-   gpattern1 (leaf x) (node left right) (x ∷ []) _≡_.refl r=q = {!!}
-   gpattern1 (node p p₁) (leaf x) r p=r r=q = {!!}
-   gpattern1 (node (leaf x) p₁) (node (leaf x₁) q₁) r p=r r=q = {!!}
-   gpattern1 (node (leaf x) p₁) (node (node q q₂) q₁) r p=r r=q = {!!}
-   gpattern1 (node (node p p₂) p₁) (node (leaf x) q₁) r p=r r=q = {!!}
-   gpattern1 (node (node p p₂) p₁) (node (node q q₂) q₁) r p=r r=q = {!!}
+lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
+lemma4 g h = begin
+       [ h , g ]                               ≈⟨ grefl ⟩
+       (h ⁻¹ ∙ g ⁻¹ ∙   h ) ∙ g                ≈⟨ assoc _ _ _ ⟩
+       h ⁻¹ ∙ g ⁻¹ ∙  (h ∙ g)                  ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6))  ⟩
+       h ⁻¹ ∙  g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹)  ≈⟨  ∙-cong grefl (lemma5 _ _ )  ⟩
+       h ⁻¹ ∙  g ⁻¹ ∙  (g ⁻¹ ∙ h ⁻¹) ⁻¹        ≈⟨ assoc _ _ _ ⟩
+       h ⁻¹ ∙ (g ⁻¹ ∙  (g ⁻¹ ∙ h ⁻¹) ⁻¹)       ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
+       h ⁻¹ ∙ (g ⁻¹ ∙   h ⁻¹ ∙ g) ⁻¹           ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
+       (g ⁻¹ ∙ h ⁻¹ ∙   g ∙ h) ⁻¹              ≈⟨ grefl ⟩
+       [ g , h ]  ⁻¹                  
+     ∎ where open EqReasoning (Algebra.Group.setoid G)
 
 deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y  → deriving i ( x ∙ y )
 deriving-mul {zero} {x} {y} _ _ = lift tt
@@ -91,22 +96,6 @@
 deriving-inv {zero} {x} (lift tt) = lift tt
 deriving-inv {suc i} {ε} uni = ccong lemma3 uni
 deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x) where
-   lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
-   lemma4 g h = begin
-       h ⁻¹ ∙ g ⁻¹ ∙ h ∙ g            ≈⟨ {!!} ⟩
-      [ g , h ] ⁻¹
-     ∎ where open EqReasoning (Algebra.Group.setoid G)
 deriving-inv {suc i} {_} (gen x x₁ )    = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
-   lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
-   lemma5 f g = begin
-     g ⁻¹ ∙ f ⁻¹           ≈⟨ {!!} ⟩
-     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ {!!} ⟩
-     (g ⁻¹ ∙ f ⁻¹  ∙ (f ∙ g)) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
-     (g ⁻¹ ∙ (f ⁻¹  ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
-     (g ⁻¹ ∙ (ε  ∙ g)) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
-     (g ⁻¹ ∙ g) ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
-     ε  ∙ (f ∙ g) ⁻¹  ≈⟨ {!!} ⟩
-     (f ∙ g) ⁻¹
-     ∎ where open EqReasoning (Algebra.Group.setoid G)
 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )