# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624243970 -32400
# Node ID 06df58697178856ab96ec99ede8fd50285c075fa
# Parent  6474d814d9a8d07bd6e49bc2ff1f4d0642bfffd2
...

diff -r 6474d814d9a8 -r 06df58697178 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 11:04:37 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 11:52:50 2021 +0900
@@ -235,32 +235,24 @@
    k  ∎ where open ≡-Reasoning
 
 decD : {k m : ℕ} → k > 1 → Dec (Dividable k m)
-decD {k} {m} k>1 = f-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m)} F I m where
-        record FF (m : ℕ ) : Set where
-           field
-              diff : ℕ
-              is-diff :  k < m  → diff  ≡ m - k
-        ff : (m : ℕ ) → FF m
-        ff 0  = record { diff = 0 ; is-diff = λ () }
-        ff m with <-cmp k m
-        ... | tri< a ¬b ¬c = record { diff = m - k ; is-diff = λ _ → refl }
-        ... | tri≈ ¬a b ¬c = record { diff = 0 ; is-diff = λ lt → ⊥-elim (¬a lt) }
-        ... | tri> ¬a ¬b c = record { diff = 0 ; is-diff = λ lt → ⊥-elim (¬a lt) }
+decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m)} F I m where
         F : ℕ → ℕ
-        F m = FF.diff (ff m)
-        F0 : ( m : ℕ ) → F m ≡ 0 →  Dec  (Dividable k m )
+        F m = m
+        F0 : ( m : ℕ ) → F (m - k) ≡ 0 →  Dec  (Dividable k m )
         F0 0 eq =  yes div0
         F0 (suc m) eq with <-cmp k (suc m)
-        ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor = subst (λ g → 1 * k + 0 ≡ g ) m=k div1*k+0=k }  where
-            m=k : k ≡ suc m
-            m=k = sym (i-j=0→i=j (≤-trans refl-≤s a ) (subst (λ k → k ≡ 0) (FF.is-diff (ff (suc m)) a ) {!!}))
+        ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor =
+            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
         ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k }
-        ... | tri> ¬a ¬b c = no (div<k k>1 {!!} c )
-        I : Finduction ℕ  _  F
+        ... | tri> ¬a ¬b c = no (div<k k>1 (s≤s z≤n ) c )
+        decl : {m  : ℕ } → 0 < m → m - k < m
+        decl {zero} ()
+        decl {suc m} = {!!}
+        I : Ninduction ℕ  _  F
         I = record {
-              fzero = {!!}
-            ; pnext = λ p → {!!}
-            ; decline = λ {p} lt → {!!}
+              pnext = λ p → p - k
+            ; fzero = λ {m} eq → {!!}
+            ; decline = λ {m} lt → decl lt
             ; ind = λ {p} prev → {!!}
           } 
 
diff -r 6474d814d9a8 -r 06df58697178 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Mon Jun 21 11:04:37 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Mon Jun 21 11:52:50 2021 +0900
@@ -402,3 +402,31 @@
    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) 
 
 
+record Ninduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
+  field
+    pnext : (p : P ) → P
+    fzero   : {p : P} → f (pnext p) ≡ zero → Q p
+    decline : {p : P} → 0 < f p  → f (pnext p) < f p
+    ind : {p : P} → Q (pnext p) → Q p
+
+n-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
+  → (f : P → ℕ) 
+  → Ninduction P Q f
+  → (p : P ) → Q p
+n-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f (Ninduction.pnext I p))
+... | tri> ¬a ¬b ()
+... | tri≈ ¬a b ¬c = Ninduction.fzero I (sym b) 
+... | tri< lt _ _ = f-induction0 p (f p) {!!}  where 
+   f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x → Q p
+   f-induction0 p zero le = Ninduction.ind I (Ninduction.fzero I {!!}) where
+      fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
+      fi0 .0 z≤n = refl
+   f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x)
+   ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a 
+   ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (y<sx→y≤x f1)) where
+       f1 : f (Ninduction.pnext I (Ninduction.pnext I p)) < suc x
+       f1 = subst (λ k → f (Ninduction.pnext I (Ninduction.pnext I p)) < k ) b ( Ninduction.decline I {Ninduction.pnext I p}
+         (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) ))
+   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c ) 
+
+