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