Mercurial > hg > Members > kono > Proof > automaton

changeset 150:36d3ecce01b2

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 Fri, 01 Jan 2021 12:36:23 +0900
parents d3a8572ced9c
children 9e16cbec717b
files agda/gcd.agda
diffstat 1 files changed, 9 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Fri Jan 01 12:16:32 2021 +0900
+++ b/agda/gcd.agda	Fri Jan 01 12:36:23 2021 +0900
@@ -32,22 +32,15 @@
 even*n : {n m : ℕ } → even n → even ( n * m )
 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
 
-gcd2 : ( i i0 j j0 : ℕ ) → i ≤ i0 → j ≤ j0 → i0 < j0  → ℕ
-gcd2 zero i0 zero j0 i<i0 j<j0 i<j = j0
-gcd2 zero i0 (suc zero) j0 i<i0 j<j0 i<j = 1
-gcd2 zero zero (suc (suc j)) j0 i<i0 j<j0 i<j = j0
--- i<i0 : zero ≤ suc i0
--- j<j0 : suc (suc j) ≤ j0
--- i<j  : suc i0 < j0
-gcd2 zero (suc i0) (suc (suc j)) j0 i<i0 j<j0 i<j with <-cmp (suc (suc j)) (suc i0)  -- non terminating
-... | tri< a ¬b ¬c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
-... | tri≈ ¬a refl ¬c = suc i0
-... | tri> ¬a ¬b c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
--- = gcd2  (suc j) (suc (suc j))  i0 (suc i0) refl-≤s refl-≤s {!!} -- suc (suc j) < suc i0
-gcd2 (suc zero) i0 zero j0 i<i0 j<j0 i<j = 1
-gcd2 (suc (suc i)) i0 zero zero i<i0 j<j0 i<j = i0
-gcd2 (suc (suc i)) i0 zero (suc j0) i<i0 j<j0 i<j  = gcd2 (suc i) (suc (suc i))  j0 (suc j0)   refl-≤s refl-≤s {!!} --  suc (suc i) < suc j0
-gcd2 (suc i) i0 (suc j) j0 i<i0 j<j0 i<j = gcd2 i i0 j j0 (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0) i<j  
+gcd2 : ( i i0 j j0 : ℕ ) → i ≤ i0 → j ≤ j0 → ℕ
+gcd2 zero i0 zero j0 i<i0 j<j0  = j0
+gcd2 zero i0 (suc zero) j0 i<i0 j<j0 = 1
+gcd2 zero zero (suc (suc j)) j0 i<i0 j<j0 = j0
+gcd2 zero (suc i0) (suc (suc j)) j0 i<i0 j<j0 = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s 
+gcd2 (suc zero) i0 zero j0 i<i0 j<j0 = 1
+gcd2 (suc (suc i)) i0 zero zero i<i0 j<j0 = i0
+gcd2 (suc (suc i)) i0 zero (suc j0) i<i0 j<j0 = gcd2 (suc i) (suc (suc i))  j0 (suc j0)   refl-≤s refl-≤s 
+gcd2 (suc i) i0 (suc j) j0 i<i0 j<j0 = gcd2 i i0 j j0 (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)   
 
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0