Mercurial > hg > Members > kono > Proof > automaton

changeset 143:f896c112f01f

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 Tue, 29 Dec 2020 15:32:57 +0900
parents 3294dbcccfe8
children 34fec132be3d
files agda/root2.agda
diffstat 1 files changed, 11 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/agda/root2.agda	Mon Dec 28 11:35:29 2020 +0900
+++ b/agda/root2.agda	Tue Dec 29 15:32:57 2020 +0900
@@ -55,6 +55,9 @@
 
 open import nat
 
+gcd24' : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
+gcd24' = {!!}
+
 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 = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
    gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
@@ -62,10 +65,16 @@
    gcd22 zero i0 (suc o) o0 = refl
    gcd22 (suc i) i0 zero o0 = refl
    gcd22 (suc i) i0 (suc o) o0 = refl 
+   1<ss : {j : ℕ} → 1 < suc (suc j)
+   1<ss = s≤s (s≤s z≤n)
    gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
    gcd21 zero .1 zero j0 o o0 1<i 1<j 1<o gn gm refl = nat-<≡ 1<i
-   gcd21 zero i0 (suc zero) j0 o o0 1<i 1<j 1<o refl gm refl = {!!}
-   gcd21 zero i0 (suc (suc j)) j0 o o0 1<i 1<j 1<o refl gm gnm = {!!}
+   gcd21 zero i0 (suc zero) j0 zero o0 1<i 1<j 1<o refl gm gnm = nat-≡< gm 1<i
+   gcd21 zero (suc i0) (suc (suc j)) j0 zero (suc o0) 1<i 1<j 1<o refl gm gnm = {!!} where
+      gcd23 : gcd1 (suc j) (suc (suc j)) o0 (suc o0) ≡ suc i0 → gcd1 i0 (suc i0) (suc j) (suc (suc j)) ≡ 1 → ⊥
+      gcd23 = {!!}
+   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = ⊥-elim ( nat-<≡ 1<k )
+   gcd21 zero i0 (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = {!!}
    gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn refl gnm = {!!}
    gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
    gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm =