# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576480972 -32400
# Node ID cc8de8bdbf7e1a34630cec6462425acc26505716
# Parent  b07e96029ae3716c1a67591948b2d7ba86f40ddd
...

diff -r b07e96029ae3 -r cc8de8bdbf7e whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 16 15:45:39 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 16 16:22:52 2019 +0900
@@ -140,8 +140,11 @@
     lemma : cx env ≡ pstate1 {!!}
     lemma = {!!}
 
-loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) →  cx e ≡ pstate2 {!!} → (exit : EnvP →  cx e ≡ pstate2 {!!} → t) → t
-loopPwithProof env exit = whileLoopP env (λ env → loopPwithProof env {!!} {!!} ) {!!}
+{-# TERMINATING #-}
+loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) →  cx e ≡ pstate2 {!!} → t) →  cx e ≡ pstate2 {!!} → t
+loopPwithProof env exit eq = whileLoopP env (λ env → loopPwithProof env exit {!!} ) (λ env → exit env {!!} ) where
+    lemma :  cx {!!} ≡ pstate2 {!!}
+    lemma = {!!}
 
 ConvP : (e : EnvP) → cx e ≡ pstate1 {!!} →  cx e ≡ pstate2 {!!}
 ConvP = {!!}
@@ -151,10 +154,9 @@
 
 whileTestPProof : {c :  ℕ } → Set
 whileTestPProof {c} = whileTestPwithProof  c
-    $ λ env eq → loopPwithProof env (ConvP env eq)
-    $ λ env eq → pvari env ≡ c10 env
+    $ λ env eq → loopPwithProof env (λ env eq → {!!} ) (ConvP env eq )
 
 whileTestPProofMeta : {c10 :  ℕ } →  whileTestPProof {c10}
-whileTestPProofMeta {c10} = ?
+whileTestPProofMeta {c10} = {!!}