# HG changeset patch
# User ryokka
# Date 1575886088 -32400
# Node ID 835b2d53815ea66f982845df1181e4163517935c
# Parent  a39a828207421701ff805b5b994287aca1800548
coinduction

diff -r a39a82820742 -r 835b2d53815e whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 09 18:47:31 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 09 19:08:08 2019 +0900
@@ -104,7 +104,7 @@
 
 
 record whileTestCondition  (c10 : ℕ)  (t : whileTestState)  : Set where
-  inductive
+  coinductive
   field
     case1 : (env : Env)  → (t ≡ state1) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestCondition c10 state2
     case2 : (env : Env) → (t ≡ state2)  → (varn env + vari env ≡ c10) → whileTestCondition c10 state2
@@ -112,14 +112,12 @@
 open whileTestCondition
 
 test2 : (c10 : ℕ) → whileTestCondition c10 state1 → whileTestCondition c10 state2 
-test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → proof3 env1 cond1 ))
+test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → proof3 env env1 cond1 ))
   where    
     whileLoopCond : (e env1 : Env) → varn env1 + vari env1 ≡ c10 → varn e + vari e ≡ c10 → whileTestCondition c10 state2
     whileLoopCond = {!!}
-    proof2 : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
-    proof2 env = record {pi1 = {!!} ; pi2 = {!!}}
-    proof3 : (env : Env) → whileTestCondition c10 state1 → whileTestCondition c10 state2
-    proof3 env cond1 = record {
-                          case1 = λ e ()
-                          ; case2 = λ e refl → conversion1 e {c10} (record { pi1 = {!!} ; pi2 = {!!} }) {!!}
-                          }
+    proof3 : (env env1 : Env) → whileTestCondition c10 state1 → whileTestCondition c10 state2
+    case1 (proof3 env env1 cond1) e ()
+    case2 (proof3 env env1 cond1) e refl cond2 = {!!}
+
+-- conversion1 e {c10} (case2  (case1 cond1 ? ? ?)) {!!}