take Stop SCM+FSA ; :: thesis: ( Stop SCM+FSA is parahalting & Stop SCM+FSA is good & Stop SCM+FSA is halt-ending & Stop SCM+FSA is unique-halt )
thus ( Stop SCM+FSA is parahalting & Stop SCM+FSA is good & Stop SCM+FSA is halt-ending & Stop SCM+FSA is unique-halt ) ; :: thesis: verum