Download RODIN Deliverable D30

Figure 3: The proof at step 15
easier. The first part also should not be too hard, if you instantiate the hypothesis with
the quantifier as early as possible.
5.3 Exercise: Theorem 3
Theorem 3 is very similar to Theorem 2. Proving also works in a very similar fashion,
except that it takes a few steps more, as we do not have any axioms on (f ; t). Then,
Theorem 1 usually is useful.
5.4 Exercise: Theorem 4
Theorem 4 states that ∀b · f [b] ⊆ b ⇒ t[b] ⊆ b. Once again, you will need the right
instantiation of a hypothesis to succeed with the proof at some stage. Here, ((N \
b) × N ) ∪ (b × b) will be a good instantiation. This proof is quite lengthy, as there
are many proofs by cases that you will need to perform. A lot of the cases can be
solved by successfully adding the negation of a selected hypothesis and thus creating a
contradiction.
13