view paper/src/cbc-hoare-while.agda.replaced @ 19:046b2b20d6c7 default tip

fix
author ryokka
date Mon, 09 Mar 2020 11:25:49 +0900
parents
children
line wrap: on
line source

whileCallwP : (c :  @$\mathbb{N}$@ ) @$\rightarrow$@ Set
whileCallwP c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (varn env) env refl (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env )  )
  where
    conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env
    conv e record { pi1 = refl ; pi2 = refl } = +zero