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