--- a/whileTestGears.agda	Thu Jan 02 20:22:24 2020 +0900
+++ b/whileTestGears.agda	Mon Jan 06 16:02:31 2020 +0900
@@ -164,7 +164,7 @@
 whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
   where
     lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
-    lem p1 p2 rewrite p1 = p2
+    lem refl refl = refl
 whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
   where
     1<0 : 1 ≤ zero → ⊥
@@ -187,10 +187,23 @@
          c10 env
       ∎
 
+
+whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
+  → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
+  → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP' zero env refl refl next exit = exit env refl
+whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
+
+
 {-# TERMINATING #-}
 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
 
+
+loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
+loopPwP' zero env refl refl exit = exit env refl
+loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit
+
 --  all codtions are correctly connected and required condtion is proved in the continuation
 --      use required condition as t in (env → t) → t
 whileTestPCallwP : (c :  ℕ ) → Set
@@ -198,6 +211,26 @@
    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
    conv e record { pi1 = refl ; pi2 = refl } = +zero
 
+test : whileTestPCallwP 100
+test = refl
+
+-- pt : (c : ℕ) → whileTestPCallwP c
+-- pt c with <-cmp 0 c
+-- ... | tri≈ ¬a b ¬c = refl
+-- ... | tri< a ¬b ¬c = refl
+
+whileTestPCallwP' : (c :  ℕ ) → Set
+whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c )  ) where
+  conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+  conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+
+{-- Nat だとできるけど 300 あたりから処理に時間がかかる --}
+test' : whileTestPCallwP' 100
+test' = refl
+
+
+
 --
 -- Using imply relation to make soundness explicit
 -- termination is shown by induction on varn