Mercurial > hg > Members > kono > Proof > automaton

changeset 166:159ad8b0104e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 Mar 2021 00:23:23 +0900
parents 6cb442050825
children fc770d1661d4
files agda/gcd.agda
diffstat 1 files changed, 3 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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