helphome pageduck scriptspecificationfirst proof pagepage 1 1

A Relation between Sum and Subtract


We want to prove
( N  M  : Nat  ) (M + N) - N = M .
We use induction on N 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 N = 0 .
  2. Induction case: assume the assertion for N = N0 , and then prove it for N = s N0 .

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:06 PST 2001.