%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Figure 11 : Var-valid data stacks
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

vvalDS : stack -> stack -> type.

vvalDS_init : vvalDS dot dot.

vvalDS_stack : vvalDS (XXi , V) (Xi , T)
               <- ({xi:stack}vvalT xi T xi)
               <- vvalDS XXi Xi.