# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624803187 -32400
# Node ID 709e63cb9d196edde5a562b5922f8f8dd33d6b91
# Parent  9f7e4a4415f72575cc26913fa9d2b86f463ac5e8
...

diff -r 9f7e4a4415f7 -r 709e63cb9d19 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 27 22:43:20 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 27 23:13:07 2021 +0900
@@ -299,6 +299,17 @@
    → Dividable k ( gcd i  j ) 
 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
+-- gcd loop invariant
+--
+record GCD ( i i0 j j0 : ℕ ) : Set where
+     i<i0  : i ≤ i0
+     j<j0  : j ≤ j0
+     div-i : Dividable i0 (j0 + i - j )
+     div-j : Dividable j0 (i0 + j - i)
+
+gcd-next : {i i0 j j0 : ℕ} → GCD (suc i) i0 (suc j) j0 → GCD i i0 j j0
+gcd-next = ?
+
 di-next : {i i0 j j0 : ℕ} → Dividable i0  ((j0 + suc i) - suc j ) ∧ Dividable j0 ((i0 + suc j) - suc i) →
            Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) 
 di-next {i} {i0} {j} {j0} x =
@@ -312,6 +323,9 @@
                suc (i0 + j) ∎ ) (proj2 x) ) ⟫    
            where open ≡-Reasoning
 
+gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD (suc (suc j)) (suc i0) (suc i0 + suc j) (suc (suc j))
+gcd-next1 = ?
+
 di-next1 : {i0 j j0 : ℕ} →  Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∧ Dividable j0 (suc (i0 + suc (suc j)))
        →    Dividable (suc i0) ((suc (suc j) + i0) - suc j) ∧ Dividable (suc (suc j)) ((suc i0 + suc j) - i0)
 di-next1 {i0} {j} {j0} x =