proposition: Lemma triple_loop: forall (g g1 g3: Graph) (g1' g3': Graph') (M: V -> Prop) root es es_done e0 es_later, let PV := reachable_by g root (Complement _ M) in let PE := Intersection E (weak_edge_prop PV g) (evalid g) in vvalid g root -> ~ M root -> let M0 := Union _ M (eq root) in (forall e, In e es <-> out_edges g root e) -> NoDup es -> es = es_done ++ e0 :: es_later -> (forall v, M v \/ ~ M v) -> let PV1 := reachable_by_through_set g (map (dst g) es_done) (Complement _ M0) in let PE1 := Intersection _ (weak_edge_prop PV1 g) (evalid g) in let PE1_root e := In e es_done in guarded_bij (Union _ PV1 (eq root)) (Union _ PE1 PE1_root) (vmap g1) (emap g1) g1 g1' /\ g ~=~ g1 /\ (forall e, Union _ PE1 PE1_root e -> Complement _ (Union _ PV1 (eq root)) (dst g1 e) -> vvalid g (dst g1 e) -> vmap g1 (dst g1 e) = dst g1' (emap g1 e)) /\ guarded_pointwise_relation (Complement V PV) eq (vmap g) (vmap g1) /\ guarded_pointwise_relation (Complement E PE) eq (emap g) (emap g1) /\ Same_set (vvalid g1') (image_set (Union _ PV1 (eq root)) (vmap g1)) /\ Same_set (evalid g1') (image_set (Union _ PE1 PE1_root) (emap g1)) -> let M_rec := Union _ M0 PV1 in let PV0 := reachable_by g (dst g e0) (Complement _ M_rec) in let PE0 := Intersection _ (weak_edge_prop PV0 g) (evalid g) in edge_copy g root M (es_done, e0) (g1, g1') (g3, g3') -> let PV3 := reachable_by_through_set g (map (dst g) (es_done ++ e0 :: nil)) (Complement _ M0) in let PE3 := Intersection _ (weak_edge_prop PV3 g) (evalid g) in let PE3_root e := In e (es_done ++ e0 :: nil) in guarded_bij (Union _ PV3 (eq root)) (Union _ PE3 PE3_root) (vmap g3) (emap g3) g3 g3' /\ g ~=~ g3 /\ (forall e, Union _ PE3 PE3_root e -> Complement _ (Union _ PV3 (eq root)) (dst g3 e) -> vvalid g (dst g3 e) -> vmap g3 (dst g3 e) = dst g3' (emap g3 e)) /\ guarded_pointwise_relation (Complement V PV) eq (vmap g) (vmap g3) /\ guarded_pointwise_relation (Complement E PE) eq (emap g) (emap g3) /\ Same_set (vvalid g3') (image_set (Union _ PV3 (eq root)) (vmap g3)) /\ Same_set (evalid g3') (image_set (Union _ PE3 PE3_root) (emap g3)).
proof: Proof. intros. unfold edge_copy in H6. destruct_relation_list p in H6; destruct p as [g2 g2']. rename H7 into COPY. rename H6 into ECOPY. assert (guarded_bij (Union _ PV3 (eq root)) (Union _ PE3 PE1_root) (vmap g2) (emap g2) g2 g2' /\ g ~=~ g2 /\ (forall e, Union _ PE3 PE1_root e -> Complement _ (Union _ PV3 (eq root)) (dst g2 e) -> vvalid g (dst g2 e) -> vmap g2 (dst g2 e) = dst g2' (emap g2 e)) /\ guarded_pointwise_relation (Complement V PV) eq (vmap g) (vmap g2) /\ guarded_pointwise_relation (Complement E PE) eq (emap g) (emap g2) /\ Same_set (vvalid g2') (image_set (Union _ PV3 (eq root)) (vmap g2)) /\ Same_set (evalid g2') (image_set (Union _ PE3 PE1_root) (emap g2))) as PRE; [clear g3 g3' ECOPY; rename H5 into PRE | clear COPY H5]. + split; [| split; [| split; [| split; [| split]]]]. - eapply triple1_copy; eauto. tauto. - eapply triple2_copy; eauto. tauto. - eapply triple3_copy; eauto. tauto. - eapply triple4_copy; eauto. tauto. - eapply triple5_copy; eauto. tauto. - eapply triple6_copy; eauto. tauto. + split; [| split; [| split; [| split; [| split]]]]. - eapply triple1_ecopy1; eauto. tauto. - eapply triple2_ecopy1; eauto. tauto. - eapply triple3_ecopy1; eauto. tauto. - eapply triple4_ecopy1; eauto. tauto. - eapply triple5_ecopy1; eauto. tauto. - eapply triple6_ecopy1; eauto. tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism