helphome pageduck scriptspecificationfirst proof pagepage 1 1

NzNat is Greater than Zero

We want to prove
( K  : NzNat  ) K > 0 .
We use induction on K to prove this goal. For this, we use the induction scheme based on the signature { 1, s } for NzNat. Induction requires that we do the following:
  1. Base case: prove the assertion for K = 1 .
  2. Induction case: assume the assertion for K = , and then prove it for K = 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:08 PST 2001.