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