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 COMPOS_1:125;
card (i ';' j) = card ((Load i) ';' (Load j))
.= (card (Load i)) + (card (Load j)) by AFINSQ_1:20
.= 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 COMPOS_1:132, FUNCT_4:26;
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