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