Mercurial > hg > Papers > 2021 > soto-prosym
view Paper/src/sound-conv.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 source
whileConvPSemSound : {l : Level} !$\rightarrow$! (input : Envc) !$\rightarrow$! ((vari input !$\equiv$! 0) !$\wedge$! (varn input !$\equiv$! c)) implies (varn input + vari input !$\equiv$! c10 input) whileConvPSemSound input = proof !$\lambda$! x !$\rightarrow$! (conversion input x) where conversion : (env : Envc ) !$\rightarrow$! (vari env !$\equiv$! 0) !$\wedge$! (varn env !$\equiv$! c10 env) !$\rightarrow$! varn env + vari env !$\equiv$! c10 env conversion e record { pi1 = refl ; pi2 = refl } = +zero