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