--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/cbc-hoare.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,14 @@
+whileTestPwP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+  env : Envc
+  env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )
+
+loopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env !$\rightarrow$! t) !$\rightarrow$! t
+loopPwP!$\prime$! zero env refl refl exit = exit env refl
+loopPwP!$\prime$! (suc n) env refl refl exit  = whileLoopPwP!$\prime$! (suc n) env refl refl (!$\lambda$! env x y !$\rightarrow$! loopPwP!$\prime$! n env x y exit) exit
+
+
+whileTestPCallwP!$\prime$! : (c :  !$\mathbb{N}$! ) !$\rightarrow$! Set
+whileTestPCallwP!$\prime$! c = whileTestPwP {_} {_} c (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (varn env) env refl (conv env s) ( !$\lambda$! env s !$\rightarrow$! vari env !$\equiv$! c10 env )  )
+
+