A checking automaton is equivalent to a one-way nonerasing stack automaton which, once it enters its stack, never again writes on its stack. The checking automaton languages (cal) form a full AFL closed under substitution. If L C a* is an infinite cal, then L contains an infinite regular set. Consequently, there are one-way nonerasing stack languages (such as {a "2 ;n > 1}) which are not cal.
Let .~ be the family of one-way stack languages and let "Lax be a subAFL of -~. .W is closed under substitution into ~1 if and only if -Z' x is contained in the family of context-free languages. &a is closed under substitution by -W1 if and only if -~t is a family of cal. Hence, the one-way stack languages are not closed under substitution. The one-way nested stack languages properly include the stack languages.
The family of quasi-real-time one-way stack languages is not closed under substitution by cal. Thus the quasi-real-time one-way stack languages are not a full AFL but are a proper subAFL of the one-way stack languages.
Let .Z'tr be the family of one-way nonerasing stack languages, and let -Z' x be a subAFL. Then &aN is closed under substitution into -~t if and only if ~x is a family of regular sets. Hence -Z}N is a proper subfamily of .L ,a.