proposition: Lemma SPO_lt : forall u, (forall t s, lt u t -> lt t s -> lt u s) /\ (lt u u -> False).
proof: Proof. assert (leF_po : preorder Sig leF). apply leF_preorder. assert (ltF_trans : transitive ltF). apply (ltA_trans Sig leF); trivial. assert (eqF_trans : transitive eqF). elim (eqA_equivalence Sig leF); trivial. assert (ltF_irrefl : forall f, f <F f -> False). intros f Hf; apply (ltA_antisym Sig leF f f); trivial. intro u; induction u as [x | h us HInd1] using term_ind_forall2. split. intros t s H1 H2. lt_inversion H1; try inversion s_is; try inversion t_is. elim (term_eq_dec s (Var x)); intro case_s. subst s; elim (var_are_min H2). apply in_var; trivial. apply (@var_inclusion (Fun f ts) s); try right; subst; trivial. exists t'; split; trivial. elim Ht'; clear Ht'; intro Ht'; [subst; constructor | apply var_in; trivial]. apply var_are_min. split. intro t; induction t as [x | g ts HInd2] using term_ind_forall2. intros t H1; elim (var_are_min H1). intro s; induction s as [x | f ss HInd3] using term_ind_forall2. intros H1 H2; elim (var_are_min H2). intros H1 H2. lt_inversion H1; try inversion s_is; try inversion t_is; subst. lt_inversion H2; try inversion s_is0; try inversion t_is0; subst. apply lt_roots. apply ltF_trans with f1; trivial. intros u u_in_us. elim (HInd1 u u_in_us); clear HInd1; intros HInd1 HInd1'. apply (HInd1 (Fun f1 ss1) (Fun g ts)). apply (Hsub u u_in_us). hyp. apply lt_roots. apply (ltA_eqA_compat_r Sig leF) with f1; trivial; elim geq; split; trivial. intros u u_in_us. elim (HInd1 u u_in_us); clear HInd1; intros HInd1 HInd1'. apply (HInd1 (Fun f1 ss1)). apply (Hsub u u_in_us). hyp. gen (HInd3 t' t'_in_ts H1); intro HInd3'. apply (lt_subterm f1 ts (Fun f0 ss0)). exists t'. split; trivial. right. elim Ht'; clear Ht'; intro Ht'. subst t'; hyp. apply HInd3'; hyp. lt_inversion H2; try inversion s_is0; try inversion t_is0; subst. apply lt_roots. apply (ltA_eqA_compat_l Sig leF) with f1; trivial. elim eqFfg; split; trivial. intros u u_in_us. elim (HInd1 u u_in_us); clear HInd1; intros HInd1 HInd1'. apply (HInd1 (Fun f1 ss1)); trivial. apply (HInd1 (Fun f0 ss0)); trivial. apply lt_subterm; exists u; split; try left; trivial. apply lt_status; trivial. apply eqF_trans with f1; trivial. elim eqFfg0; split; trivial. elim eqFfg; split; trivial. intros u u_in_us; elim (HInd1 u u_in_us); clear HInd1; intros HInd1 HInd1'. apply (HInd1 (Fun f1 ss1)); trivial. apply Hsub; trivial. assert (Hs1 : tau f1 = tau g). apply status_eq; trivial. assert (Hs2 : tau f0 = tau f1). apply status_eq; trivial. rewrite <- Hs1. elim (SPO_to_status_SPO f1 lt ss0 HInd1); intros trans_to_status_trans H'. apply trans_to_status_trans with ss1; trivial. rewrite <- Hs2; trivial. gen (HInd3 t' t'_in_ts H1); intro HInd3'. apply (lt_subterm f1 ts (Fun f0 ss0)). exists t'. split; trivial. right. elim Ht'; clear Ht'; intro Ht'. subst t'; hyp. apply HInd3'; hyp. lt_inversion H2; try inversion s_is; try inversion t_is0; subst. elim Ht'; clear Ht'; intro Ht'. rewrite Ht'; apply (Hsub t' t'_in_ts). apply (HInd2 t' t'_in_ts (Fun g ts) Ht'). apply (Hsub t' t'_in_ts). elim Ht'; clear Ht'; intro Ht'. rewrite Ht'. apply Hsub; trivial. apply (HInd2 t' t'_in_ts (Fun g ts)); trivial. apply Hsub; trivial. apply lt_subterm. exists t'0. split; trivial. elim Ht'0; clear Ht'0; intro Ht'0. subst t'0; right; hyp. right; apply (HInd3 t'0 t'_in_ts0); trivial. intro H. lt_inversion H; try inversion t_is; subst; try inversion s_is; subst. apply (ltF_irrefl f); trivial. elim (SPO_to_status_SPO f lt ss HInd1); intros trans_to_status_trans irrefl_to_status_irrefl. apply (irrefl_to_status_irrefl); trivial. elim (HInd1 t' t'_in_ts); intros HInd1' HInd1''. elim Ht'; clear Ht'; intro Ht'. apply HInd1''; subst; trivial. apply HInd1''. apply HInd1' with (Fun f ts); trivial. apply immediate_subterm_property; trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)