let n be Element of NAT ; :: thesis: for i being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))),n
let i be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))),n
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds Shift (stop I),1 c= Comput (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))),n
let I be Program of SCMPDS ; :: thesis: Shift (stop I),1 c= Comput (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))),n
set pI = stop I;
set iI = i ';' I;
set piI = stop (i ';' I);
set IsiI = Initialized (stop (i ';' I));
set s3 = s +* (Initialized (stop (i ';' I)));
( card (Load i) = 1 & i ';' I = (Load i) ';' I ) by SCMPDS_4:def 4, SCMPDS_5:6;
then A1: Shift (stop I),1 c= stop (i ';' I) by Th24;
stop (i ';' I) c= s +* (Initialized (stop (i ';' I))) by FUNCT_4:26, SCMPDS_4:57;
then Shift (stop I),1 c= s +* (Initialized (stop (i ';' I))) by A1, XBOOLE_1:1;
hence Shift (stop I),1 c= Comput (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))),n by AMI_1:81; :: thesis: verum