proposition: Lemma parametrized_semi_confluence (R : X -> X -> Prop) (m : nat) (s t1 t2 : X) : uniform_confluent R -> pow R m s t1 -> R s t2 -> exists k l u, k <= 1 /\ l <= m /\ pow R k t1 u /\ pow R l t2 u /\ m + k = S l.
proof: Proof. intros unifConfR; revert s t1 t2; induction m; intros s t1 t2 s_to_t1 s_to_t2. - unfold pow in s_to_t1. simpl in *. subst s. exists 1, 0, t2. repeat split; try lia. econstructor. split; try eassumption; econstructor. - destruct s_to_t1 as [v [s_to_v v_to_t1]]. destruct (unifConfR _ _ _ s_to_v s_to_t2) as [H | [u [v_to_u t2_to_u]]]. + subst v. eexists 0, m, t1; repeat split; try lia; eassumption. + destruct (IHm _ _ _ v_to_t1 v_to_u) as [k [l [u' H]]]. eexists k, (S l), u'; repeat split; try lia; try tauto. econstructor. split. eassumption. tauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith