theorem Th1: :: SCM_HALT:2

Macro (halt SCM+FSA) is InitHalting