(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) + 1Prove 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 6Now, use DT Induction. First, show the property holds for elements formed by "new()"
size(new()) + 1 > size(new()) ==> 0 + 1 > 0 ==> trueNext, 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