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