Data Type Induction Example 1



Consider these axia for type STACK:
   (1) top(new()) = undef
   (2) top(push(S,x)) = x
   (3) pop(new()) = new()
   (4) pop(push(S,x)) = S
   (5) size(new()) = 0
   (6) size(push(S,x)) = size(S) + 1
Prove this property: size(push(S,x)) > size(S)

We can first (or at any time) reduce the property by application of our axioms:

   size(push(S,x)) > size(S) 
     ==> size(S) + 1 > size(S)    by axiom 6
Now, use DT Induction. First, show the property holds for elements formed by "new()"
   size(new()) + 1 > size(new())
     ==> 0 + 1 > 0
     ==> true
Next, assume the property holds to some S' in STACK, i.e.,
   assume  size(S') + 1 > size(S')
Now, show that the property holds for elements formed by push(S',x):
   size(push(S',x)) + 1 > size(push(S',x))
     ==> size(S') + 1 + 1 > size(S') + 1      by axiom 6
     ==> size(S') + 1 > size(S')              sub. 1 from each side
                                                  (axiom of arithmetic)
     ==> true                                 by inductive hypothesis