proposition: Lemma triple_mark1_componded_mark_list: forall root l_done l_later l (g1 g2: Graph), vvalid g1 root -> (unmarked g1) root -> step_list g1 root l -> l = l_done ++ l_later -> relation_list (nothing root :: mark1 root :: nothing root :: componded_mark_list root l_done :: nil) g1 g2 -> let marked' := Union _ (marked g1) (eq root) in let PV1 := reachable_by_through_set g1 l_done (Complement _ marked') in (predicate_partialgraph g1 (Complement _ (Union _ PV1 (eq root)))) ~=~ (predicate_partialgraph g2 (Complement _ (Union _ PV1 (eq root)))) /\ Same_set (marked g2) (Union _ marked' PV1).
proof: Proof. intros root ? ? ? g g4. intros. destruct_relation_list g1 g2 g3 in H3. pose proof triple_mark1 root g g1 g2 H4 H5 as PRE. cbv zeta in PRE. apply (triple_nothing _ g2 g3 root l nil l H H0 H1 eq_refl) in PRE; [| auto]. clear g1 g2 H4 H5 H6. revert g4 l_later H2 H3; rev_induction l_done; intros. + unfold componded_mark_list, relation_list in H3. simpl in H3. subst g3. auto. + clear PRE. rename l0 into l_done. rewrite <- app_assoc in H3; simpl in H3. unfold componded_mark_list in H4; rewrite map_app in H4; simpl in H4. apply (proj1 ((proj1 (same_relation_spec _ _) (relation_list_tail _ _)) _ _)) in H4. rename g3 into g1, g4 into g5. apply compond_relation_spec in H4; destruct H4 as [g2 [? ?]]. cbv zeta in H2. specialize (H2 g2 (x :: l_later) H3 H4). rename H2 into PRE; clear H4. unfold componded in H5. apply compond_relation_spec in H5. destruct H5 as [g4 [? ?]]. apply compond_relation_spec in H2. destruct H2 as [g3 [? ?]]. apply (triple_nothing _ g2 g3 root _ _ _ H H0 H1 H3) in PRE; [| auto]. apply (triple_nothing _ g4 g5 root l (l_done ++ x :: nil) l_later H H0 H1); [rewrite <- app_assoc; exact H3 | | auto]. split. - eapply triple1_mark; eauto. - eapply triple2_mark; eauto. 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