I’m trying to prove the following reduction

t{x:=u}{y:=v} = t{y:=v}{x:=u{y:=v}}

We have the following Assuming:

(1)($x neq y$ )

(2)x is not a free Variable of v (i.e $x notin $fv$(v)$ðŸ™‚

My idea is to do it by induction, but I’m a bit stuck with the base case. I would appreciate if someone can explain to me how to such a proof. I’m including what I tried (but it’s wrong/incomplete)

```
*Base case*: Assuming t is a just a variable `m` (t=m),
#on the left side we have
if m = x ==> u{y:=v} (if u=y then `v` else `u`)
else ==> m{y:=v} (if m=y then `v` else `m`)
#On the right side
if m=y ==> v{x:=u{y:=v}} (if u=y then `v{x:=v}` else `u{x:=u}` ( so we get either (v=x==> `v` else `v`) or else u=x==> `u` or else `u`) )
else ==> m{x:=u{y:=v}} (if m=y then `m{x:=v}` else `m{x:=u}`( so we get either v or m))
```

I understand we end up getting the same four branches, but is that considered really a proof? Is this the proper way to write such proof and conclude for the base case? Also the given assumptions didn’t help much here so I think I’m missing the part where I need to use those assumptions…

I think once the base case is proven,

we can do the following

case t = ($t_{1}$$t_{2}$)

```
t{x:=u}{y:=v} ==> t1t2{x:=u}{y:=v}
==> t1{x:=u}{y:=v} t2{x:=u}{y:=v} and we have just proven in the base case that:
t1{x:=u}{y:=v} = t1{y:=v}{x:=u{y:=v}} and t2{x:=u}{y:=v} = t2{y:=v}{x:=u{y:=v}}
so t1{x:=u}{y:=v} t2{x:=u}{y:=v} = t1{y:=v}{x:=u{y:=v}} t2{y:=v}{x:=u{y:=v}}
= t1t2{x:=u}{y:=v} = t1t2{y:=v}{x:=u{y:=v}}
```

Now only part left is if $t= lambda m . t$

so we have $(lambda m . t)${x:=u}{y:=v}

this can be directly re-written as $lambda m . t${x:=u}{y:=v}, which is the base case again…

Could someone please help ne finish this proof correctly and explain to me the right way to do it?

Thanks in advance