// Non-empty stacks.
// 
// For purpose statements and algebraic specification, see Stack.java.

class Push<E> extends StackBase<E> {

    Stack<E> s;       // the other elements of this Stack
    E x;              // the topmost element of this Stack

    Push (Stack<E> s, E x) {
        this.s = s;
        this.x = x;
    }

    public Stack<E> push (E x) {
        return new Push<E> (this, x);
    }

    public boolean isEmpty () {
        return false;
    }

    public E top () {
        return x;
    }

    public Stack<E> pop () {
        return s;
    }

    public int size () {
        return 1 + s.size();
    }
}