Mercurial > hg > Papers > 2022 > soto-sigos
annotate Paper/src/cbc-hoare-soundness.agda.replaced @ 0:14a0e409d574
ADD fast commit
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Apr 2022 23:13:44 +0900 |
| parents | |
| children |
| rev | line source |
|---|---|
| 0 | 1 whileCallwP : (c : !$\mathbb{N}$!) !$\rightarrow$! whileTestPCallwP!$\prime$! c |
| 2 whileCallwP c = whileTestPwP {_} {_} c | |
| 3 (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (c10 env) env (sym (pi2 s)) (conv env s) {!!}) | |
| 4 | |
| 5 | |
| 6 -- Goal: (env!$\_{1}$! : Envc) !$\rightarrow$! | |
| 7 -- vari env!$\_{1}$! !$\equiv$! c10 env!$\_{1}$! !$\rightarrow$! | |
| 8 -- loopPwP!$\prime$! c (whileTestP c (!$\lambda$! env!$\_{2}$! !$\rightarrow$! env!$\_{2}$!)) refl +zero | |
| 9 -- (!$\lambda$! env!$\_{2}$! s!$\_{1}$! !$\rightarrow$! vari env!$\_{2}$! !$\equiv$! c10 env!$\_{2}$!) | |
| 10 -- ———————————————————————— | |
| 11 -- s : (vari env !$\equiv$! 0) !$\wedge$! (varn env !$\equiv$! c10 env) | |
| 12 -- env : Envc | |
| 13 -- c : !$\mathbb{N}$! |