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