helphome pageduck scriptspecificationfirst proof pagepage 1 1

A Lemma About Double Operation


We want to prove
( M  N  : Nat  )
            2 * M = 2 * N
       implies
            M = N .
We take the following steps:
  • Quantifier elimination introduces the new constant(s) m, n : Nat  .
  • Implication elimination assumes
        2 * m = 2 * n .
  • We introduce the lemma
      ( M  : Nat  ) div2(2 * M) = M.
    Click here to see its proof.
  • We apply an operation div2 to the both sides of the equation in the hypothesis:
             2 * m = 2 * n ,
    and get   m = n .
  • We change the equation m = n to rewriting rule.
  • We show m = n 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:12 PST 2001.