fth DATA is
	sort Element .
endfth

fmod STACK{E :: DATA} is
	sort Stack .
	subsort E$Element < Stack .
	protecting NAT .
	
	op empty : -> Stack .
	op push : E$Element Stack -> Stack .
	op top : Stack -> E$Element .
	op pop : Stack -> Stack .
	op length : Stack -> Nat .
	
	var X Y : E$Element . vars S S2 : Stack .
	eq top(push(X,S)) = X .
	eq pop(push(X,S)) = S .
	eq length(empty) = 0 .
	eq length(push(X,S)) = 1 + length(S) .
endfm

*** Example usage
red pop(push(X,S)) == S .
red top(pop(push(X,push(Y,S)))) == Y .
red S == push(X,S2) implies push(top(S),pop(S)) == S .
red S == push(X,S2) implies length(pop(S)) + 1 == length(S) .