theorem :: SCMPDS_2:79

for I being set holds
( not I is Instruction of SCMPDS or I = [0,{},{}] or ex k1 being Integer st I = goto k1 or ex a being Int_position st I = return a or ex a being Int_position ex k1 being Integer st I = saveIC (a,k1) or ex a being Int_position ex k1 being Integer st I = a := k1 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) := k2 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st I = (a,k1) >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = MultBy (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = Divide (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st I = (a,k1) := (b,k2) )