Mercurial > hg > Members > kono > Proof > automaton

changeset 144:34fec132be3d

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:38:52 +0900
parents f896c112f01f
children cdfdc8bfb3db
files agda/root2.agda
diffstat 1 files changed, 2 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/agda/root2.agda	Tue Dec 29 15:32:57 2020 +0900
+++ b/agda/root2.agda	Tue Dec 29 15:38:52 2020 +0900
@@ -68,13 +68,8 @@
    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 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 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) 1<i
+   gcd21 zero i0 (suc j) j0 o o0 1<i 1<j 1<o refl 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 =