TerminatingQ property

[maxitg]

The problem

We can prove that a system is not terminating (as a multiway system) if there exists a subhistory e such that its initial state e[0] is isomorphic to a subset of its final state.

We should be able to use this to prove that some systems are non-terminating, and implement a property "TerminatingQ" which would check for that.

Possible solution

More specifically, it will return:

1. True if the termination reason is "FixedPoint".
2. False if the property specified above is satisfied.
3. Missing["Unknown"] if neither.

Additional context

This is an idea from Jonathan Gorard mentioned in the context of combinators.