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= Computation (s +* (Initialized (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= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds Shift (stop I),2 c= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n
let I be Program of SCMPDS ; :: thesis: Shift (stop I),2 c= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n
set pI = stop I;
set pjI = stop ((i ';' j) ';' I);
set IsjI = Initialized (stop ((i ';' j) ';' I));
set s3 = s +* (Initialized (stop ((i ';' j) ';' I)));
card (i ';' j) = card ((Load i) ';' (Load j)) by SCMPDS_4:def 6
.= (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 +* (Initialized (stop ((i ';' j) ';' I))) by FUNCT_4:26, SCMPDS_4:57;
then Shift (stop I),2 c= s +* (Initialized (stop ((i ';' j) ';' I))) by A1, XBOOLE_1:1;
hence Shift (stop I),2 c= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n by AMI_1:81; :: thesis: verum