# logic – how to prove equivalence of two substitutions by induction

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?