--- a/Solvable.agda	Sun Aug 16 22:08:46 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 11:02:16 2020 +0900
@@ -4,6 +4,7 @@
 
 open import Data.Unit
 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function
 open import Data.Nat using (ℕ; suc; zero)
 open import Relation.Nullary
 open import Data.Empty
@@ -17,28 +18,88 @@
 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 
 
 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
-  uni  : Commutator P ε
-  gen  : {f g h : Carrier} → P g → P h  → Commutator P f → Commutator P ( f ∙ [ g , h ]  )
-  ccong  : {f g  : Carrier} → f ≈ g → Commutator P f → Commutator P g
+  uni   : Commutator P ε
+  comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
+  gen   : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙  g  )
+  ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
 
 deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
 deriving (suc i) x = Commutator (deriving i) x 
 
--- deriving stage is closed on multiplication and inversion
-
-deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y  → deriving i ( x ∙ y )
-deriving-mul {zero} {x} {y} (lift tt) (lift tt) = lift tt
-deriving-mul {suc i} {ε} {ε} uni uni = ccong (Algebra.Group.sym G (proj₁ identity ε)) uni 
-deriving-mul {suc i} {ε} {_} uni (gen x x₁ iy) = ccong (Algebra.Group.sym G (proj₁ identity _)) (gen x x₁ iy)
-deriving-mul {suc i} {_} {ε} (gen x x₁ ix) uni = ccong (Algebra.Group.sym G (proj₂ identity _)) (gen x x₁ ix)
-deriving-mul {suc i} {_} {_} (gen x x₁ ix) (gen x₂ x₃ iy) = ccong {!!} (gen x₂ x₃ (gen x x₁ iy))
-deriving-mul {suc i} {_} {_} _ _ = {!!}
-
-deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
-deriving-inv {i} {x} ix = ?
-
 record Solvable : Set (Level.suc n ⊔ m) where
   field 
      dervied-length : ℕ
      end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  
+
+-- deriving stage is closed on multiplication and inversion
+
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+gsym = Algebra.Group.sym G
+grefl = Algebra.Group.refl G
+lemma3 : ε ≈ ε ⁻¹
+lemma3 = begin
+     ε          ≈⟨ gsym (proj₁ inverse _) ⟩
+     ε ⁻¹ ∙ ε   ≈⟨ proj₂ identity _ ⟩
+     ε ⁻¹
+   ∎ where open EqReasoning (Algebra.Group.setoid G)
+
+open import Data.List using ([] ; _∷_ ; List )
+
+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 ∷ []
+   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 
+
+glist : List Carrier → Carrier
+glist [] = ε
+glist (x ∷ []) = x
+glist (x ∷ y) = x ∙ glist y
+
+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
+   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 p p₁) (node q q₁) r p=r r=q = {!!}
+
+deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y  → deriving i ( x ∙ y )
+deriving-mul {zero} {x} {y} _ _ = lift tt
+deriving-mul {suc i} {x} {y} ix iy = gen ix iy
+
+deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
+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 )
+