not (Macro (SubFrom (a,b))) ';' (if=0 (a,I,J)) is halt-free ;
hence not if=0 (a,b,I,J) is halt-free by SCMFSA6A:def 6; :: thesis: verum