Cfrgtkky

I have to use natural deduction on the following 2 sequents:
$$t_1=t_2 vdash (t+t_1)=(t+t_2)$$
$$(x=0)lor ((x+x)>0)vdash (y=(x+x))to ((y>0)lor (y=0+x))$$

At first I thought that the first one is pretty easy, but I am stuck.
$$t_1=t_2 vdash (t+t_1)=(t+t_2)$$
$t_1=t_2 qquad qquad qquad qquad text{premise} \
(t+t_1)=(t+t_1)qquad qquad =_i \
(t+t_2)=(t+t_2) qquad qquad =_e 1,2 \ $

Now I am stuck at this point. I also tried to use $lor_e$ after $lor_i$, but I dont know how i can prove that.

The second one is a bit harder, but I have an idea.
$$(x=0)lor ((x+x)>0)vdash (y=(x+x))to ((y>0)lor (y=0+x))$$
$(x=0)lor ((x+x)>0) qquad qquad text{premise} \
\ ______________________________________ \ (y=(x+x)) qquad qquad qquad qquad text{assumption}$

The next step is the $lor_e$ , where i want to show that $(x=0)to y>0$ and $((x+x)> 0)to y>0)$. But that is impossible, since the first implication never holds.

Can somebody help me with my problem?

Thank you

For the first one :

1) $vdash t+t_2=t+t_2$ --- by $=$-intro

2) $t_1=t_2 vdash t_2=t_1$ --- from 1) by $(=text{symmetric})$ : $s=t vdash t=s$, derivable with $=$-intro and $=$-elim

3) $t_2=t_1, t+t_2=t+t_2 vdash t+t_1=t+t_2$ --- by $=$-elim : $s=t, ϕ[s/x] vdash ϕ[t/x]$, with $s,t$ terms substitutable for $x$ in $ϕ$, and $ϕ$ a formula : use $t+x=t+t_2$ as $ϕ$, $t_2$ as $s$ and $t_1$ as $t$.

4) $t_1=t_2 vdash t+t_1=t+t_2$ --- from 1), 2) and 3).

Note : the same derivation can be used for any term $r$; thus we can generalize it to the derived rule: $(=text{term})$ : $s=t vdash r[s/x]=r[t/x]$.

For the 2nd one, we can split it into two sub-derivations:

1) $x=0, y=x+x vdash y=0+x$ --- by $=$-elim, with $y=z+x$ as $ϕ$

2) $x=0, y=x+x vdash (y >0) lor (y=0+x)$ --- from 1) by $lor$-intro

3) $x=0 vdash (y=x+x) to ((y >0) lor (y=0+x))$ --- from 2) by $to$-intro.

In the same way, we can derive :

4) $(x+x)>0 ⊢ (y=x+x) → ((y>0) ∨ (y=0+x))$

and then conclude by $lor$-elim from : $(x=0) lor (x+x)>0$.

You write:

At first I thought that the first one is pretty easy, but I am stuck.
$$t_1=t_2 vdash (t+t_1)=(t+t_2)$$
$t_1=t_2 qquad qquad qquad qquad text{premise} \
(t+t_1)=(t+t_1)qquad qquad =_i \
(t+t_2)=(t+t_2) qquad qquad =_e 1,2 \ $

Actually, it's very easy: when doing $=_e$ using $t_1=t_2$, you do not have to replace all instances of $t_1$ with $t_2$: you can just replace some of them. So, if you just replace the second $t_1$ in $(t+t_1)=(t+t_1)$ with $t_2$, you end up with the desired conclusion:

$t_1=t_2 qquad qquad qquad qquad text{premise} \
(t+t_1)=(t+t_1)qquad qquad =_i \
(t+t_1)=(t+t_2) qquad qquad =_e 1,2 \ $