Now you have to talk about what a specification is. If it is a relation from some function input to its output, that would be one step. And of course, function

Now you have to talk about what a specification is. If it is a relation from some function input to its output, that would be one step. And of course, functions are composable that way. But say you have a system behaviour that is a stream of function applications, e.g. [f(0), f(f(0)), f(f(f(0)))...] and I forgot the name for this function. This infinite stream is your system behaviour. Now we have a different behaviour [g(0), g(g(0)), g(g(g(0)))...] You can (more or less) easily reason about the relation of g^n(0) to f^n(0) where both streams or behaviours are synchronous. But reasoning about the behaviour of all g^n(0) in relation to all f^m(0) is difficult. All the useful properties for these streams, liveness, fairness, as well as other invariants, are not easily encoded.