:: deftheorem defines halting GLIB_000:def 82 :
for GSq being GraphSeq holds
( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) );