let i be Instruction of SCMPDS; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
let I be Program of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
set iI = i ';' I;
set s3 = s +* (Initialize (stop (i ';' I)));
set P3 = P +* (stop (i ';' I));
A2: 0 in dom (Load i) by SCMPDS_5:2;
card (i ';' I) = (card I) + 1 by Th15;
then A3: 0 in dom (i ';' I) by AFINSQ_1:70;
i ';' I c= stop (i ';' I) by AFINSQ_1:78;
then dom (i ';' I) c= dom (stop (i ';' I)) by RELAT_1:25;
then B3: 0 in dom (stop (i ';' I)) by A3;
A4: (P +* (stop (i ';' I))) /. (IC (Initialize s)) = (P +* (stop (i ';' I))) . (IC (Initialize s)) by PBOOLE:158;
(P +* (stop (i ';' I))) . 0 = (P +* (stop (i ';' I))) . 0
.= (stop (i ';' I)) . 0 by B3, FUNCT_4:14
.= (i ';' I) . 0 by A3, Th20
.= ((Load i) ';' I) . 0
.= (Load i) . 0 by A2, AFINSQ_1:def 4
.= i by SCMPDS_5:4 ;
hence CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i by A4, COMPOS_1:223; :: thesis: verum