Checking automata and one-way stack languages

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 ⊆ a* is an infinite cal, then L contains an infinite regular set. Consequently, there are one-way nonerasing stack languages (such as (an2|n≥1|)) which are not cal. Let L be the family of one-way stack languages and let L1 be a subAFL of L. L is closed under substitution into L1 if and only if L1 is contained in the family of context-free languages. L is closed under substitution by L1 if and only if L1 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 LN be the family of one-way nonerasing stack languages, and let L1 be a subAFL. Then LN is closed under substitution into L1 if and only if L1 is a family of regular sets. Hence LN is a proper subfamily of L.