thus halt (STC N) is ins-loc-free ; :: according to COMPOS_1:def 39 :: thesis: verum