take Macro (halt SCM+FSA) ; :: thesis: ( Macro (halt SCM+FSA) is keeping_0 & Macro (halt SCM+FSA) is InitHalting )
thus ( Macro (halt SCM+FSA) is keeping_0 & Macro (halt SCM+FSA) is InitHalting ) ; :: thesis: verum