let i be Instruction of SCMPDS; :: thesis:
let m, n be Nat; :: thesis:
assume that
A1: i valid_at m and
A2: m <= n ; :: thesis:

A3: now :: thesis:

assume InsCode i = 4 ; :: thesis:
then consider a being Int_position, k1, k2 being Integer such that
A4: i = (a,k1) <>0_goto k2 and
A5: m + k2 >= 0 by A1;
take a = a; :: thesis:
take k1 = k1; :: thesis:
take k2 = k2; :: thesis:
thus i = (a,k1) <>0_goto k2 by A4; :: thesis:
thus n + k2 >= 0 by A2, A5, XREAL_1:6; :: thesis:

end;

A6: now :: thesis:

assume InsCode i = 6 ; :: thesis:
then consider a being Int_position, k1, k2 being Integer such that
A7: i = (a,k1) >=0_goto k2 and
A8: m + k2 >= 0 by A1;
take a = a; :: thesis:
take k1 = k1; :: thesis:
take k2 = k2; :: thesis:
thus i = (a,k1) >=0_goto k2 by A7; :: thesis:
thus n + k2 >= 0 by A2, A8, XREAL_1:6; :: thesis:

end;

A9: now :: thesis:

assume InsCode i = 5 ; :: thesis:
then consider a being Int_position, k1, k2 being Integer such that
A10: i = (a,k1) <=0_goto k2 and
A11: m + k2 >= 0 by A1;
take a = a; :: thesis:
take k1 = k1; :: thesis:
take k2 = k2; :: thesis:
thus i = (a,k1) <=0_goto k2 by A10; :: thesis:
thus n + k2 >= 0 by A2, A11, XREAL_1:6; :: thesis:

end;

now :: thesis:

assume InsCode i = 14 ; :: thesis:
then consider k1 being Integer such that
A12: i = goto k1 and
A13: m + k1 >= 0 by A1;
take k1 = k1; :: thesis:
thus i = goto k1 by A12; :: thesis:
thus n + k1 >= 0 by A2, A13, XREAL_1:6; :: thesis:

end;

hence i valid_at n by A3, A9, A6; :: thesis: