proposition: Lemma trc_ISMod : exists f', exists g', ISMod (E!) R f' g' /\ (exists k, g' 0 = g k) /\ (f' 0 = f 0 \/ R (f 0) (f' 0)).
proof: Proof. set (HexP := build_trs_proof). pose (reid := rec_ch_min _ HexP). pose (f0 := fun i => f (reid i)). pose (g0 := fun i => g (reid i)). assert (eq_fg0 : forall j, j < reid 0 -> (f j) = (g j)). intros j lt_j0. gen (is_min_ch _ (HexP 0)). intros Hproj. gen (Hproj j). intros HT. cut (E # (f j) (g j)). intros HT0. destruct (rtc_split HT0) as [| HT1]; auto. destruct (NatCompat.le_not_lt (HT (conj (@le_0_n j) HT1))). hyp. apply (proj1 (hyp1 j)). assert (eq_fgi : forall i j, S (reid i) <= j -> j < (reid (S i)) -> (f j) = (g j)). intros i j. simpl. intros le_Sij lt_jx. gen (is_min_ch _ (HexP (S (reid i)))). intros Hproj. gen (Hproj j). intros HT. cut (E # (f j) (g j)). intros HT0. destruct (rtc_split HT0) as [| HT1]; auto. destruct (NatCompat.le_not_lt (HT (conj le_Sij HT1))). hyp. apply (proj1 (hyp1 j)). assert (HEfg : forall i, (E !) (f (reid i)) (g (reid i))). intro i. induction i. 2: { destruct (rec_ch_minP _ HexP i); hyp. } destruct (ch_minP _ (HexP 0)); hyp. assert (HRfg : forall i j k, (reid i) <= j -> j < k -> k <= reid (S i) -> R (g j) (f k)). intros i j k le_ij lt_jk le_ki. induction k. destruct (Nat.nlt_0_r lt_jk). destruct (NatCompat.le_lt_or_eq (NatCompat.lt_n_Sm_le lt_jk)) as [HT | HT]. 2: { rewrite HT. apply (proj2 (hyp1 k)). } apply (@TrsR _ (f k)). apply IHk; try lia. rewrite (eq_fgi i k); try lia. apply (proj2 (hyp1 k)). assert (HRfg0 : forall j k, j < k -> k <= reid 0 -> R (g j) (f k)). intros j k lt_jk le_k0. induction k. destruct (Nat.nlt_0_r lt_jk). destruct (NatCompat.le_lt_or_eq (NatCompat.lt_n_Sm_le lt_jk)) as [HT | HT]. 2: { rewrite HT. apply (proj2 (hyp1 k)). } apply (@TrsR _ (f k)). apply IHk; try lia. rewrite (eq_fg0 k); try lia. apply (proj2 (hyp1 k)). exists f0; exists g0. split. intro i. simpl. unfold f0, g0. split. apply HEfg. apply (HRfg i); auto. destruct (rec_ch_minP _ HexP i) as [HT _]. apply (@Nat.lt_le_trans (reid i) (S (reid i)) (reid (S i))); auto. split. exists (reid 0). simpl. auto. unfold f0. case_eq (reid 0); intros. left; refl. right. rewrite eq_fg0; try lia. apply HRfg0; lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)