proposition: Lemma Tle_monotone_afs : Trel_monotone Tle_afs.
proof: Proof. intros f l1 l2 H. unfold Tle_afs; unfold afs; simpl; destruct (afs_symb f) as [g|i|g ns]; simpl. apply Tle_mono; induction H; [ left | right ]; assumption. generalize (Nat.le_gt_cases (length l1) i); intros [Hi|Hi]. rewrite nth_overflow; [| rewrite map_length; assumption ]; rewrite nth_overflow; [| rewrite map_length; apply one_step_list_length_eq in H; rewrite <- H; assumption ]. apply Tle_refl. revert i Hi; induction H; destruct i; simpl; intros; [ assumption | apply Tle_refl | apply Tle_refl | apply IHone_step_list; apply (proj2 (Nat.succ_lt_mono _ _) Hi) ]. cut (refl_trans_clos (one_step_list Tle) (afs_filt (map afs l1) ns) (afs_filt (map afs l2) ns)); [ unfold afs; intros [Hr|x y Htc]; [ apply Tle_refl |]; induction Htc; [| apply Tle_trans with (M.Term g y); [| assumption ]]; apply Tle_mono; assumption |]. revert l1 l2 H; induction ns; intros; [ constructor |]. cut ( (nth_error (map afs l1) a = None /\ nth_error (map afs l2) a = None) \/ (exists t1, exists t2, nth_error (map afs l1) a = Some t1 /\ nth_error (map afs l2) a = Some t2 /\ Tle t1 t2)); [ intros [[H0 H1]|[t1 [t2 [H0 [H1 H2]]]]]; simpl; rewrite H0; rewrite H1; [ exact (IHns _ _ H) | right ]; right with (t2 :: afs_filt (map afs l1) ns); [ left; assumption |]; apply IHns in H; destruct H; [ left; left; apply Tle_refl | induction H; [ left; right; assumption |]; right with (t2::y); [ right |]; assumption ] |]. revert l1 l2 H; induction a. intros; inversion H; subst; right; [ exists (afs t1); exists (afs t2) | exists (afs t); exists (afs t) ]; split; try reflexivity; split; try reflexivity; [ assumption | apply Tle_refl ]. intros; inversion H; subst; simpl; [| exact (IHa _ _ H0) ]; destruct (nth_error (map afs l) a); [ right; exists t; exists t; split; try reflexivity; split; try reflexivity; apply Tle_refl | left; split; reflexivity ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)