|
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!$\prime$! : {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!$\prime$! zero env refl refl exit = exit env refl
|
|
|
8 loopPwP!$\prime$! (suc n) env refl refl exit = whileLoopPwP!$\prime$! (suc n) env refl refl (!$\lambda$! env x y !$\rightarrow$! loopPwP!$\prime$! n env x y exit) exit
|
|
|
9
|
|
|
10
|
|
|
11 whileTestPCallwP!$\prime$! : (c : !$\mathbb{N}$! ) !$\rightarrow$! Set
|
|
|
12 whileTestPCallwP!$\prime$! c = whileTestPwP {_} {_} c (!$\lambda$! env s !$\rightarrow$! loopPwP!$\prime$! (varn env) env refl (conv env s) ( !$\lambda$! env s !$\rightarrow$! vari env !$\equiv$! c10 env ) )
|
|
|
13
|
|
|
14
|
