--- a/whileTestGears1.agda	Sun Oct 31 23:43:06 2021 +0900
+++ b/whileTestGears1.agda	Mon Nov 01 08:34:07 2021 +0900
@@ -156,27 +156,33 @@
        lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 lt1 eq lt1 
     ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
-TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set ) → (ExitCond : Set) → ( reduce : Index → ℕ)
-   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → (exit : ExitCond → t) → t)
-   → (i : ℕ) → (r : Index) → reduce r ≡ i  → (p : Invraiant r)  → (exit : ExitCond → t)  → t 
+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 ) → (ExitCond : Index → Set) → ( reduce : Index → ℕ)
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → (exit : (re : Index) → ExitCond re → t) → t)
+   → (i : ℕ) → (r : Index) → reduce r ≡ i  → (p : Invraiant r)  → (exit : (re : Index) → ExitCond re → t)  → t 
 TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop  i r refl p exit with <-cmp 0 i
 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) exit 
-... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r1) r1  {!!} {!!} {!!} {!!} ) exit where 
-    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r →  reduce r1 < reduce r → t
-    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j {!!})) exit  
-    TerminatingLoop1 (suc j) r r1  n≤j p lt with <-cmp (reduce r1) (suc j)
-    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p lt 
-    ... | tri≈ ¬a b ¬c = loop {!!} {!!} {!!} {!!} where
-       lemma4 : (r1 : Index) → Invraiant r → reduce r1 < reduce r  → t
-       lemma4 r1 p1 lt1 = TerminatingLoop1 (reduce r1) r r1 {!!} p1 lt1 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 i r r1 (≤-step lt1) p1 lt1 ) exit where 
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
+    ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 exit where
+       lemma4 : (r2 : Index) → Invraiant r2 → reduce r2 < reduce r1  → t
+       lemma4 r2 p2 lt1 = TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1  
     ... | 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 ))) 
+proofGearsTermS : {c10 :  ℕ } → ⊤
+proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
+    TerminatingLoopS Env (λ env → varn env + vari env ≡ c10) (λ e1 → vari e1 ≡ c10) (λ env → varn env)
+        (λ n2 p2 loop exit → whileLoopSeg {_} {_} {c10} n2 p2 loop exit) (varn n1) n1 refl p1 (λ ne pe → whileTestSpec1 c10 ne pe))) 
 
 
 
 
 
 
+
+