proposition: Lemma valid_int_or_ptr_ii1: forall i, valid_int_or_ptr (Z2val (i + i + 1)).
proof: Proof. intros. simpl. first [rewrite Int.unsigned_repr_eq | rewrite Int64.unsigned_repr_eq]. rewrite Zodd_mod. apply Zeq_is_eq_bool. replace (i+i) with (2 * i)%Z by lia. rewrite <- Zmod_div_mod; try lia. - rewrite Z.mul_comm, Z.add_comm, Z_mod_plus_full. reflexivity. - compute; reflexivity. - first [now exists (Z.div Int.modulus 2) | now exists (Z.div Int64.modulus 2)]. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List