il. k in NAT by AMI_1:def 4;
hence k is Instruction-Location of SCM+FSA by AMI_1:def 4; :: thesis: verum