proposition: Lemma ind_RV_DEC: forall (P: NodePred V -> list V -> NodePred V -> Prop), (forall m m', (m ~=~ m')%NodePred -> P m nil m') -> (forall m v m' l m'', P m' l m'' -> forall (R_DEC: forall x, In x (v :: l) -> ReachDecidable g x (negateP m)) (V_DEC: forall x, In x (v :: l) -> Decidable (vvalid g x)), mark m v m' -> mark_list m' l m'' -> P m (v :: l) m'') -> (forall m l m', (forall x, In x l -> ReachDecidable g x (negateP m)) -> (forall x, In x l -> Decidable (vvalid g x)) -> mark_list m l m' -> P m l m').
proof: Proof. intros P H_nil IH m l m' R_DEC V_DEC ?. induction H. + apply H_nil; auto. + apply (IH m v m0 vs m1); auto. apply IHmark_list. - destruct (V_DEC v (or_introl eq_refl)) as [?H | ?H]. * intros. apply (mark_preserved_reach_decidable m v); auto. 1: apply R_DEC; right; auto. 1: apply R_DEC; left; auto. * pose proof mark_invalid m v m0 H1 H. intros. apply (ReachDecidable_si g g (negateP m)); [reflexivity | | apply R_DEC; right; auto]. hnf in H2 |- *; clear - H2. intros; specialize (H2 x). rewrite !negateP_spec; tauto. - intros; apply V_DEC; right; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2