proposition: Lemma typed_true_tag: forall (to : nat) (g : LGraph) (index : nat), typed_true tint (force_val (option_map (fun b : bool => Val.of_bool (negb b)) (bool_val_i (Val.of_bool (negb (Int.lt (Int.repr (raw_tag (vlabel g (to, index)))) (Int.repr 251))))))) -> ~ no_scan g (to, index).
proof: Proof. intros. remember (Int.lt (Int.repr (raw_tag (vlabel g (to, index)))) (Int.repr 251)). unfold typed_true in H. destruct b; simpl in H; [|inversion H]. symmetry in Heqb. apply lt_repr in Heqb. - unfold no_scan. rep_lia. - red. pose proof (raw_tag_range (vlabel g (to, index))). rep_lia. - red. rep_lia. Qed.
imports: VST.veric.rmaps CertiGraph.lib.List_ext CertiGraph.graph.graph_model Coq.Program.Basics CertiGraph.graph.graph_gen CertiGraph.CertiGC.GCGraph VST.msl.wand_frame CertiGraph.CertiGC.env_graph_gc CertiGraph.CertiGC.spatial_gcgraph CertiGraph.msl_ext.iter_sepcon CertiGraph.CertiGC.gc_spec CertiGraph.msl_ext.ramification_lemmas