|
0
|
1 whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
2 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
|
|
|
3 env : Envc
|
|
|
4 env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )
|
|
|
5
|
|
|
6 loopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
7 loopPwP' zero env refl refl exit = exit env refl
|
|
|
8 loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl (@$\lambda$@ env x y @$\rightarrow$@ loopPwP' n env x y exit) exit
|
|
|
9
|
|
|
10
|
|
|
11 whileTestPCallwP' : (c : @$\mathbb{N}$@ ) @$\rightarrow$@ Set
|
|
|
12 whileTestPCallwP' c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (varn env) env refl (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env ) )
|
|
|
13
|
|
|
14
|
