proposition: Lemma acc_union_rest_alt_weak : forall A (R1 R2 : relation A) (P : A -> Prop), (forall (a b : A), P a -> R1 b a -> P b) -> (forall (a b : A), P a -> R2 b a -> P b) -> forall a, (forall b, refl_trans_clos (compose_rel R2 (refl_trans_clos R1)) b a -> Acc R1 b) -> (forall b, refl_trans_clos R1 b a -> Acc (compose_rel (refl_trans_clos R1) R2) b) -> P a -> Acc (union _ R1 R2) a.
proof: Proof. intros A R1 R2 P Inv1 Inv2 a H1a H2a Pa. assert (H : Acc (union _ (rest P R1) (rest P R2)) a). apply acc_union_alt_weak. intros b H; apply Acc_incl with R1. clear; intros a1 a2 [H _]; assumption. apply H1a. apply refl_trans_incl with (compose_rel (rest P R2) (refl_trans_clos (rest P R1))); trivial. clear; intros a1 a2 H; inversion H as [c1 a c2 H1 H2]; subst. apply Comp with a. inversion H1; trivial. apply refl_trans_incl with (rest P R1); [idtac | assumption]. clear; intros a1 a2 [H _]; assumption. intros b H; apply Acc_incl with (compose_rel (refl_trans_clos R1) R2). clear; intros a1 a2 H; inversion H as [c1 a c2 H1 [H2 _]]; subst. apply Comp with a; [idtac | assumption]. apply refl_trans_incl with (rest P R1); [idtac | assumption]. clear; intros a1 a2 [H _]; assumption. apply H2a. apply refl_trans_incl with (rest P R1); [idtac | assumption]. clear; intros a1 a2 [H _]; assumption. clear H1a H2a; revert Pa; induction H as [a Acc_a IH]. intro Pa; apply Acc_intro; intros a1 [H1 | H2]; apply IH. left; repeat split; trivial. apply Inv1 with a; assumption. apply Inv1 with a; assumption. right; repeat split; trivial. apply Inv2 with a; assumption. apply Inv2 with a; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)