thus ( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting ) by Lm2; :: according to SCMFSA6C:def 1,SCMFSA6C:def 2 :: thesis: verum