proposition: Lemma rpo_add_context : forall bb p ctx s t, rpo bb s t -> is_a_pos ctx p = true -> rpo bb (replace_at_pos ctx s p) (replace_at_pos ctx t p).
proof: Proof. intros bb p; induction p as [ | i p ]; intros ctx s t R H; trivial; destruct ctx as [ v | f l ]. discriminate. assert (Status : forall g, g = f -> status Prec g = status Prec f). intros; subst; trivial. do 2 (rewrite replace_at_pos_unfold); destruct (status Prec f); generalize (Status f (eq_refl _)); clear Status; intro Status. apply Top_eq_lex; trivial. apply prec_eq_refl. left; clear; revert l; induction i as [ | i]; intros [ | a l]; simpl; trivial. rewrite IHi; apply eq_refl. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl. simpl in H; destruct i; discriminate. destruct i as [ | i]. apply List_gt; trivial. simpl in H; apply IHp; trivial. apply List_eq. reflexivity. apply IHl; trivial. intros s' s'_mem_ls; assert (H' : exists s'', rpo_eq bb s' s'' /\ mem equiv s'' (replace_at_pos_list l t i p)). generalize i H s' s'_mem_ls; clear i H s' s'_mem_ls; induction l as [ | u l]; intros i H; simpl. intros; contradiction. destruct i as [ | i]. intros s' [s'_eq_s'' | s'_mem_l]. exists (replace_at_pos u t p); split. apply Lt; rewrite (equiv_rpo_equiv_2 _ s'_eq_s''). apply IHp; trivial. left; reflexivity. exists s'; split. apply Equiv; apply Eq. right; trivial. intros s' [s'_eq_u | s'_mem_l]. exists u; split. apply Equiv; trivial. left; reflexivity. simpl in IHl; simpl in H. destruct (IHl i H s' s'_mem_l) as [s'' [s'_le_s'' s''_mem_l']]. exists s''; split; trivial. right; trivial. destruct H' as [s'' [s'_le_s'' s''_mem_l']]. apply Subterm with s''; trivial. apply Top_eq_mul; trivial. apply prec_eq_refl. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl. simpl in H; destruct i; discriminate. destruct i as [ | i]. apply (@List_mul bb (replace_at_pos u t p) nil (replace_at_pos u s p :: nil) l); reflexivity || auto. intros b [b_eq_s' | b_mem_nil]. exists (replace_at_pos u t p); split. left; reflexivity. rewrite (equiv_rpo_equiv_2 _ b_eq_s'). apply IHp; trivial. contradiction. simpl in IHl; simpl in H; assert (H' := IHl i H). inversion H' as [a lg ls lc l' l'' ls_lt_alg P1 P2]; subst. apply (@List_mul bb a lg ls (u :: lc)); trivial. rewrite <- permut0_cons_inside; trivial; try reflexivity. apply equiv_equiv. rewrite app_comm_cons. rewrite <- permut0_cons_inside; trivial; try reflexivity. apply equiv_equiv. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)