# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1609734031 -32400
# Node ID 690a8352c1ad66aad5f48e4b8afec98e854396b3
# Parent  e5dc512f5306ce1b8511340041df73956fe577b6
...

diff -r e5dc512f5306 -r 690a8352c1ad agda/gcd.agda
--- a/agda/gcd.agda	Mon Jan 04 12:52:04 2021 +0900
+++ b/agda/gcd.agda	Mon Jan 04 13:20:31 2021 +0900
@@ -158,12 +158,9 @@
 open Comp
 
 comp-n : ( n : ℕ ) → (c : Comp n ) → Comp (compa c + n) 
-comp-n n c = record { compa = suc (compa c) ; compb = n ; is-comp = 
+comp-n n c = record { compa = compa c ; compb = suc (compb c) ; is-comp = 
    begin
-      n * suc (compa c)  ≡⟨ *-comm n (suc (compa c)) ⟩
-      n + compa c * n ≡⟨ +-comm n (compa c * n) ⟩
-      compa c * n + n ≡⟨ cong (λ k → k + n) ( *-comm (compa c) n) ⟩
-      (n * compa c) + n ≡⟨ cong (λ k → k + n) {!!} ⟩ 
+      compa c + compb c * compa c ≡⟨ cong (λ k → compa c + k) (is-comp c) ⟩ 
       compa c + n ∎ 
     } where open ≡-Reasoning
 
@@ -204,8 +201,9 @@
 
 gcd23 : ( n m k : ℕ) → 1 < n → 1 < m  → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
 gcd23 n m k 1<n 1<m gn gm = gcd230 n n m m k k 1<n 1<m ≤-refl ≤-refl ≤-refl gn gm where
-     gcd232 : (i i0 k k0 : ℕ) → (1 < i0) → i ≤ i0 → k ≤ k0 → gcd1 (suc i) i0 (suc k) k0 ≡ suc k → gcd1 i i0 (suc k) k0 ≡ suc k
-     gcd232 i i0 k k0 1<i0 i<i0 k<k0 = {!!}
+     gcd232 : (i0 j0 k0 : ℕ) → (1 < i0) → k ≤ k0 → gcd1 0 i0 0 k0 ≡ suc k → gcd1 0 j0 0 k0 ≡ suc zero
+         → suc zero ≤ gcd1 0 i0 0 j0
+     gcd232 i0 j0 k0 1<i0 k<k0 gi gj = {!!}
      gcd231 : (i0 k k0 : ℕ) → (1 < i0) → (suc k ≤ k0) → gcd1 0 i0 (suc k) k0 ≡ suc k → suc k ≤ i0
      gcd231 i0 k k0 1<i0 sk<k0 gi = subst (λ m → m ≤ i0 ) gi ( gcd50 0 i0 (suc k) k0 1<i0 z≤n sk<k0 )
      gcd230 : (i i0 j j0 k k0 : ℕ) → 1 < i0 → 1 < j0 → i ≤ i0 → j ≤ j0 → k ≤ k0  → gcd1 i i0 k k0 ≡ k → gcd1 j j0 k k0 ≡ k → k ≤ gcd1 i i0 j j0
@@ -216,8 +214,14 @@
      ... | tri> ¬a ¬b c = gcd231 j0 k k0 1<j k<k0 gj 
      gcd230 zero i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
      gcd230 (suc i) i0 zero j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
-     gcd230 (suc i) i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = subst (λ m → suc k ≤ m) (sym (gcd22 i i0 j j0))
-         (gcd230 i i0 j j0 (suc k) k0 {!!} {!!} {!!} {!!} k<k0 {!!} {!!} ) -- gcd1 (suc i) i0 (suc k) k0 ≡ suc k → gcd1 i i0 (suc k) k0 ≡ suc k
+     gcd230 (suc zero) i0 (suc zero) j0 (suc zero) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj =
+         gcd232 i0 j0 k0 1<i {!!} {!!} {!!}
+     gcd230 (suc zero) i0 (suc zero) j0 (suc (suc k)) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 (suc zero) i0 (suc (suc j)) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 (suc (suc i)) i0 (suc zero) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 (suc (suc i)) i0 (suc (suc j)) j0 (suc zero) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!}
+     gcd230 (suc (suc i)) i0 (suc (suc j)) j0 (suc (suc k)) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = 
+          {!!} -- gcd230 (suc i) i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj 
 
 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k 1<n 1<m gn gm  )))