Mercurial > hg > Papers > 2021 > soto-prosym
diff Paper/src/agda-mdg.agda.replaced @ 5:339fb67b4375
INIT rbt.agda
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Nov 2021 00:51:16 +0900 |
| parents | c59202657321 |
| children |
line wrap: on
line diff
--- a/Paper/src/agda-mdg.agda.replaced Sat Nov 06 20:06:24 2021 +0900 +++ b/Paper/src/agda-mdg.agda.replaced Sun Nov 07 00:51:16 2021 +0900 @@ -4,7 +4,7 @@ sf : whileTestState -whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set -whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) -whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) -whileTestStateP sf env = (vari env @$\equiv$@ c10 env) +whileTestStateP : whileTestState !$\rightarrow$! Envc !$\rightarrow$! Set +whileTestStateP s1 env = (vari env !$\equiv$! 0) !$\wedge$! (varn env !$\equiv$! c10 env) +whileTestStateP s2 env = (varn env + vari env !$\equiv$! c10 env) +whileTestStateP sf env = (vari env !$\equiv$! c10 env)