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 / 7 / b / ii

Use conjunction elimination to extract the three inputs, then apply the implication elimination rule three times:

12345678910 E \to (F \to (G \to H)) ∣ (E \land F) \land G ∣ E \land F ∣ G ∣ E ∣ F ∣ F \to (G \to H) ∣ G \to H ∣ H ((E \land F) \land G) \to H premise assumption \land -elim-L 2 \land -elim-R 2 \land -elim-L 3 \land -elim-R 3 \to -elim 1, 5 \to -elim 7, 6 \to -elim 8, 4 \to -intro 2 - 9

E \to F \to G \to H ⊢ ((E \land F) \land G) \to H .

 Ancestors (12)

There are no discussions about this article yet.

There are currently no matching articles.