# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615562603 -32400
# Node ID 159ad8b0104e9338d49b72221e4743bbafbce31e
# Parent  6cb442050825273ab72415967808a8a65b4a172f
...

diff -r 6cb442050825 -r 159ad8b0104e agda/gcd.agda
--- a/agda/gcd.agda	Sat Mar 13 00:03:36 2021 +0900
+++ b/agda/gcd.agda	Sat Mar 13 00:23:23 2021 +0900
@@ -72,11 +72,11 @@
 gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
 gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!}
 gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} 
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k (decf if) {!!} (decf jf) j0f j0=0 {!!} {!!} {!!} 
 gcd-gt (suc zero) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
-     gcd-gt zero i0 j j0 k {!!} i0f {!!} j0f i0=0 j0=0 {!!} {!!}
+     gcd-gt zero i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!}
 gcd-gt (suc (suc i)) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
-     gcd-gt (suc i) i0 j j0 k {!!} i0f {!!} j0f i0=0 j0=0 {!!} {!!}
+     gcd-gt (suc i) i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!}
 
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n