# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1635804534 -32400
# Node ID c3b08293a72e229c5d4045f895c4e1ba86914116
# Parent  a7263ecf8671c3db0af0d201d5488949ca634aff
remove exit from LoopS

diff -r a7263ecf8671 -r c3b08293a72e whileTestGears.agda
--- a/whileTestGears.agda	Mon Nov 01 09:59:43 2021 +0900
+++ b/whileTestGears.agda	Tue Nov 02 07:08:54 2021 +0900
@@ -159,25 +159,25 @@
 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)
-   → (r : Index) → (p : Invraiant r)  → (exit : (re : Index) → ExitCond re → t)  → t 
-TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop  r p exit with <-cmp 0 (reduce r)
-... | 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 r) r r1 (≤-step lt1) p1 lt1 ) exit where 
+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 
+TerminatingLoopS {_} {t} Index {Invraiant} reduce loop  r p with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) 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 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
     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
+    ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 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 )   
 
 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) n1 p1 (λ ne pe → whileTestSpec1 c10 ne pe))) 
+    TerminatingLoopS Env (λ env → varn env)
+        (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))