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&#39;}
      {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1&#39; \:\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&#39;}
      {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1 \:\mathtt{then}\: t_2&#39; \:\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&#39;_2$ else $r_3$ and that there exists some deriviation $r_2 \rightarrow r&#39;_2$ (the premise). If we now choose $u = r&#39;_2$, we conclude the case.
$r=$ if false then $r_2$ else $r_3$. Equivalently proven as above.
$r=$ if $r_1$ then $r_2$ else $r_3$ with $r_1 \neq $ true or false. (a) both deriviations were done with the E-If rule. We now know that $s =$ if $r&#39;_1$ then $r_2$ else $r_3$ and $t =$ if $r&#39;&#39;_1$ then $r_2$ else $r_3$. We also know that there exists deriviations $r_1 \rightarrow r&#39;_1$ and $r_1 \rightarrow r&#39;&#39;_1$ (the premises). We can now use the induction hypothese to say that there exists some term $r&#39;&#39;&#39;_1$ such that $r&#39;_1 \rightarrow r&#39;&#39;&#39;_1$ and $r&#39;&#39;_1 \rightarrow r&#39;&#39;&#39;_1$. We now conclude the case by saying $u =$ if $r&#39;&#39;&#39;_1$ then $r_2$ else $r_3$ and noticing that  $s \rightarrow u$ and $t \rightarrow u$ by the E-If rule. (b) one derivation was done by the E-If rule and one by the E-Funny rule.


This latter case, where one derivation was done by E-If and one by E-Funny is the case I am missing... I can't seem to be able to use the hypotheses.

Help will be much appreciated.
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&#39;_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ where $t_1 \rightarrow t&#39;_1$ and $t = \mathtt{if}\: t_1 \:\mathtt{then}\: t&#39;_2 \:\mathtt{else}\: t_3$ where $t_2 \rightarrow t&#39;_2$.

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