reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by Def2;
9 in {9,10,11,12,13} by ENUMSET1:def 3;
then [9,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th20;
hence [9,{},<*a,b,k1,k2*>] is Instruction of SCMPDS ; :: thesis: verum