We start with some notation and definitions. Given a finite set of
states, we write for the set of finite sequences of states over
, and for the set of possibly infinite state sequences.
Where `' stands for a possibly infinite state sequence in
and is a natural number, by `' we mean the
state of index in , by `' we mean the prefix
denotes the concatenation of and