proposition: Lemma symb_sup_gen_list : forall R1 Rlist1 R2 Rlist2, (forall l r, R1 r l <-> In (l,r) Rlist1) -> (forall l r, R2 r l <-> In (l,r) Rlist2) -> {Slist | forall f g, symb_sup_gen R1 R2 f g <-> In (f,g) Slist}.
proof: Proof. intros R1 Rlist1; revert R1. induction Rlist1 as [ | [l r] Rlist1]; intros R1 R2 Rlist2 Rlist_ok1 Rlist_ok2. exists nil; intros f g; split; intro H. destruct H as [r [l [[H _] _]]]; rewrite Rlist_ok1 in H; contradiction. contradiction. set (R' := fun b a => R1 b a /\ In (a,b) Rlist1). assert (Rlist_ok' : forall a b, R' b a <-> In (a,b) Rlist1). intros a b; split; intro H. destruct H as [_ H]; assumption. split; [rewrite Rlist_ok1; right | ]; assumption. destruct (IHRlist1 R' R2 Rlist2 Rlist_ok' Rlist_ok2) as [Slist Slist_ok]. destruct l as [x | f l]. exists Slist; intros f g; split. intros [u [v [[H1 H2] [H3 H4]]]]. rewrite Rlist_ok1 in H1; simpl in H1; destruct H1 as [H1 | H1]. injection H1; intros; subst; contradiction H2. rewrite <- Slist_ok; exists u; exists v; split; split. rewrite Rlist_ok'; assumption. assumption. assumption. destruct H4 as [g l t H4]; constructor 1 with l t. assumption. intro H; rewrite <- Slist_ok in H; destruct H as [u [v [[H1 H2] [H3 H4]]]]. exists u; exists v; split; split. rewrite Rlist_ok1; right; rewrite <- Rlist_ok'; assumption. assumption. assumption. destruct H4 as [g l t H4]; constructor 1 with l t. assumption. exists ((map (fun g => (f,g)) (filter (fun g => if defined_dec _ _ Rlist_ok2 g then true else false) (symb_list r))) ++ Slist). intros g g'; split; intro H. destruct H as [u [v [H1 [H2 H3]]]]. destruct H1 as [H H1]. rewrite Rlist_ok1 in H; simpl in H; destruct H as [H | H]. injection H; clear H; intros; subst; subst. apply in_or_app; left; rewrite in_map_iff; exists g'; split; [apply eq_refl | ]. rewrite filter_In; split. rewrite symb_list_ok; assumption. destruct (defined_dec R2 Rlist2 Rlist_ok2 g') as [Dg' | NDg']. apply eq_refl. apply False_rect; apply NDg'; assumption. apply in_or_app; right; rewrite <- Slist_ok. exists u; exists v; split; split. rewrite Rlist_ok'; assumption. assumption. assumption. assumption. destruct (in_app_or _ _ _ H) as [H1 | H2]; clear H. rewrite in_map_iff in H1; destruct H1 as [g'' [H1 H2]]. injection H1; clear H1; intros; subst. rewrite filter_In in H2; destruct H2 as [g'_in_r H2]. destruct (defined_dec R2 Rlist2 Rlist_ok2 g') as [Dg' | NDg']; [ clear H2 | discriminate H2]. exists r; exists (Term g l); split; split. rewrite Rlist_ok1; left; apply eq_refl. apply eq_refl. rewrite <- symb_list_ok; assumption. assumption. rewrite <- Slist_ok in H2; destruct H2 as [u [v [[H1 H2] [H3 H4]]]]. exists u; exists v; split; split. rewrite Rlist_ok1; right; rewrite <- Rlist_ok'; assumption. assumption. assumption. assumption. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)