--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/cbc-hoare-soundness.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,13 @@
+whileCallwP : (c : !$\mathbb{N}$!) !$\rightarrow$! whileTestPCallwP!$\prime$! c
+whileCallwP c = whileTestPwP {_} {_} c
+  (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (c10 env) env (sym (pi2 s)) (conv env s) {!!})
+
+
+-- Goal: (env!$\_{1}$! : Envc) !$\rightarrow$!
+--        vari env!$\_{1}$! !$\equiv$! c10 env!$\_{1}$! !$\rightarrow$!
+--        loopPwP!$\prime$! c (whileTestP c (!$\lambda$! env!$\_{2}$! !$\rightarrow$! env!$\_{2}$!)) refl +zero
+--        (!$\lambda$! env!$\_{2}$! s!$\_{1}$! !$\rightarrow$! vari env!$\_{2}$! !$\equiv$! c10 env!$\_{2}$!)
+-- ————————————————————————
+-- s   : (vari env !$\equiv$! 0) !$\wedge$! (varn env !$\equiv$! c10 env)
+-- env : Envc
+-- c   : !$\mathbb{N}$!