:: deftheorem defines halting GLIB_000:def 55 :
for F being ManySortedSet of NAT holds
( F is halting iff ex n being Nat st F . n = F . (n + 1) );