# HG changeset patch
# User ryokka
# Date 1576831556 -32400
# Node ID 1be7bb658cf0eafb2594bb52238dda150f0d2698
# Parent  3adf50622101b259241903f7198127d351694d74
proof whileLoopPwP tri= case, conv

diff -r 3adf50622101 -r 1be7bb658cf0 whileTestGears.agda
--- a/whileTestGears.agda	Fri Dec 20 16:13:52 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 20 17:45:56 2019 +0900
@@ -147,7 +147,11 @@
     → (next : (env : Envc ) → whileTestStateP s2 env  → t)
     → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
 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 = 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
+
 whileLoopPwP env s next exit | tri< a ¬b ¬c =
      next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!}
 
@@ -158,10 +162,14 @@
 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 = {!!}
+    conv e record { pi1 = refl ; pi2 = refl } = +zero
+
+Proof : (c :  ℕ ) → whileTestPCallwP c
+Proof c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → {!!} ) ) 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
 
 
 
 
 
-