proposition: Lemma triple1_mark: forall (g g1 g2: Graph) root l l_done son l_later, vvalid g root -> (unmarked g) root -> let marked' := Union _ (marked g) (eq root) in step_list g root l -> l = l_done ++ son :: l_later -> let PV1 := reachable_by_through_set g l_done (Complement _ marked') in (predicate_partialgraph g (Complement _ (Union _ PV1 (eq root)))) ~=~ (predicate_partialgraph g1 (Complement _ (Union _ PV1 (eq root)))) /\ Same_set (marked g1) (Union _ marked' PV1) -> mark son g1 g2 -> let PV2 := reachable_by_through_set g (l_done ++ son :: nil) (Complement _ marked') in (predicate_partialgraph g (Complement _ (Union _ PV2 (eq root)))) ~=~ (predicate_partialgraph g2 (Complement _ (Union _ PV2 (eq root)))).
proof: Proof. intros. destruct H3 as [PRE_psi PRE_unm]. destruct H4 as [? _]. transitivity (predicate_partialgraph g1 (Complement _ (Union _ PV2 (eq root)))). + eapply si_stronger_partialgraph_simple; [| exact PRE_psi]. apply Complement_Included_rev. unfold PV2; rewrite reachable_by_through_app'. rewrite !(Union_comm _ _ (eq root)), <- Union_assoc. apply left_Included_Union. + eapply si_stronger_partialgraph_simple; [| exact H3]. unfold PV2. eapply Included_trans. - apply Complement_Included_rev. apply left_Included_Union. - rewrite Complement_reachable_by_through_app_strong. unfold unmarked. rewrite negateP_spec'. rewrite PRE_unm. rewrite (Union_comm _ marked'). rewrite (triple_mark_aux1' g PV1 root marked') by auto. rewrite reachable_by_eq_partialgraph_reachable'. rewrite <- Intersection_Complement. rewrite <- partial_partialgraph, <- PRE_psi. rewrite <- reachable_by_eq_partialgraph_reachable'. rewrite reachable_by_through_singleton'. apply Intersection2_Included. rewrite !reachable_by_eq_partialgraph_reachable', !partial_partialgraph. rewrite Intersection_Complement. rewrite (triple_mark_aux1' g _ root marked') by auto. rewrite Intersection_Complement. apply Included_refl. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Classes.Morphisms VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.lib.relation_list CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.subgraph2 CertiGraph.graph.dual_graph