let n be Element of NAT ; :: thesis: for i being Instruction of
for s being State of
for I being Program of holds Shift (stop I),1 c= Computation (s +* (Initialized (stop (i ';' I)))),n
let i be Instruction of ; :: thesis: for s being State of
for I being Program of holds Shift (stop I),1 c= Computation (s +* (Initialized (stop (i ';' I)))),n
let s be State of ; :: thesis: for I being Program of holds Shift (stop I),1 c= Computation (s +* (Initialized (stop (i ';' I)))),n
let I be Program of ; :: thesis: Shift (stop I),1 c= Computation (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= Computation (s +* (Initialized (stop (i ';' I)))),n by AMI_1:81; :: thesis: verum