Confluence proof for a simple rewriting system

Assume we have a simple language that consists of the terms:

• $\mathtt{true}$

• $\mathtt{false}$

• if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$

Now assume the following logical evaluation rules:

$$ \begin{gather*}
\dfrac{}
{\mathtt{if}\: \mathtt{true} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_2}
\text{[E-IfTrue]} \quad
\dfrac{}
{\mathtt{if}\: \mathtt{false} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_3}
\text{[E-IfFalse]} \\
\dfrac{t_1 \to t_1'}
{\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1' \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3}
\text{[E-If]} \\
\end{gather*} $$

Suppose we also add the following funky rule:

$$
\dfrac{t_2 \to t_2'}
{\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1 \:\mathtt{then}\: t_2' \:\mathtt{else}\: t_3}
\text{[E-IfFunny]}
$$

For this simple language with the given evaluation rules I wish to prove the following:

Theorem: If $r \rightarrow s$ and $r \rightarrow t$ then there is some term $u$ such that $s \rightarrow u$ and $t \rightarrow u$.

I am proving this by induction on the structure of $r$. Here is my proof so far, it all worked out well, but I am stuck at the very last case. It seems like induction on the structure of $r$ is not sufficing, can anyone help me out?

Proof. By induction on $r$, we will seperate all the forms that $r$ can take:

• $r$ is a constante, nothing to prove since a normal form does not evaluate to anything.

• $r=$ if true then $r_2$ else $r_3$. (a) both derivations were done with the E-IfTrue rule. In this case $s=t$, so there is nothing to prove. (b) one deriviation was done with the E-IfTrue rule, the other with the E-Funny rule. Assume $r \rightarrow s$ was done with E-IfTrue, the other case is equivalently proven. We now know that $s = r_2$. We also know that $t =$ if true then $r'_2$ else $

Okay, so let's consider the case that $r = \mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$, $s$ has been derived by applying the E-If rule and $t$ has been derived by applying the E-Funny rule: So $s = \mathtt{if}\: t'_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ where $t_1 \rightarrow t'_1$ and $t = \mathtt{if}\: t_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ where $t_2 \rightarrow t'_2$.

The $u$ we're looking for is $u = \mathtt{if}\: t'_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$. $s \rightarrow u$ follows from rule E-Funny and $t \rightarrow u$ follows from rule E-If.

StackExchange Computer Science Q#1060, answer score: 8