take h = halt SCM+FSA; :: thesis: h is good
Macro h is good by SCMFSA7B:11, SCMFSA8C:99;
hence h is good by Def1; :: thesis: verum