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