|
4
|
1 stmt2Cond : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Cond
|
|
2
|
2 stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0)
|
|
|
3
|
|
7
|
4 lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10})
|
|
|
5 (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
|
|
4
|
6 lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
7
|
7 begin
|
|
|
8 ? -- ?0
|
|
|
9 @$\equiv$@@$\langle$@ ? @$\rangle$@ -- ?1
|
|
|
10 ? -- ?2
|
|
|
11 @$\blacksquare$@ )
|
|
2
|
12
|
|
|
13 -- ?0 : Bool
|
|
|
14 -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) @$\equiv$@ true
|
|
|
15 -- ?2 : Bool
|
