 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2013/digital-systems-linear-algebra-introduction-to-formal-proof/8/b/ii/solution

Use reflexivity to obtain

T_{1} = T_{1}

ϕ (z)

to be

z = T_{1}

, and replace the designated first occurrence of

T_{1}

using the premise

T_{1} = T_{2}

Symmetry from reflexivity and replacement

Line	Open assumptions	Formula	Justification
1	1	$T_{1} = T_{2}$	Premise
2	1	$T_{1} = T_{1}$	equality introduction rule
3	1	$T_{2} = T_{1}$	equality elimination rule 1, 2

Therefore

T_{2} = T_{1} .

The second occurrence of

T_{1}

T_{1} = T_{1}

is part of the fixed parameter in

ϕ (z)

and is not replaced.

 New to topics? Read the docs here!