let i be Instruction of SCMPDS ; :: thesis: for m, n being Element of NAT st i valid_at m & m <= n holds
i valid_at n
let m, n be Element of NAT ; :: thesis: ( i valid_at m & m <= n implies i valid_at n )
assume that
A1: i valid_at m and
A2: m <= n ; :: thesis: i valid_at n

A3: now

assume InsCode i = 4 ; :: thesis: ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <>0_goto k2 & n + k2 >= 0 )
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, Def11;
take a = a; :: thesis: ex k1, k2 being Integer st
( i = a,k1 <>0_goto k2 & n + k2 >= 0 )
take k1 = k1; :: thesis: ex k2 being Integer st
( i = a,k1 <>0_goto k2 & n + k2 >= 0 )
take k2 = k2; :: thesis: ( i = a,k1 <>0_goto k2 & n + k2 >= 0 )
thus i = a,k1 <>0_goto k2 by A4; :: thesis: n + k2 >= 0
thus n + k2 >= 0 by A2, A5, XREAL_1:8; :: thesis: verum

end;

A6: now

assume InsCode i = 6 ; :: thesis: ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 >=0_goto k2 & n + k2 >= 0 )
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, Def11;
take a = a; :: thesis: ex k1, k2 being Integer st
( i = a,k1 >=0_goto k2 & n + k2 >= 0 )
take k1 = k1; :: thesis: ex k2 being Integer st
( i = a,k1 >=0_goto k2 & n + k2 >= 0 )
take k2 = k2; :: thesis: ( i = a,k1 >=0_goto k2 & n + k2 >= 0 )
thus i = a,k1 >=0_goto k2 by A7; :: thesis: n + k2 >= 0
thus n + k2 >= 0 by A2, A8, XREAL_1:8; :: thesis: verum

end;

A9: now

assume InsCode i = 5 ; :: thesis: ex a being Int_position ex k1, k2 being Integer st
( i = a,k1 <=0_goto k2 & n + k2 >= 0 )
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, Def11;
take a = a; :: thesis: ex k1, k2 being Integer st
( i = a,k1 <=0_goto k2 & n + k2 >= 0 )
take k1 = k1; :: thesis: ex k2 being Integer st
( i = a,k1 <=0_goto k2 & n + k2 >= 0 )
take k2 = k2; :: thesis: ( i = a,k1 <=0_goto k2 & n + k2 >= 0 )
thus i = a,k1 <=0_goto k2 by A10; :: thesis: n + k2 >= 0
thus n + k2 >= 0 by A2, A11, XREAL_1:8; :: thesis: verum

end;

now

assume InsCode i = 0 ; :: thesis: ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 )
then consider k1 being Integer such that
A12: i = goto k1 and
A13: m + k1 >= 0 by A1, Def11;
take k1 = k1; :: thesis: ( i = goto k1 & n + k1 >= 0 )
thus i = goto k1 by A12; :: thesis: n + k1 >= 0
thus n + k1 >= 0 by A2, A13, XREAL_1:8; :: thesis: verum

end;

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