Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2015/digital-systems-linear-algebra-introduction-to-formal-proof-resit/7/a/solution

The implication introduction rule opens a subproof under a temporary assumption , derives , then performs assumption discharge to conclude . The negation introduction rule instead derives logical falsity under a temporary assumption , discharges it, and concludes :
The rectangular boxes delimit these subproofs and the scope of their temporary assumptions. A line depending on the boxed temporary assumption cannot simply be used outside the box. The relevant introduction rule exports the indicated logical implication or negation; other surrounding assumptions stay in force.

New to topics? Read the docs here!