helphome pageduck scriptspecificationfirst proof pagepage 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.

BOBJ proof scoreLeft    Up    Down    Right   
 

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