--- a/whileTestGears.agda	Sat Apr 08 07:49:41 2023 +0900
+++ b/whileTestGears.agda	Sat Apr 08 07:52:36 2023 +0900
@@ -56,31 +56,6 @@
 lemma1 {zero} not = refl
 lemma1 {suc i} not = ⊥-elim ( not (s≤s z≤n) )
 
-{-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
-whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10)
-   → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t
-whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
-whileLoop' env {c10} proof next | no p = next env ( begin
-       vari env            ≡⟨ refl ⟩
-       0 + vari env        ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩
-       varn env + vari env ≡⟨ proof ⟩
-       c10 ∎ ) where open ≡-Reasoning  
-whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where
-      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
-      1<0 : 1 ≤ zero → ⊥
-      1<0 ()
-      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
-      proof3 (s≤s lt) with varn  env
-      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
-      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in begin
-             n' + (vari env + 1)  ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-             n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1) + vari env  ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-             (suc n' ) + vari env ≡⟨⟩
-             varn env + vari env  ≡⟨ proof  ⟩
-             c10
-          ∎
-
 -- Condition to Invaliant
 conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
                → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
@@ -98,10 +73,6 @@
 whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
 whileTestSpec1 _ _ x = tt
 
-proofGears : {c10 :  ℕ } → ⊤
-proofGears {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
-
---                                                                      ↓PreCondition(Invaliant)
 whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
    → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)     -- next with PostCondition
    → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
@@ -141,22 +112,6 @@
 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
 lemma5 (s≤s z≤n) ()
 
-TerminatingLoop : {l : Level} {t : Set l} {c10 :  ℕ } → (i : ℕ) → (env : Env) → i ≡ varn env
-   →  varn env + vari env ≡ c10 
-   →  (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
-TerminatingLoop {_} {t} {c10} i env refl p exit with <-cmp 0 i
-... | tri≈ ¬a b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 eq lt → ⊥-elim (lemma3 b lt) ) exit 
-... | tri< a ¬b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 p1 lt1 → TerminatingLoop1 i env e1 (≤-step lt1) p1 lt1 ) exit where --  varn e1 < suc (varn env)
-    TerminatingLoop1 : (j : ℕ) → (env e1 : Env) → varn e1 < suc j  → varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t
-    TerminatingLoop1 zero env e1 n≤j eq lt = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
-    TerminatingLoop1 (suc j) env e1 n≤j eq lt with <-cmp (varn e1) (suc j)
-    ... | tri< a ¬b ¬c = TerminatingLoop1 j env e1 a eq lt 
-    ... | tri≈ ¬a refl ¬c = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → TerminatingLoop1 j e1 e2 lt1 eq lt1 ) exit 
-    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
-
-proofGearsTerm : {c10 :  ℕ } → ⊤
-proofGearsTerm {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → TerminatingLoop (varn n1) n1 refl p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
-
 TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
    → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t)
    → (r : Index) → (p : Invraiant r)  → t