[CST-2] Types: y2000p9q13

[George van den Driessche]

----- Original Message -----
From: "David Singleton" <dps29@hermes.cam.ac.uk>
To: <cst-2@srcf.ucam.org>
Sent: Sunday, June 02, 2002 11:44 AM
Subject: [CST-2] Types: y2000p9q13


>
> Has anyone done this question, and could they tell me how to do the
> proof?
>
> I presume that we need to show that if phi holds of a judgement,
> phi still holds when the axiom and rules are applied.
>
> I think I've managed this for the axiom.
>
> How do we proceed - if by structural induction, on what?

Rule induction. Prove that phi holds for the axioms, and also that for each
rule, if it holds for the premises then it holds for the conclusion. You
need to cope with several different implications to get the rules to work,
because there's implication internal to phi, and also from premises to
conclusion. It gets a bit confusing.

Once you've done that, the rest falls into place.

George