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