1theory Proc2
2imports "HOL-SPARK.SPARK"
3begin
4
5spark_open \<open>loop_invariant/proc2\<close>
6
7spark_vc procedure_proc2_7
8  by (simp add: ring_distribs mod_simps)
9
10spark_end
11
12end
13