# HG changeset patch
# User ryokka
# Date 1576913754 -32400
# Node ID 990d1d8923989369b964508ac9b4625e988fe390
# Parent  34601fe34b713d3c2861c9f43ab4a4d98eaeec31
Maybe All Proof. but Non-Terminating

diff -r 34601fe34b71 -r 990d1d892398 whileTestGears.agda
--- a/whileTestGears.agda	Sat Dec 21 15:47:30 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 16:35:54 2019 +0900
@@ -183,12 +183,7 @@
     conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
     conv e record { pi1 = refl ; pi2 = refl } = +zero
 
+{-# TERMINATING #-}
 Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof zero = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → refl))
-  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
-Proof (suc c) = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → {!!})) -- Proof c したいが with <-cmp 0 c とか with 0 ≤ c とかするとAgda の check が終わらない
-  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
+Proof zero = whileTestPwP {_} {_} zero (λ env s → refl)
+Proof (suc c) = Proof (suc c)