let n be Element of NAT ; :: thesis: for i, j being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop ((i ';' j) ';' I)))),((Initialize s) +* (stop ((i ';' j) ';' I))),n
let i, j be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop ((i ';' j) ';' I)))),((Initialize s) +* (stop ((i ';' j) ';' I))),n
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop ((i ';' j) ';' I)))),((Initialize s) +* (stop ((i ';' j) ';' I))),n
let I be Program of SCMPDS ; :: thesis: Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop ((i ';' j) ';' I)))),((Initialize s) +* (stop ((i ';' j) ';' I))),n
set pI = stop I;
set pjI = stop ((i ';' j) ';' I);
set s3 = s +* (Initialize (stop ((i ';' j) ';' I)));
I1: s +* (Initialize (stop ((i ';' j) ';' I))) = (Initialize s) +* (stop ((i ';' j) ';' I)) by SCMPDS_4:5;
card (i ';' j) = card ((Load i) ';' (Load j))
.= (card (Load i)) + (card (Load j)) by SCMPDS_4:45
.= 1 + (card (Load j)) by SCMPDS_5:6
.= 1 + 1 by SCMPDS_5:6 ;
then A1: Shift (stop I),2 c= stop ((i ';' j) ';' I) by Th24;
stop ((i ';' j) ';' I) c= s +* (Initialize (stop ((i ';' j) ';' I))) by FUNCT_4:26, SCMPDS_4:57;
then Shift (stop I),2 c= s +* (Initialize (stop ((i ';' j) ';' I))) by A1, XBOOLE_1:1;
hence Shift (stop I),2 c= Comput (ProgramPart ((Initialize s) +* (stop ((i ';' j) ';' I)))),((Initialize s) +* (stop ((i ';' j) ';' I))),n by I1, AMI_1:81; :: thesis: verum