take halt S ; :: thesis: halt S is ins-loc-free
thus halt S is ins-loc-free ; :: thesis: verum