proposition: Lemma rewrite_decomposed_term : forall t s sigma, t = apply_subst sigma s -> well_formed s -> (forall x u, In (x,u) sigma -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) -> (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) -> (forall x y u, In (x,u) sigma -> In (y,u) sigma -> x = y) -> (forall x, In x (var_list s) -> In x (map (@fst _ _) sigma)) -> forall u, one_step R u t -> ((exists s', one_step R s' s /\ u = apply_subst sigma s') \/ (exists p, exists x, exists u', subterm_at_pos s p = Some (Var x) /\ one_step R u' (apply_subst sigma (Var x)) /\ u = replace_at_pos t u' p)).
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v s sigma h0 Ws h1 h2 h3 h4 u H'. inversion H' as [t1' t2' H1 | ]; clear H'; subst. inversion H1 as [r l phi H2 H3 H4]; clear H1; subst. destruct l as [x | ]; [apply False_rect; apply (R_var _ _ H2) | discriminate]. intros f lt Hlt s sigma h0 Ws h1 h2 h3 h4 u H'. inversion H' as [t1' t2' H1 | f' l1 l2' H1 H2]; clear H'; subst. inversion H1 as [r l phi H2 H3 H4]; clear H1; subst. destruct (decompose_subst s (subst_rest (var_list s) sigma) l phi Ws) as [phi' [K1 [K2 [K3 K4]]]]. intros x u xu_in_rest_sig; apply (h1 x u); apply subst_rest_subst with (var_list s); trivial. intros x u v xu_in_rest_sig xv_in_rest_sig; apply (h2 x u v); apply subst_rest_subst with (var_list s); trivial. intros x y u xu_in_rest_sig yu_in_rest_sig; apply (h3 x y u). apply subst_rest_subst with (var_list s); trivial. apply subst_rest_subst with (var_list s); trivial. intro x; split. intro x_in_s; assert (x_in_sig : In x (map (@fst _ _) sigma)). apply h4; assumption. rewrite in_map_iff in x_in_sig; destruct x_in_sig as [[x' u] [x_eq_x' x_in_sig]]; simpl in x_eq_x'; subst x'. rewrite in_map_iff; exists (x,u); split; trivial. apply subst_rest_subst_rest; trivial. intro x_in_rest_sig; rewrite in_map_iff in x_in_rest_sig; destruct x_in_rest_sig as [[x' u] [x_eq_x' x_in_rest_sig]]; simpl in x_eq_x'; subst x'. apply subst_rest_rest with sigma u; trivial. apply (proj2 (WR _ _ H2)). rewrite H4; rewrite h0. rewrite <- subst_eq_vars; intros v v_in_s; rewrite subst_rest_ok; trivial. left; exists (apply_subst phi' r); split. rewrite <- K2; apply at_top; apply instance; trivial. rewrite <- subst_comp_is_subst_comp; rewrite <- subst_eq_vars; intros v v_in_r. assert (v_in_l : In v (var_list l)). apply (R_reg _ _ H2); trivial. apply sym_eq; rewrite <- K1; trivial. do 2 rewrite subst_comp_is_subst_comp. rewrite <- subst_eq_vars; intros z z_in_v_phi'. rewrite subst_rest_ok; trivial. rewrite <- K2. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ v_in_l)) as [p Sub]. apply var_in_subterm with (apply_subst phi' (Var v)) p; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos l p phi'). rewrite Sub; trivial. destruct s as [x | g ls]. right; exists nil; exists x; exists (Term f l1). split; trivial. split; trivial. rewrite <- h0; apply in_context; trivial. destruct (one_step_in_list H1) as [ti [ui [lt1 [lt2 [K [K1 K2]]]]]]. simpl in h0; injection h0; clear h0; intro h0; intro; subst g. rewrite K1 in h0. destruct (split_map_set _ _ _ _ (sym_eq h0)) as [ls1 [ls2 [J1 [J2 J3]]]]. destruct ls2 as [ | si ls2]. discriminate. simpl in J3; injection J3; clear J3; intros J3 j3. destruct Hlt with ti si sigma ui as [[si' [L1 L2]] | [p [x [ui' [Sub [L1 L2]]]]]]; trivial. rewrite K1; apply in_or_app; right; left; reflexivity. apply sym_eq; assumption. apply (proj1 (well_formed_unfold Ws)); rewrite J1; apply in_or_app; right; left; reflexivity. intros x x_in_si; apply h4; rewrite J1; simpl; rewrite var_list_list_app; apply in_or_app; right; apply in_or_app; left; assumption. left; exists (Term f (ls1 ++ si' :: ls2)); split. apply in_context; rewrite J1. revert L1; clear; induction ls1 as [ | s1 ls1]. intro; apply head_step; trivial. intro; apply tail_step; apply IHls1; trivial. simpl; apply f_equal; rewrite map_app; rewrite K2; apply sym_eq; apply f_equal2; trivial. simpl; apply f_equal2; trivial. apply sym_eq; trivial. right; exists ((length ls1) :: p); exists x; exists ui'; split. rewrite J1; simpl; rewrite nth_error_at_pos; rewrite Sub; trivial. split; trivial. rewrite K1; rewrite K2; replace (length ls1) with (length lt1). simpl; apply f_equal; revert L2; clear. induction lt1 as [ | t1 lt1]; simpl. intro; apply (f_equal (fun u => u :: lt2)); assumption. intro; apply f_equal; apply IHlt1; assumption. rewrite <- J2; rewrite length_map; reflexivity. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)