let I, J be Program of ; :: thesis: for s being State of
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop I))),k) = CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),k)
let s be State of ; :: thesis: for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop I))),k) = CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),k)
let k be Element of NAT ; :: thesis: ( I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) implies CurInstr (Computation (s +* (Initialized (stop I))),k) = CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),k) )
set IsI = Initialized (stop I);
set IsJ = Initialized (stop (I ';' J));
set s1 = s +* (Initialized (stop I));
set s2 = s +* (Initialized (stop (I ';' J)));
set s3 = Computation (s +* (Initialized (stop I))),k;
set s4 = Computation (s +* (Initialized (stop (I ';' J)))),k;
set SS = Stop SCMPDS ;
assume that
A1: I is_closed_on s and
A2: ( I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) ) ; :: thesis: CurInstr (Computation (s +* (Initialized (stop I))),k) = CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),k)
A3: IC (Computation (s +* (Initialized (stop I))),k) in dom I by A1, A2, Th40;
A4: IC (Computation (s +* (Initialized (stop I))),k) = IC (Computation (s +* (Initialized (stop (I ';' J)))),k) by A1, A2, Th39;
A5: stop I = I ';' (Stop SCMPDS ) by SCMPDS_4:def 7;
A6: IC (Computation (s +* (Initialized (stop I))),k) in dom (stop I) by A1, Def2;
( Initialized (stop (I ';' J)) c= s +* (Initialized (stop (I ';' J))) & stop (I ';' J) c= Initialized (stop (I ';' J)) ) by FUNCT_4:26, SCMPDS_4:9;
then A7: ( dom (stop I) c= dom (stop (I ';' J)) & stop (I ';' J) c= s +* (Initialized (stop (I ';' J))) ) by SCMPDS_5:16, XBOOLE_1:1;
( Initialized (stop I) c= s +* (Initialized (stop I)) & stop I c= Initialized (stop I) ) by FUNCT_4:26, SCMPDS_4:9;
then A8: stop I c= s +* (Initialized (stop I)) by XBOOLE_1:1;
A9: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS ) by SCMPDS_4:def 7
.= I ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46 ;
thus CurInstr (Computation (s +* (Initialized (stop I))),k) = (s +* (Initialized (stop I))) . (IC (Computation (s +* (Initialized (stop I))),k)) by AMI_1:54
.= (stop I) . (IC (Computation (s +* (Initialized (stop I))),k)) by A6, A8, GRFUNC_1:8
.= I . (IC (Computation (s +* (Initialized (stop I))),k)) by A3, A5, SCMPDS_4:37
.= (stop (I ';' J)) . (IC (Computation (s +* (Initialized (stop I))),k)) by A3, A9, SCMPDS_4:37
.= (s +* (Initialized (stop (I ';' J)))) . (IC (Computation (s +* (Initialized (stop (I ';' J)))),k)) by A4, A6, A7, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),k) by AMI_1:54 ; :: thesis: verum