 Solution

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

t_{1} = t_{1}

ϕ (z)

to be

z = t_{1}

. Substituting

t_{2}

for

t_{1}

Line	Context	Formula	Justification
1	${1}$	$t_{1} = t_{2}$	Premise
2	${1}$	$t_{1} = t_{1}$	equality introduction rule $= -intro$
3	${1}$	$t_{2} = t_{1}$	equality elimination rule $= -elim$ on 1, 2

Thus

t_{1} = t_{2} ⊢ t_{2} = t_{1}

. This uses only the two supplied equality rules; symmetry has not been assumed as an additional rule.

 New to topics? Read the docs here!