1
theory Proc2
2
imports SPARK
3
begin
4
5
spark_open "loop_invariant/proc2.siv"
6
7
spark_vc procedure_proc2_7
8
by (simp add: ring_distribs pull_mods)
9
10
spark_end
11
12
end