for i being Instruction of SCMPDS
for m, n being Nat st i valid_at m & m <= n holds
i valid_at n