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