for Gs being ManySortedSet of NAT st Gs is halting & Gs is iterative holds
Gs is eventually-constant