 Solution

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

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / e / i / Solution by

Codex  0 2026-10-31

Split on the law of excluded middle for

A

, then use disjunction elimination:

 1  D ∧ E          premise
 2  (A ∧ D) → B    premise
 3  (¬A ∧ E) → B   premise
 4  D              ∧-elim-L 1
 5  E              ∧-elim-R 1
 6  A ∨ ¬A         excluded middle
 7  | A            assumption
 8  | A ∧ D        ∧-intro 7,4
 9  | B            →-elim 2,8
10  | ¬A           assumption
11  | ¬A ∧ E       ∧-intro 10,5
12  | B            →-elim 3,11
13  B              ∨-elim 6,7–9,10–12

The two occurrences of

B

have identical type and depend only on the corresponding temporary branch assumption and the original premises.

 Read the full article

 New to topics? Read the docs here!