Induction Proofs

We want to show


n Even
----------
(S n) Odd'


This is really a property of all even numbers, and
so it is our induction principle for even numbers
that we want to use.


Even was characterised by:

-----  E_1
0 Even


n Even
--------------- E_2
(S (S n)) Even



Proof by induction of P(n): Even n ==> (S n) Odd'


Base case, corresponding to E_1:

Show P(0), i.e. (S 0) Odd', which follows immediately
from rule O'_1.



Inductive case, corresponding to E_2:

Assume IH: P(n) == (S n) Odd'.

Show P(S (S n)): (S (S (S n))) Odd'.



---------- IH
(S n) Odd'
------------------ O_2
(S (S (S n))) Odd'



That concludes our proof by induction of n Even ==> P(n).

Proving M is the same language as L has two components:

s M       s L
---  and  ---
s L       s M



Let's look at the right hand side of those two problems first.


Clearly we need to proceed by rule induction on the
rules that characterise L. The problem is, the L_J
rule establishes s_1 s_2 J and all we know about s_1
is that s_1 N. We wouldn't have an IH about s_q if we
induct on the rules that characterise J.

That might be fine if we'd already proven what we need
about N, but we can't do that without thinking about L.


Solution: Simultaneous Induction. Prove s L ==> P(s)
and s N ==> Q(s) at the same time.


In this case, P(s) = Q(s) = s M.


Proof of P/Q by rule induction on the defining rules
of L & N.



The base case comes from rule L_E, which shows ε L. We
must show P(ε) == ε M.

This is just rule M_E:

---- M_E
ε  M



Inductive case 1 from rule N_N:

Assume s L and P(s). P(s) == s M.

Show Q( (s) ) == (s) M.

This is just rule M_N:

s M
----- M_N
(s) M



Inductive case 2 from rule L_J:

Assume s1 N and Q(s1) and s2 L and P(s2).

Q(s1) == s1 M.
P(s2) == s2 M.

We must prove s1s2 M.

This is just rule M_J:

s1 M     s2 M
------------- M_J
    s1s2 M


So we have shown by induction that s L ==> s M
and s N ==> s M, one of which is what we required.