helphome pageduck scriptspecificationfirst proof pagepage 1 1

A Lemma About Double Operation


We want to prove
( M  N  : Nat  )
            (2 * M) * M = N * N
       implies
             (K  : Nat  ) N = 2 * K .
We take the following steps:
  • Quantifier elimination introduces the new constant(s) m, n : Nat  .
  • Implication elimination assumes
        (2 * m) * m = n * n .
  • We introduce the lemma
      ( M  : Nat  )
           (N  : Nat  )
                      M = 2 * N
                 or
                      M = (2 * N) + 1.
    Click here to see its proof.
  • In the following hypothesis
        ( M  : Nat  )
           (N  : Nat  )
                      M = 2 * N
                 or
                      M = (2 * N) + 1
    ,
    let M  = n , we get
        (N  : Nat  )
                n = 2 * N
           or
                n = (2 * N) + 1
    ,
  • By skolemization, we can get
              n = 2 * n1
    or
          n = (2 * n1) + 1
    from the following hypothesis
        (N  : Nat  )
                n = 2 * N
           or
                n = (2 * N) + 1
    .
  • We do case analysis on
              n = 2 * n1
    or
          n = (2 * n1) + 1
    ,
    and we get 2 cases:
    1. Case: n = 2 * n1 .
      • We change the equation n = 2 * n1 to rewriting rule.
      • Let K = n1 . Then we need to prove
            n = 2 * n1 .
      • We show n = 2 * n1 by reduction.
    2. Case: n = (2 * n1) + 1 .
      • Then we apply equation n = (2 * n1) + 1 to the hypothesis
            (2 * m) * m = n * n ,
        and get
            (2 * m) * m = s (((((n1 * n1) + (n1 * n1)) + ((n1 * n1) + (n1 * n1))) + (n1 + n1)) + (n1 + n1)) ,
      • We introduce the lemma
          ( M  : Nat  ) mod2(2 * M) = 0.
        Click here to see its proof.
      • We introduce the lemma
          ( M  : Nat  ) mod2((2 * M) + 1) = 1.
        Click here to see its proof.
      • We apply an operation mod2 to the both sides of the equation in the hypothesis:
                 (2 * m) * m = s (((((n1 * n1) + (n1 * n1)) + ((n1 * n1) + (n1 * n1))) + (n1 + n1)) + (n1 + n1)) ,
        and get   0 = s 0 .
      • We show 0 = s 0 is false by reduction.

And thus the main goal is proved.

BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Tue Feb 13 19:36:10 PST 2001.