Mercurial > hg > Members > kono > Proof > automaton

changeset 210:2aba74f9708d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
max
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Jun 2021 23:25:01 +0900
parents 1c537e2b8f69
children 28d4fb7b576f
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 72 insertions(+), 168 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 20 19:26:46 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 20 23:25:01 2021 +0900
@@ -227,35 +227,26 @@
    → Dividable k ( gcd i  j ) 
 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
-gg1 : {i0 : ℕ } → 1 * i0 + 0 ≡ i0
-gg1 {i0} = begin  1 * i0 + 0 ≡⟨ +-comm _ 0 ⟩
-    i0 + 0 ≡⟨ +-comm _ 0 ⟩
-    i0 ∎   where open ≡-Reasoning  
-
-gg3 : {i0 : ℕ } → i0 * 1 + 0 ≡ i0
-gg3 = trans (+-comm _ 0 ) m*1=m
-
-open import Data.Sum.Base
-
-gcd-divable1 : ( i j  : ℕ )
+gcd-divable : ( i j  : ℕ )
       → Dividable ( gcd i j ) i ∧ Dividable ( gcd i  j ) j
-gcd-divable1 i j  = f-induction {_} {_} {ℕ ∧ ℕ}
+gcd-divable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
    {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
         F : ℕ ∧ ℕ → ℕ
-        F ⟪ 0 , j ⟫ = 0
-        F ⟪ i , 0 ⟫ = 0
+        F ⟪ 0 , 0 ⟫ = 0
+        F ⟪ 0 , suc j ⟫ = 0
+        F ⟪ suc i , 0 ⟫ = 0
         F ⟪ suc i , suc j ⟫ with <-cmp i j
-        ... | tri< a ¬b ¬c = j - i 
+        ... | tri< a ¬b ¬c = suc j
         ... | tri≈ ¬a b ¬c = 0
-        ... | tri> ¬a ¬b c = i - j
+        ... | tri> ¬a ¬b c = suc i
         F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0)
         F0 {zero} {zero} p = case1 refl
         F0 {zero} {suc j} p =  case2 (case1 refl)
         F0 {suc i} {zero} p =  case2 (case2 refl)
         F0 {suc i} {suc j} p with <-cmp i j
-        ... | tri< a ¬b ¬c = case1 ( sym (cong suc ( i-j=0→i=j {j} {i} (<to≤ a)  p )) )
-        ... | tri≈ ¬a refl ¬c = case1 refl
-        ... | tri> ¬a ¬b c = case1 (cong suc ( i-j=0→i=j {i} {j} (<to≤ c) p ))
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        ... | tri≈ ¬a refl ¬c =  case1 refl
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
         F00 :  {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
         F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq
         ... | case1 refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
@@ -263,169 +254,82 @@
                                     , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
         ... | case2 (case2 refl) = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
                                     , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫
+        Fsym :  {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫
+        Fsym {0} {0} = refl
+        Fsym {0} {suc j} = refl
+        Fsym {suc i} {0} = refl
+        Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i
+        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = {!!}
+        ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
+        ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
+        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = {!!}
+        ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+        ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = {!!}
+        ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
+        ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!}
+        ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!}
+        F< :  {i j k : ℕ } → 0 < i → i < j  → j < k → F ⟪ i , j ⟫ < F ⟪ i , k ⟫
+        F< = {!!}
         record Fdec ( i j : ℕ ) : Set where
            field
                ni : ℕ 
                nj : ℕ 
                fdec :  0 < F ⟪ i , j ⟫  → F ⟪ ni , nj ⟫  < F ⟪ i , j ⟫
-        F<i : {i j : ℕ} → 0 < i  → 0 < j →  F ⟪ i , j  ⟫  <  j
-        F<i {suc i} {suc j} 0<i 0<j with <-cmp i j
-        ... | tri< a ¬b ¬c = fd3 where
-           fd3 : suc j - suc i < suc j
-           fd3 = {!!} 
-        ... | tri≈ ¬a refl ¬c = fd4 where
-           fd4 : 0 < suc j
-           fd4 = {!!} 
-        ... | tri> ¬a ¬b c = fd5 where
-           fd5 : suc i - suc j < suc j
-           fd5 = {!!} 
-        i-j≤F : {i j : ℕ} → 0 < i  → 0 < j → j < i  →  i - j ≤ F ⟪ i , j  ⟫  
-        i-j≤F = {!!}
-        F-sym : {i j : ℕ} → F ⟪ i , j  ⟫  ≡  F ⟪ j , i  ⟫ 
-        F-sym {zero} {zero} = refl
-        F-sym {zero} {suc j} = refl
-        F-sym {suc i} {zero} = refl
-        F-sym {suc i} {suc j} with <-cmp  i j | <-cmp j i
-        ... | tri< a ¬b ¬c | tri> a' ¬b' ¬c' = refl
-        ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (¬c₁ a)
-        ... | tri< a ¬b ¬c | tri≈ ¬a refl ¬c₁ = ⊥-elim (¬b refl)
-        ... | tri≈ ¬a refl ¬c |  tri≈ ¬a' refl ¬c'  = refl
-        ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬a a)
-        ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)
-        ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
-        ... | tri> ¬a ¬b c | tri≈ ¬a₁ refl ¬c = ⊥-elim (¬b refl)
-        ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a c₁)
         fedc0 : (i j : ℕ ) → Fdec i j
-        fedc0 0 j = record { ni = 0 ; nj = j ; fdec =  λ lt → ⊥-elim  {!!} }
-        fedc0 i 0 = record { ni = i ; nj = 0 ; fdec =  λ lt → ⊥-elim  {!!} }
+        fedc0 0 0 = record { ni =  0 ; nj = 0 ; fdec = λ ()  } 
+        fedc0 (suc i) 0 = record { ni =  suc i ; nj = 0 ; fdec = λ ()  } 
+        fedc0 0 (suc j)  = record { ni =  0 ; nj = suc j ; fdec = λ ()  } 
         fedc0 (suc i) (suc j) with <-cmp i j
-        ... | tri< a ¬b ¬c = record { ni =  suc i ; nj = suc j - suc i ; fdec = λ lt → fd1 } where
-            fd1 :  F ⟪ suc i , suc j - suc i ⟫ < F ⟪ suc i , suc j ⟫
-            fd1 = begin
-              suc (F ⟪ suc i , suc j - suc i ⟫) ≤⟨ F<i {suc i} {suc j - suc i} (s≤s z≤n)  {!!}  ⟩
-              suc j - suc i  ≤⟨ i-j≤F {!!} {!!} {!!} ⟩
-              F ⟪ suc i , suc j ⟫ ∎   where open ≤-Reasoning  
-        ... | tri≈ ¬a b ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ lt → ⊥-elim (nat-≡< {!!} {!!} ) }
-        ... | tri> ¬a ¬b c = record { ni =  suc i - suc j ; nj = suc j ; fdec = {!!} }
+        ... | tri< a ¬b ¬c = record { ni =  suc i ; nj = j - i ; fdec = λ lt → fd1 (j - i) refl  } where
+            fd1 : ( k : ℕ ) → k ≡ j - i →  F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫
+            fd1 0 eq = {!!}
+            fd1 (suc k) eq = fd2 i j k a eq where
+               fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i  →  F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫
+               fd2 i j k i<j eq with <-cmp i k | <-cmp i j
+               ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where
+                    fd3 : suc k < suc j
+                    fd3 = {!!}
+               ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim {!!} -- i ≡ j
+               ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim {!!} 
+               ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n
+               ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim {!!} -- i ≡ j
+               ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c =  s≤s z≤n -- i > j
+               ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where
+                    fd4 : suc i < suc j
+                    fd4 = s≤s a
+               ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c =  ⊥-elim {!!}
+               ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ =  ⊥-elim {!!}
+        ... | tri≈ ¬a refl ¬c = record { ni =  suc i ; nj = suc j     ; fdec = λ eq → {!!}  }
+        ... | tri> ¬a ¬b c = record { ni =  i - j ; nj = suc j ; fdec = λ lt → {!!} } where
+        ind :   ( i j : ℕ ) →
+            Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j))
+            ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j))
+             → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
+        ind zero zero prev = ind0 where
+           ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero
+           ind0 = {!!}
+        ind zero (suc j) prev = ind1 where
+           ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j)
+           ind1 = {!!}
+        ind (suc i) zero prev = ind2 where
+           ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero
+           ind2 = {!!}
+        ind (suc i) (suc j) prev with <-cmp i j
+        ... | tri< a ¬b ¬c = {!!}
+        ... | tri≈ ¬a b ¬c = {!!}
+        ... | tri> ¬a ¬b c = {!!}
+        --ind3 where
+        --   ind3 : Dividable (gcd (suc i) (suc j)) (suc i) ∧ Dividable (gcd (suc i) (suc j)) (suc j)
+        --   ind3 = {!!}
+
         I : Finduction (ℕ ∧ ℕ) _ F
         I = record {
               fzero = F00 
             ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) ,  Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ 
             ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p))  lt
-            ; ind = {!!}
+            ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           } 
 
-gcd-divable : ( i i0 j j0 : ℕ )
-      → (if : Factor i0 j0) (jf : Factor j0 i0)   -- factor eq * i0 + (j0 - i0) = j0
-      → ((i0 ≤ j0) ∧ (remain if ≡ j - i))  ∨ ((j0 ≤ i0) ∧ (remain jf ≡ i - j))
-      → Dividable ( gcd1 i i0 j j0 ) i0 ∧ Dividable ( gcd1 i i0 j j0 ) j0
-gcd-divable zero i0 zero j0 if jf if=0∨jf=0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = (gg2 if=0∨jf=0) } ⟫ where
-    gg2 : (if=0∨jf=0 : ((i0 ≤ j0) ∧ (remain if ≡ 0)) ∨ ((j0 ≤ i0) ∧ (remain jf ≡ 0))) →  factor if *  i0 + 0 ≡ j0
-    gg2 (case1 x) = begin
-      factor if * i0 + 0 ≡⟨ cong (λ k → factor if * i0 + k) (sym (proj2 x)) ⟩
-      factor if * i0 + remain if ≡⟨ is-factor if ⟩
-      j0 ∎   where open ≡-Reasoning  
-    gg2 (case2 x) = ⊥-elim ( nat-≤> (proj1 x) a)
-... | tri≈ ¬a refl ¬c = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
-... | tri> ¬a ¬b c = ⟪ record { factor = factor jf ; is-factor = gg2 if=0∨jf=0  } ,  record { factor = 1 ; is-factor = gg1 } ⟫ where
-    gg2 : (if=0∨jf=0 : ((i0 ≤ j0) ∧ (remain if ≡ 0)) ∨ ((j0 ≤ i0) ∧ (remain jf ≡ 0))) → factor jf *  j0 + 0 ≡ i0
-    gg2 (case1 x) = ⊥-elim ( nat-≤> (proj1 x) c)
-    gg2 (case2 x) = begin
-      factor jf * j0 + 0 ≡⟨ cong (λ k → factor jf * j0 + k) (sym (proj2 x)) ⟩
-      factor jf * j0 + remain jf ≡⟨ is-factor jf ⟩
-      i0 ∎   where open ≡-Reasoning  
-gcd-divable zero i0 (suc zero) j0 if jf if=0∨jf=0 =  ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫ 
-gcd-divable zero zero (suc (suc j)) j0 if jf if=0∨jf=0 = ⟪ record { factor = factor jf ; is-factor = gg4 } ,  record { factor = 1 ; is-factor = gg1 } ⟫
-   where
-    gg4 :  factor jf * j0  + 0 ≡ zero
-    gg4 with  m*n≡0⇒m≡0∨n≡0 (factor jf) (  m+n≡0⇒m≡0 (factor jf * j0) (is-factor jf))
-    ... | inj₁ x = begin
-      factor jf * j0 + 0 ≡⟨ +-comm _ 0 ⟩
-      factor jf * j0  ≡⟨ cong (λ k → k * j0) x  ⟩
-      0 ∎   where open ≡-Reasoning
-    ... | inj₂ y = begin
-      factor jf * j0 + 0 ≡⟨ +-comm _ 0 ⟩
-      factor jf * j0  ≡⟨ cong (λ k → factor jf * k) y  ⟩
-      factor jf * 0  ≡⟨ *-comm (factor jf) 0  ⟩
-      0 ∎   where open ≡-Reasoning
-gcd-divable zero (suc i0) (suc (suc j)) j0 if jf if=0∨jf=0  =
-    ⟪ record { factor = gg8 ; is-factor = {!!} } , record { factor = gg8 ; is-factor = {!!} } ⟫ where
-    gg8 : ℕ
-    gg8 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
-    gg9 : 1 * suc i0 + (suc j - i0) ≡ suc (suc j)
-    gg9 = begin
-      1 * suc i0 + (suc j - i0)   ≡⟨ +-comm (1 * suc i0) _ ⟩
-      (suc (suc j) - suc i0 ) + 1 * suc i0    ≡⟨ cong (λ k →  (suc (suc j) - suc i0 ) + suc k ) (+-comm i0 0) ⟩
-      (suc (suc j) - suc i0 ) + suc i0    ≡⟨ minus+n (s≤s (s≤s {!!})) ⟩
-      suc (suc j)  ∎   where open ≡-Reasoning
-    gg10 : factor jf * suc (suc j) + (i0 - suc j) ≡ suc i0
-    gg10 = begin
-      factor jf * suc (suc j) + (i0 - suc j) ≡⟨ {!!}  ⟩
-      factor jf * j0 + remain jf ≡⟨ is-factor jf  ⟩
-      suc i0  ∎   where open ≡-Reasoning
-    gg11 : ((suc i0 ≤ j0) ∧ (remain if ≡ (suc (suc j) - zero))) ∨ ((j0 ≤ suc i0) ∧ (remain jf ≡ (zero - suc (suc j))))
-       → ((suc i0 ≤ suc (suc j)) ∧ ((suc j - i0) ≡ (suc j - i0))) ∨ ((suc (suc j) ≤ suc i0) ∧ ((i0 - suc j) ≡ (i0 - suc j)))
-    gg11 (case1 x) = case1 ⟪ {!!} , refl ⟫
-    gg11 (case2 x) = case2 ⟪ {!!} , refl ⟫
-    gg7 : Dividable gg8 (suc i0) ∧ Dividable gg8 (suc (suc j))
-    gg7 = gcd-divable i0 (suc i0) (suc j) (suc (suc j)) -- Factor (suc i0) (suc (suc j)),  Factor (suc (suc j)) (suc i0)
-        record { factor = 1 ; is-factor = {!!} ; remain = suc j - i0 }
-        record { factor = factor jf ; is-factor = {!!} ; remain = i0 - suc j } {!!} 
---
---   gcd i (i + j ) = gcd i j
---if   : Factor (suc i0) j0    --  factor if * (suc i0) + (suc (suc j) - zero  ≡ j0
---jf   : Factor j0 (suc i0)    --  factor jf * j0 + (zero - suc (suc j))) ≡ suc i0
---if=0 : remain if ≡ (suc (suc j) - zero)
---jf=0 : remain jf ≡ (zero - suc (suc j))
---    factor if * suc i0 + (suc j - i0) ≡ suc (suc j)
---    factor jf * suc (suc j) + (i0 - suc j) ≡ suc i
-gcd-divable (suc zero) i0 zero j0 if jf if=0∨jf=0 = ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫
-gcd-divable (suc (suc i)) i0 zero zero if jf if=0∨jf=0 = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg4 } ⟫
-   where
-    gg4 :  factor if * i0  + 0 ≡ zero
-    gg4 with  m*n≡0⇒m≡0∨n≡0 (factor if) (  m+n≡0⇒m≡0 (factor if * i0) (is-factor if))
-    ... | inj₁ x = begin
-      factor if * i0 + 0 ≡⟨ +-comm _ 0 ⟩
-      factor if * i0  ≡⟨ cong (λ k → k * i0) x  ⟩
-      0 ∎   where open ≡-Reasoning
-    ... | inj₂ y = begin
-      factor if * i0 + 0 ≡⟨ +-comm _ 0 ⟩
-      factor if * i0  ≡⟨ cong (λ k → factor if * k) y  ⟩
-      factor if * 0  ≡⟨ *-comm (factor if) 0  ⟩
-      0 ∎   where open ≡-Reasoning
-gcd-divable (suc (suc i)) i0 zero (suc j0) if jf if=0∨jf=0 with gcd-divable (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} {!!}
-... | t = ⟪ {!!} , {!!} ⟫
-gcd-divable (suc zero) i0 (suc j) j0 if jf if=0∨jf=0 =  
-     gcd-divable zero i0 j j0 record {  factor = factor if ; is-factor = gg4 ; remain = j - zero }
-                              record {  factor = factor jf ; is-factor = gg5 ; remain = zero - j  } {!!} where
-    gg4 : factor if * i0 + (j - zero) ≡ j0
-    gg4 = begin
-      factor if * i0 + (j - zero)  ≡⟨  cong ( λ k → factor if * i0 + k) (sym {!!}) ⟩
-      factor if * i0 + remain if ≡⟨ is-factor if   ⟩
-      j0 ∎   where open ≡-Reasoning  
-    gg5 : factor jf * j0 + (zero - j) ≡ i0
-    gg5 = begin
-      factor jf * j0 + (zero - j)  ≡⟨  cong ( λ k → factor jf * j0 + k) (sym {!!}) ⟩
-      factor jf * j0 + remain jf ≡⟨ is-factor jf   ⟩
-      i0 ∎   where open ≡-Reasoning  
-gcd-divable (suc (suc i)) i0 (suc j) j0 if jf if=0∨jf=0 = 
-     gcd-divable (suc i) i0 j j0 record {  factor = factor if ; is-factor = gg4 ; remain = j - suc i }
-                              record {  factor = factor jf ; is-factor = gg5 ; remain = suc i - j } (gg6 if=0∨jf=0) where
-    gg6 : ((i0 ≤ j0) ∧ (remain if ≡ (suc j - suc (suc i)))) ∨ ((j0 ≤ i0) ∧ (remain jf ≡ (suc (suc i) - suc j)))
-        → ((i0 ≤ j0) ∧ ((j - suc i) ≡ (j - suc i))) ∨ ((j0 ≤ i0) ∧ ((suc i - j) ≡ (suc i - j)))
-    gg6 (case1 x) = case1 ⟪ proj1 x , refl ⟫ 
-    gg6 (case2 x) = case2 ⟪ proj1 x , refl ⟫ 
-    gg4 : factor if * i0 + (j - suc i ) ≡ j0
-    gg4 = begin
-      factor if * i0 + ( j - suc i ) ≡⟨ cong ( λ k → factor if * i0 + k ) (sym {!!}) ⟩ 
-      factor if * i0 + remain if  ≡⟨ is-factor if   ⟩
-      j0 ∎   where open ≡-Reasoning  
-    gg5 : factor jf * j0 + (suc i - j) ≡ i0
-    gg5 = begin
-      factor jf * j0 + ( suc i - j ) ≡⟨ cong ( λ k → factor jf * j0 + k ) (sym {!!}) ⟩  
-      factor jf * j0 + remain jf  ≡⟨ is-factor jf   ⟩
-      i0 ∎   where open ≡-Reasoning  
 
 gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
 gcd203 zero = refl