page 1 1

A Natural Number Must be Odd or Even

We want to prove
( M  : Nat  )
(N  : Nat  )
M = 2 * N
or
M = (2 * N) + 1 .
We use induction on M to prove this goal. For this, we use the induction scheme based on the signature { 0, s } for Nat. Induction requires that we do the following:
1. Base case: prove the assertion for M = 0 .
• Let N = 0 . Then we need to prove  0 = 2 * 0 or       0 = (2 * 0) + 1 .
• Disjunction elimination yields 2 subgoals:
1. 0 = 2 * 0
2. 0 = (2 * 0) + 1
2. Induction case: assume the assertion for M = N0 , and then prove it for M = s N0 .
• Quantifier elimination introduces the new constant(s) n0 : Nat  .
• Implication elimination assumes  (N  : Nat  )             n0 = 2 * N       or             n0 = (2 * N) + 1 .
• By skolemization, we can get  n0 = 2 * n1 or       n0 = (2 * n1) + 1
from the following hypothesis  (N  : Nat  )             n0 = 2 * N       or             n0 = (2 * N) + 1 .
• We do case analysis on  n0 = 2 * n1 or       n0 = (2 * n1) + 1 ,
and we get 2 cases:
1. Case: n0 = 2 * n1 .
• We change the equation n0 = 2 * n1 to rewriting rule.
• Let N = n1 . Then we need to prove  s n0 = 2 * n1 or       s n0 = (2 * n1) + 1 .
• Disjunction elimination yields 2 subgoals:
1. s n0 = 2 * n1
2. s n0 = (2 * n1) + 1
2. Case: n0 = (2 * n1) + 1 .
• We change the equation n0 = (2 * n1) + 1 to rewriting rule.
• Let N = n1 + 1 . Then we need to prove  s n0 = 2 * (n1 + 1) or       s n0 = (2 * (n1 + 1)) + 1 .
• Disjunction elimination yields 2 subgoals:
1. s n0 = 2 * (n1 + 1)
2. s n0 = (2 * (n1 + 1)) + 1

And thus the main goal is proved.

 Left    Up    Down    Right

This page was generated by Kumo on Tue Feb 13 19:35:59 PST 2001.