proposition: Lemma rpo_lt_dec : rel_dec lt.
proof: Proof. intros p q. gen p. clear p. pattern q. apply term_rect_forall with Sig term_eq_dec. right. intro F. apply var_are_min with x p. hyp. clear q. intros q v IH p. gen IH. clear IH. pattern p. apply term_rect_forall with Sig term_eq_dec; clear p. intros x IH. destruct (rpo_lt_subterm_dec (Var x) v). hyp. left. apply lt_subterm. destruct s as [a [av ax]]. exists a. unfold ge in ax. split_all. right. intro H. lt_inversion H; try discr. apply n. exists t'. replace v with ts. unfold ge. split_all. congruence. intros f vf IH IH'. destruct (rpo_lt_subterm_dec (Fun f vf) v). hyp. left. apply lt_subterm. destruct s as [a [av ax]]. exists a. unfold ge in ax. split_all. assert (all_lt_dec : { forall t, In t vf -> lt t (Fun q v) } + { exists t, In t vf /\ ~lt t (Fun q v) }). destruct (list_dec_all (fun vs => lt vs (Fun q v)) vf); try solve [split_all]. intros. apply IH. apply Inb_intro. hyp. hyp. assert (lt_roots_dec : {lt (Fun f vf) (Fun q v)} + {~(f <F q) \/ exists t, In t vf /\ ~lt t (Fun q v)}). destruct (ltF_dec f q); try solve [split_all]. destruct all_lt_dec; split_all. left. apply lt_roots; hyp. destruct lt_roots_dec. split_all. assert (lt_status_dec : {lt (Fun f vf) (Fun q v)} + {~f =F= q \/ ~tau q lt vf v \/ exists t, In t vf /\ ~lt t (Fun q v)}). destruct (eqF_dec f q); try solve [split_all]. destruct (tau_dec q lt vf v); try solve [split_all]. intros. apply (IH' s). apply Inb_intro. hyp. destruct all_lt_dec; try solve [split_all]. left. apply lt_status; try solve [split_all]. apply eqF_sym. hyp. destruct lt_status_dec. split_all. right. intro ord. lt_inversion ord. destruct o as [f_q | [t [t_vf t_qv]]]. apply f_q. congruence. apply t_qv. replace q with g; replace v with ts; try solve [congruence]. apply Hsub. congruence. destruct o0 as [f_q | [tau_vfv | [t [t_vf t_qv]]]]. apply f_q. congruence. apply tau_vfv. rewrite (status_eq q f0). congruence. apply eqF_sym. congruence. apply t_qv. replace q with g; replace v with ts; try solve [congruence]. apply Hsub. congruence. apply n. exists t'. split. congruence. unfold ge. split_all. Defined.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)