let i be Instruction of SCMPDS ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds CurInstr (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))) = i
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds CurInstr (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))) = i
let I be Program of SCMPDS ; :: thesis: CurInstr (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))) = i
set iI = i ';' I;
set IsiI = Initialized (stop (i ';' I));
set s3 = s +* (Initialized (stop (i ';' I)));
A1: 0 in dom (Load i) by SCMPDS_5:2;
card (i ';' I) = (card I) + 1 by Th15;
then A2: 0 in dom (i ';' I) by SCMPDS_4:1;
Y: (ProgramPart (s +* (Initialized (stop (i ';' I))))) /. (IC (s +* (Initialized (stop (i ';' I))))) = (s +* (Initialized (stop (i ';' I)))) . (IC (s +* (Initialized (stop (i ';' I))))) by AMI_1:150;
i ';' I c= Initialized (stop (i ';' I)) by Th17;
then dom (i ';' I) c= dom (Initialized (stop (i ';' I))) by GRFUNC_1:8;
then (s +* (Initialized (stop (i ';' I)))) . 0 = (Initialized (stop (i ';' I))) . 0 by A2, FUNCT_4:14
.= (i ';' I) . 0 by A2, Th20
.= ((Load i) ';' I) . 0 by SCMPDS_4:def 4
.= (Load i) . 0 by A1, SCMPDS_4:37
.= i by SCMPDS_5:4 ;
hence CurInstr (ProgramPart (s +* (Initialized (stop (i ';' I))))),(s +* (Initialized (stop (i ';' I)))) = i by FUNCT_4:26, SCMPDS_5:18, Y; :: thesis: verum