Mercurial > hg > Papers > 2021 > soto-prosym
view Paper/src/cbc-hoare-loophelper.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
loopHelper : (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (eq : varn env !$\equiv$! n) !$\rightarrow$! (seq : whileTestStateP s2 env) !$\rightarrow$! loopPwP!$\prime$! n env (sym eq) seq (!$\lambda$! env!$\_{1}$! x !$\rightarrow$! (vari env!$\_{1}$! !$\equiv$! c10 env!$\_{1}$!)) loopHelper zero env eq refl rewrite eq = refl loopHelper (suc n) env refl refl = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))