let i be Instruction of SCMPDS; :: thesis: for s being State of SCMPDS
for I being Program of
for P being Instruction-Sequence of SCMPDS holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
let s be State of SCMPDS; :: thesis: for I being Program of
for P being Instruction-Sequence of SCMPDS holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
let I be Program of ; :: thesis: for P being Instruction-Sequence of SCMPDS holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
let P be Instruction-Sequence of SCMPDS; :: thesis: CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i
set iI = i ';' I;
set P3 = P +* (stop (i ';' I));
A1: 0 in dom (Load i) by COMPOS_1:50;
card (i ';' I) = (card I) + 1 by Th1;
then A2: 0 in dom (i ';' I) by AFINSQ_1:66;
i ';' I c= stop (i ';' I) by AFINSQ_1:74;
then dom (i ';' I) c= dom (stop (i ';' I)) by RELAT_1:11;
then A3: 0 in dom (stop (i ';' I)) by A2;
A4: (P +* (stop (i ';' I))) /. (IC (Initialize s)) = (P +* (stop (i ';' I))) . (IC (Initialize s)) by PBOOLE:143;
(P +* (stop (i ';' I))) . 0 = (P +* (stop (i ';' I))) . 0
.= (stop (i ';' I)) . 0 by A3, FUNCT_4:13
.= (i ';' I) . 0 by A2, COMPOS_1:63
.= ((Load i) ';' I) . 0
.= (Load i) . 0 by A1, AFINSQ_1:def 3
.= i ;
hence CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i by A4, MEMSTR_0:47; :: thesis: verum