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