# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624843366 -32400
# Node ID d475257ffe30172ede473fd37a888c1b1ab82780
# Parent  3aad251b8d8b816980c72b4521f7d130e4a65d7f
...

diff -r 3aad251b8d8b -r d475257ffe30 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 09:30:41 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 10:22:46 2021 +0900
@@ -536,6 +536,29 @@
 ge3 : {a b c d : ℕ } → b > a → b - a ≡ d - c → d > c
 ge3 {a} {b} {c} {d} b>a eq = minus>0→x<y (subst (λ k → 0 < k ) eq (minus>0 b>a))
 
+ge00 : ( i0 j j0 ea eb : ℕ )  
+   → ( di : GCD 0 (suc i0) (suc (suc j)) j0 )
+  → (ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0 > eb * j0
+  → (((ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0) - (eb * j0)) ≡ (ea * suc i0) - (eb * suc (suc j))       
+ge00 i0 j j0 ea eb di lt = ge1 where
+   f = Dividable.factor (GCD.div-i di)
+   ge4 :  suc (j0 + 0) > suc (suc j)
+   ge4 = subst (λ k → k > suc (suc j)) (+-comm 0 _ ) ( s≤s (GCD.j<j0  di ))
+   ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
+   ge1  = begin
+      ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm 0 _) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (j0 + 0) )  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (sym (minus+n {j0 + 0} {suc (suc j)} ge4 )) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (((j0 + 0) -  suc (suc j)) + suc (suc j)  )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm _ (suc (suc j)) ) ⟩
+      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + ((j0 + 0) -  suc (suc j))))
+              ≡⟨ cong (λ k → ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k) )) (sym (Dividable.is-factor (GCD.div-i di))) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k))) (+-comm _ 0) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 ) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - k) (*-distribˡ-+  eb (suc (suc j)) (f * suc i0)) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * suc (suc j) + eb * (f * suc i0)) ≡⟨ cong (λ k → k - (eb * suc (suc j) + eb * (f * suc i0))) (*-distribʳ-+ (suc i0)  ea  _) ⟩ 
+      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + (eb * (f * (suc i0))) )
+           ≡⟨ cong (λ k →  (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + k )) (sym (*-assoc eb _ _ )) ⟩ 
+      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) )   ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)}  ⟩ 
+      (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
+
 gcd-equlid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Equlid i0 j0 (gcd1 i i0 j j0)
 gcd-equlid1 zero i0 zero j0 di with <-cmp i0 j0
 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!}  }
@@ -544,30 +567,14 @@
 gcd-equlid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
 gcd-equlid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
 gcd-equlid1 zero (suc i0) (suc (suc j)) j0 di with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
-... | e = record { eqa = ea + eb * f ; eqb =  eb ;  is-equ< = ge0 ; is-equ> = {!!} } where
+... | e = record { eqa = ea + eb * f ; eqb =  eb
+      ;  is-equ< =  λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Equlid.is-equ< e (ge3 lt (ge1 lt))) (ge1 lt) ; is-equ> = {!!} } where
    ea = Equlid.eqa e 
    eb = Equlid.eqb e
    f = Dividable.factor (GCD.div-i di)
-   ge4 :  suc (j0 + 0) > suc (suc j)
-   ge4 = subst (λ k → k > suc (suc j)) (+-comm 0 _ ) ( s≤s (GCD.j<j0  di))
-   ge0 : (ea + eb * f) * suc i0 > eb * j0 → (((ea + eb * f) * suc i0) - (eb * j0)) ≡ gcd1 i0 (suc i0) (suc j) (suc (suc j))
-   ge0 lt = subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Equlid.is-equ< e ge2 ) ge1 where
-    ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
-    ge1  = begin
-      ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm 0 _) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (j0 + 0) )  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (sym (minus+n {j0 + 0} {suc (suc j)} ge4 )) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (((j0 + 0) -  suc (suc j)) + suc (suc j)  )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm _ (suc (suc j)) ) ⟩
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + ((j0 + 0) -  suc (suc j))))
-              ≡⟨ cong (λ k → ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k) )) (sym (Dividable.is-factor (GCD.div-i di)))  ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k))) (+-comm _ 0) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 ) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - k) (*-distribˡ-+  eb (suc (suc j)) (f * suc i0)) ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * suc (suc j) + eb * (f * suc i0)) ≡⟨ cong (λ k → k - (eb * suc (suc j) + eb * (f * suc i0))) (*-distribʳ-+ (suc i0)  ea  _) ⟩ 
-      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + (eb * (f * (suc i0))) )
-           ≡⟨ cong (λ k →  (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + k )) (sym (*-assoc eb _ _ )) ⟩ 
-      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) )   ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)}  ⟩ 
-      (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
-    ge2 : ea * suc i0 > eb * suc (suc j)
-    ge2 = ge3 lt ge1 
+   ge1 : (ea + eb * Dividable.factor (GCD.div-i di)) * suc i0 > eb * j0 → ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
+   ge1 lt = ge00  i0 j j0 ea eb di lt
+
 gcd-equlid1 (suc zero) i0 zero j0 di = {!!} 
 gcd-equlid1 (suc (suc i)) i0 zero zero di = {!!}
 gcd-equlid1 (suc (suc i)) i0 zero (suc j0) di with gcd-equlid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di)))