|
0
|
1 module whileTestPrimProof where
|
|
|
2
|
|
|
3 open import Function
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ )
|
|
|
6 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
7 open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9
|
|
|
10 open import utilities hiding ( _@$\wedge$@_ )
|
|
|
11 open import whileTestPrim
|
|
|
12
|
|
|
13 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
|
|
|
14
|
|
|
15 open Env
|
|
|
16
|
|
|
17 initCond : Cond
|
|
|
18 initCond env = true
|
|
|
19
|
|
|
20 stmt1Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond
|
|
|
21 stmt1Cond {c10} env = Equal (varn env) c10
|
|
|
22
|
|
|
23 init-case : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (( @$\lambda$@ e @$\rightarrow$@ true @$\Rightarrow$@ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) @$\equiv$@ true
|
|
|
24 init-case {c10} _ = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ @$\equiv$@@$\rightarrow$@Equal refl )
|
|
|
25
|
|
|
26 init-type : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (@$\lambda$@ env @$\rightarrow$@ true) (@$\lambda$@ env @$\rightarrow$@ record { varn = c10 ; vari = vari env }) (stmt1Cond {c10})
|
|
|
27 init-type {c10} env = init-case env
|
|
|
28
|
|
|
29 stmt2Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond
|
|
|
30 stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0)
|
|
|
31
|
|
|
32 lemma1 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
|
|
|
33 lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
|
34 begin
|
|
|
35 (Equal (varn env) c10 ) @$\wedge$@ true
|
|
|
36 @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@
|
|
|
37 Equal (varn env) c10
|
|
|
38 @$\equiv$@@$\langle$@ cond @$\rangle$@
|
|
|
39 true
|
|
|
40 @$\blacksquare$@ )
|
|
|
41
|
|
|
42 -- simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm
|
|
|
43 -- simple c10 =
|
|
|
44 -- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
|
|
|
45 -- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})
|
|
|
46
|
|
|
47 proofs : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (simple c10) (stmt2Cond {c10})
|
|
|
48 proofs c10 =
|
|
|
49 SeqRule {initCond} ( PrimRule (init-case {c10} ))
|
|
|
50 $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10})
|
|
|
51
|
|
|
52 open import Data.Empty
|
|
|
53
|
|
|
54 open import Data.Nat.Properties
|
|
|
55
|
|
|
56 whileInv : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond
|
|
|
57 whileInv {c10} env = Equal ((varn env) + (vari env)) c10
|
|
|
58
|
|
|
59 whileInv' : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond
|
|
|
60 whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) @$\wedge$@ lt zero (varn env)
|
|
|
61
|
|
|
62 termCond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond
|
|
|
63 termCond {c10} env = Equal (vari env) c10
|
|
|
64
|
|
|
65
|
|
|
66 -- program : @$\mathbb{N}$@ @$\rightarrow$@ Comm
|
|
|
67 -- program c10 =
|
|
|
68 -- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
|
|
|
69 -- $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}))
|
|
|
70 -- $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) )
|
|
|
71 -- (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} ))
|
|
|
72 -- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} ))
|
|
|
73
|
|
|
74
|
|
|
75 proof1 : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (program c10 ) (termCond {c10})
|
|
|
76 proof1 c10 =
|
|
|
77 SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule (init-case {c10} ))
|
|
|
78 $ SeqRule {@$\lambda$@ e @$\rightarrow$@ Equal (varn e) c10} ( PrimRule lemma1 )
|
|
|
79 $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) c10) @$\wedge$@ (Equal (vari e) 0)} lemma2 (
|
|
|
80 WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) c10}
|
|
|
81 $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e) } lemma3 )
|
|
|
82 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
|
|
|
83 where
|
|
|
84 lemma21 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env @$\equiv$@ c10
|
|
|
85 lemma21 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 eq)
|
|
|
86 lemma22 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond {c10} env @$\equiv$@ true @$\rightarrow$@ vari env @$\equiv$@ 0
|
|
|
87 lemma22 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi2 eq)
|
|
|
88 lemma23 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env + vari env @$\equiv$@ c10
|
|
|
89 lemma23 {env} {c10} eq = let open @$\equiv$@-Reasoning in
|
|
|
90 begin
|
|
|
91 varn env + vari env
|
|
|
92 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x + vari env ) (lemma21 eq ) @$\rangle$@
|
|
|
93 c10 + vari env
|
|
|
94 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ c10 + x) (lemma22 {env} {c10} eq ) @$\rangle$@
|
|
|
95 c10 + 0
|
|
|
96 @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@
|
|
|
97 0 + c10
|
|
|
98 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
99 c10
|
|
|
100 @$\blacksquare$@
|
|
|
101 lemma2 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology stmt2Cond whileInv
|
|
|
102 lemma2 {c10} env = bool-case (stmt2Cond env) (
|
|
|
103 @$\lambda$@ eq @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
|
104 begin
|
|
|
105 (stmt2Cond env) @$\Rightarrow$@ (whileInv env)
|
|
|
106 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
107 (stmt2Cond env) @$\Rightarrow$@ ( Equal (varn env + vari env) c10 )
|
|
|
108 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ ( Equal x c10 ) ) ( lemma23 {env} eq ) @$\rangle$@
|
|
|
109 (stmt2Cond env) @$\Rightarrow$@ (Equal c10 c10)
|
|
|
110 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ x ) (@$\equiv$@@$\rightarrow$@Equal refl ) @$\rangle$@
|
|
|
111 (stmt2Cond {c10} env) @$\Rightarrow$@ true
|
|
|
112 @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@
|
|
|
113 true
|
|
|
114 @$\blacksquare$@
|
|
|
115 ) (
|
|
|
116 @$\lambda$@ ne @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
|
117 begin
|
|
|
118 (stmt2Cond env) @$\Rightarrow$@ (whileInv env)
|
|
|
119 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x @$\Rightarrow$@ (whileInv env) ) ne @$\rangle$@
|
|
|
120 false @$\Rightarrow$@ (whileInv {c10} env)
|
|
|
121 @$\equiv$@@$\langle$@ f@$\Rightarrow$@ {whileInv {c10} env} @$\rangle$@
|
|
|
122 true
|
|
|
123 @$\blacksquare$@
|
|
|
124 )
|
|
|
125 lemma3 : Axiom (@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e)) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = vari env + 1 }) whileInv'
|
|
|
126 lemma3 env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
|
127 begin
|
|
|
128 whileInv' (record { varn = varn env ; vari = vari env + 1 })
|
|
|
129 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
130 Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ (lt 0 (varn env) )
|
|
|
131 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ z ) (@$\wedge$@-pi2 cond ) @$\rangle$@
|
|
|
132 Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ true
|
|
|
133 @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@
|
|
|
134 Equal (varn env + (vari env + 1)) (suc c10)
|
|
|
135 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) @$\rangle$@
|
|
|
136 Equal ((varn env + vari env) + 1) (suc c10)
|
|
|
137 @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) +1@$\equiv$@suc @$\rangle$@
|
|
|
138 Equal (suc (varn env + vari env)) (suc c10)
|
|
|
139 @$\equiv$@@$\langle$@ sym Equal+1 @$\rangle$@
|
|
|
140 Equal ((varn env + vari env) ) c10
|
|
|
141 @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@
|
|
|
142 true
|
|
|
143 @$\blacksquare$@ )
|
|
|
144 lemma41 : (env : Env ) @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ (varn env + vari env) @$\equiv$@ (suc c10) @$\rightarrow$@ lt 0 (varn env) @$\equiv$@ true @$\rightarrow$@ Equal ((varn env - 1) + vari env) c10 @$\equiv$@ true
|
|
|
145 lemma41 env {c10} c1 c2 = let open @$\equiv$@-Reasoning in
|
|
|
146 begin
|
|
|
147 Equal ((varn env - 1) + vari env) c10
|
|
|
148 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-pred@$\mathbb{N}$@=n c2) ) @$\rangle$@
|
|
|
149 Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 ) - 1) + vari env) c10
|
|
|
150 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
151 Equal ((pred@$\mathbb{N}$@ {varn env} c2 ) + vari env) c10
|
|
|
152 @$\equiv$@@$\langle$@ Equal+1 @$\rangle$@
|
|
|
153 Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 )) + vari env) (suc c10)
|
|
|
154 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env ) (suc c10) ) (suc-pred@$\mathbb{N}$@=n c2 ) @$\rangle$@
|
|
|
155 Equal (varn env + vari env) (suc c10)
|
|
|
156 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ (Equal z (suc c10) )) c1 @$\rangle$@
|
|
|
157 Equal (suc c10) (suc c10)
|
|
|
158 @$\equiv$@@$\langle$@ @$\equiv$@@$\rightarrow$@Equal refl @$\rangle$@
|
|
|
159 true
|
|
|
160 @$\blacksquare$@
|
|
|
161 lemma4 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom whileInv' (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env - 1 ; vari = vari env }) whileInv
|
|
|
162 lemma4 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
|
163 begin
|
|
|
164 whileInv (record { varn = varn env - 1 ; vari = vari env })
|
|
|
165 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
166 Equal ((varn env - 1) + vari env) c10
|
|
|
167 @$\equiv$@@$\langle$@ lemma41 env (Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 cond)) (@$\wedge$@-pi2 cond) @$\rangle$@
|
|
|
168 true
|
|
|
169 @$\blacksquare$@
|
|
|
170 )
|
|
|
171 lemma51 : (z : Env ) @$\rightarrow$@ neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)) z @$\equiv$@ true @$\rightarrow$@ varn z @$\equiv$@ zero
|
|
|
172 lemma51 z cond with varn z
|
|
|
173 lemma51 z refl | zero = refl
|
|
|
174 lemma51 z () | suc x
|
|
|
175 lemma5 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology ((@$\lambda$@ e @$\rightarrow$@ Equal (varn e + vari e) c10) and (neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)))) termCond
|
|
|
176 lemma5 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in
|
|
|
177 begin
|
|
|
178 termCond env
|
|
|
179 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
180 Equal (vari env) c10
|
|
|
181 @$\equiv$@@$\langle$@@$\rangle$@
|
|
|
182 Equal (zero + vari env) c10
|
|
|
183 @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env) c10 ) (sym ( lemma51 env ( @$\wedge$@-pi2 cond ) )) @$\rangle$@
|
|
|
184 Equal (varn env + vari env) c10
|
|
|
185 @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@
|
|
|
186 true
|
|
|
187 @$\blacksquare$@
|
|
|
188 )
|
|
|
189
|
|
|
190 --- necessary definitions for Hoare.agda ( Soundness )
|
|
|
191
|
|
|
192 State : Set
|
|
|
193 State = Env
|
|
|
194
|
|
|
195 open import RelOp
|
|
|
196 module RelOpState = RelOp State
|
|
|
197
|
|
|
198 open import Data.Product
|
|
|
199 open import Relation.Binary
|
|
|
200
|
|
|
201 NotP : {S : Set} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S
|
|
|
202 NotP X s = @$\neg$@ X s
|
|
|
203
|
|
|
204 _@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond
|
|
|
205 b1 @$\wedge$@ b2 = b1 and b2
|
|
|
206
|
|
|
207 _\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond
|
|
|
208 b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2)
|
|
|
209
|
|
|
210 SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set
|
|
|
211 SemCond c p = c p @$\equiv$@ true
|
|
|
212
|
|
|
213 tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@
|
|
|
214 (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ SemCond b2 s
|
|
|
215 tautValid b1 b2 taut s cond with b1 s | b2 s | taut s
|
|
|
216 tautValid b1 b2 taut s () | false | false | refl
|
|
|
217 tautValid b1 b2 taut s _ | false | true | refl = refl
|
|
|
218 tautValid b1 b2 taut s _ | true | false | ()
|
|
|
219 tautValid b1 b2 taut s _ | true | true | refl = refl
|
|
|
220
|
|
|
221 respNeg : (b : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@
|
|
|
222 Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s)
|
|
|
223 respNeg b s = ( left , right ) where
|
|
|
224 left : not (b s) @$\equiv$@ true @$\rightarrow$@ (b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@
|
|
|
225 left ne with b s
|
|
|
226 left refl | false = @$\lambda$@ ()
|
|
|
227 left () | true
|
|
|
228 right : ((b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@) @$\rightarrow$@ not (b s) @$\equiv$@ true
|
|
|
229 right ne with b s
|
|
|
230 right ne | false = refl
|
|
|
231 right ne | true = @$\bot$@-elim ( ne refl )
|
|
|
232
|
|
|
233 respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@
|
|
|
234 Iff (SemCond (b1 @$\wedge$@ b2) s)
|
|
|
235 ((SemCond b1 s) @$\times$@ (SemCond b2 s))
|
|
|
236 respAnd b1 b2 s = ( left , right ) where
|
|
|
237 left : b1 s @$\wedge$@ b2 s @$\equiv$@ true @$\rightarrow$@ (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true)
|
|
|
238 left and with b1 s | b2 s
|
|
|
239 left () | false | false
|
|
|
240 left () | false | true
|
|
|
241 left () | true | false
|
|
|
242 left refl | true | true = ( refl , refl )
|
|
|
243 right : (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true) @$\rightarrow$@ b1 s @$\wedge$@ b2 s @$\equiv$@ true
|
|
|
244 right ( x1 , x2 ) with b1 s | b2 s
|
|
|
245 right (() , ()) | false | false
|
|
|
246 right (() , _) | false | true
|
|
|
247 right (_ , ()) | true | false
|
|
|
248 right (refl , refl) | true | true = refl
|
|
|
249
|
|
|
250 PrimSemComm : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l
|
|
|
251 PrimSemComm prim s1 s2 = Id State (prim s1) s2
|
|
|
252
|
|
|
253
|
|
|
254
|
|
|
255 axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@
|
|
|
256 (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@
|
|
|
257 SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ SemCond bPost s2
|
|
|
258 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1
|
|
|
259 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
|
|
|
260 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
|
|
|
261 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
|
|
|
262 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
|
|
|
263
|
|
|
264 open import HoareSoundness
|
|
|
265 Cond
|
|
|
266 PrimComm
|
|
|
267 neg
|
|
|
268 _and_
|
|
|
269 Tautology
|
|
|
270 State
|
|
|
271 SemCond
|
|
|
272 tautValid
|
|
|
273 respNeg
|
|
|
274 respAnd
|
|
|
275 PrimSemComm
|
|
|
276 Axiom
|
|
|
277 axiomValid
|
|
|
278
|
|
|
279 PrimSoundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
280 HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost
|
|
|
281 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
|
|
|
282
|
|
|
283
|
|
|
284 proofOfProgram : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (input output : Env )
|
|
|
285 @$\rightarrow$@ initCond input @$\equiv$@ true
|
|
|
286 @$\rightarrow$@ (SemComm (program c10) input output)
|
|
|
287 @$\rightarrow$@ termCond {c10} output @$\equiv$@ true
|
|
|
288 proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem
|
