page 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:
Base case: prove the assertion for
K = 1
.
We show
1 > 0
by
reduction
.
Induction case: assume the assertion for
K =
, and then prove it for
K = s N0
.
Quantifier elimination
introduces the new constant(s)
n0 : Nat
.
We show
(s n0) > 0
by
reduction
.
And thus the main goal is proved.
Left
Up
Down
Right
This page was generated by Kumo on Tue Feb 13 19:36:08 PST 2001.
K
: NzNat
)
K > 0 .
