1theory Proc1
2imports "HOL-SPARK.SPARK"
3begin
4
5spark_open \<open>loop_invariant/proc1\<close>
6
7spark_vc procedure_proc1_5
8  by (simp add: ring_distribs mod_simps)
9
10spark_vc procedure_proc1_8
11  by (simp add: ring_distribs mod_simps)
12
13spark_end
14
15lemma pow_2_32_simp: "4294967296 = (2::int)^32"
16  by simp
17
18end
19