let i be Instruction of SCMPDS; :: thesis: for m, n being Nat st i valid_at m & m <= n holds

i valid_at n

let m, n be 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

i valid_at n

let m, n be 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 :: thesis: ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) )

( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) )

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;

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:6; :: thesis: verum

end;( 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;

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:6; :: thesis: verum

A6: now :: thesis: ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) )

( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) )

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;

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:6; :: thesis: verum

end;( 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;

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:6; :: thesis: verum

A9: now :: thesis: ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) )

( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) )

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;

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:6; :: thesis: verum

end;( 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;

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:6; :: thesis: verum

now :: thesis: ( InsCode i = 14 implies ex k1 being Integer st

( i = goto k1 & n + k1 >= 0 ) )

hence
i valid_at n
by A3, A9, A6; :: thesis: verum( i = goto k1 & n + k1 >= 0 ) )

assume
InsCode i = 14
; :: 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;

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:6; :: thesis: verum

end;( i = goto k1 & n + k1 >= 0 )

then consider k1 being Integer such that

A12: i = goto k1 and

A13: m + k1 >= 0 by A1;

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:6; :: thesis: verum