proposition: Lemma parametrized_confluence (R : X -> X -> Prop) (m n : nat) (s t1 t2 : X) : uniform_confluent R -> pow R m s t1 -> pow R n s t2 -> exists k l u, k <= n /\ l <= m /\ pow R k t1 u /\ pow R l t2 u /\ m + k = n + l.
proof: Proof. revert n s t1 t2; induction m; intros n s t1 t2 unifConR s_to_t1 s_to_t2. - unfold pow in s_to_t1. simpl in s_to_t1. subst s. exists n, 0, t2. repeat split; try now lia. eassumption. - unfold pow in s_to_t1. simpl in *. destruct s_to_t1 as [v [s_to_v v_to_t1]]. destruct (parametrized_semi_confluence unifConR s_to_t2 s_to_v) as [k [l [u [k_lt_1 [l_lt_n [t2_to_u [v_to_u H]]]]]]]. destruct (IHm _ _ _ _ unifConR v_to_t1 v_to_u) as [l'[k'[u'[l'_lt_l [k'_lt_m [t1_to_u' [u_to_u' H2]]]]]]]. exists l', (k + k'), u'. repeat split; try lia. eassumption. rewrite pow_add. econstructor; split; eassumption. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith