thus l -' k is Instruction-Location of S by AMI_1:def 4; :: thesis: verum