reconsider v = a as Element of SCM-Data-Loc by Def2;
2 in {2,3} by TARSKI:def 2;
then [2,{},<*v,k1*>] in SCMPDS-Instr by Th18;
hence [2,{},<*a,k1*>] is Instruction of SCMPDS ; :: thesis: verum