set IJ = I ';' J;

_{1} being Program of st b_{1} = I ';' J holds

b_{1} is shiftable
; :: thesis: verum

now :: thesis: for n being Nat

for i being Instruction of SCMPDS st n in dom (I ';' J) & i = (I ';' J) . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

hence
for bfor i being Instruction of SCMPDS st n in dom (I ';' J) & i = (I ';' J) . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )

set D = { (l + (card I)) where l is Nat : l in dom J } ;

let n be Nat; :: thesis: for i being Instruction of SCMPDS st n in dom (I ';' J) & i = (I ';' J) . n holds

( InsCode b_{3} <> 1 & InsCode b_{3} <> 3 & b_{3} valid_at b_{2} )

let i be Instruction of SCMPDS; :: thesis: ( n in dom (I ';' J) & i = (I ';' J) . n implies ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} ) )

assume that

A1: n in dom (I ';' J) and

A2: i = (I ';' J) . n ; :: thesis: ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} )

dom (Shift (J,(card I))) = { (l + (card I)) where l is Nat : l in dom J } by VALUED_1:def 12;

then A3: dom (I ';' J) = (dom I) \/ { (l + (card I)) where l is Nat : l in dom J } by FUNCT_4:def 1;

end;let n be Nat; :: thesis: for i being Instruction of SCMPDS st n in dom (I ';' J) & i = (I ';' J) . n holds

( InsCode b

let i be Instruction of SCMPDS; :: thesis: ( n in dom (I ';' J) & i = (I ';' J) . n implies ( InsCode b

assume that

A1: n in dom (I ';' J) and

A2: i = (I ';' J) . n ; :: thesis: ( InsCode b

dom (Shift (J,(card I))) = { (l + (card I)) where l is Nat : l in dom J } by VALUED_1:def 12;

then A3: dom (I ';' J) = (dom I) \/ { (l + (card I)) where l is Nat : l in dom J } by FUNCT_4:def 1;

per cases
( n in dom I or n in { (l + (card I)) where l is Nat : l in dom J } )
by A1, A3, XBOOLE_0:def 3;

end;

suppose A4:
n in dom I
; :: thesis: ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} )

then
I . n = i
by A2, AFINSQ_1:def 3;

hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A4, Def9; :: thesis: verum

end;hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A4, Def9; :: thesis: verum

suppose
n in { (l + (card I)) where l is Nat : l in dom J }
; :: thesis: ( InsCode b_{2} <> 1 & InsCode b_{2} <> 3 & b_{2} valid_at b_{1} )

then consider l being Nat such that

A5: n = l + (card I) and

A6: l in dom J ;

A7: J . l = i by A2, A5, A6, AFINSQ_1:def 3;

hence ( InsCode i <> 1 & InsCode i <> 3 ) by A6, Def9; :: thesis: i valid_at n

i valid_at l by A6, A7, Def9;

hence i valid_at n by A5, Th20, NAT_1:11; :: thesis: verum

end;A5: n = l + (card I) and

A6: l in dom J ;

A7: J . l = i by A2, A5, A6, AFINSQ_1:def 3;

hence ( InsCode i <> 1 & InsCode i <> 3 ) by A6, Def9; :: thesis: i valid_at n

i valid_at l by A6, A7, Def9;

hence i valid_at n by A5, Th20, NAT_1:11; :: thesis: verum

b