# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576826032 -32400
# Node ID 3adf50622101b259241903f7198127d351694d74
# Parent  03235251b3a70ba2ce3ff1dfe8e0e518c422db1d
...

diff -r 03235251b3a7 -r 3adf50622101 whileTestGears.agda
--- a/whileTestGears.agda	Fri Dec 20 15:57:17 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 20 16:13:52 2019 +0900
@@ -143,25 +143,25 @@
    env : Envc
    env = whileTestP c10 ( λ env → env )
 
-whileLoopPwP : {l : Level} {t : Set l} → Envc
+whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env 
     → (next : (env : Envc ) → whileTestStateP s2 env  → t)
     → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-whileLoopPwP env next exit with <-cmp 0 (varn env)
-whileLoopPwP env next exit | tri≈ ¬a b ¬c = exit env {!!}
-whileLoopPwP env next exit | tri< a ¬b ¬c =
+whileLoopPwP env s next exit with <-cmp 0 (varn env)
+whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env {!!}
+whileLoopPwP env s next exit | tri< a ¬b ¬c =
      next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!}
 
 {-# TERMINATING #-}
-loopPwP : {l : Level} {t : Set l} → Envc → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
-loopPwP env exit = whileLoopPwP env (λ env s → loopPwP env exit ) exit
+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
 
-whileTestPCallwP : (c10 :  ℕ ) → Set
-whileTestPCallwP c10 = whileTestPwP {_} {_} c10 (λ env → loopPwP env (λ env x x1 → vari env ≡ c10 )) 
+whileTestPCallwP : (c :  ℕ ) → Set
+whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (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 = {!!}
 
 
 
 
 
 
-
-