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