let s1, s2 be State of ; :: thesis: for I being Program of st I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let I be Program of ; :: thesis: ( I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
set pI = stop I;
set IsI = Initialized (stop I);
assume that
A1: I is_closed_on s1 and
A2: Initialized (stop I) c= s1 and
A3: Initialized (stop I) c= s2 and
A4: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( IC (Computation s1,i) = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
A5: IC SCMPDS in dom (Initialized (stop I)) by SCMPDS_4:7;
then A6: IC s1 = (Initialized (stop I)) . (IC SCMPDS ) by A2, GRFUNC_1:8
.= IC s2 by A3, A5, GRFUNC_1:8 ;
defpred S₁[ Element of NAT ] means ( IC (Computation s1,$1) = IC (Computation s2,$1) & CurInstr (Computation s1,$1) = CurInstr (Computation s2,$1) & DataPart (Computation s1,$1) = DataPart (Computation s2,$1) );
stop I c= Initialized (stop I) by SCMPDS_4:9;
then A7: dom (stop I) c= dom (Initialized (stop I)) by GRFUNC_1:8;
A8: s1 = s1 +* (Initialized (stop I)) by A2, FUNCT_4:79;
then IC (Computation s1,0 ) in dom (stop I) by A1, SCMPDS_6:def 2;
then A9: IC s1 in dom (stop I) by AMI_1:13;
then A10: s1 . (IC s1) = (Initialized (stop I)) . (IC s1) by A2, A7, GRFUNC_1:8
.= s2 . (IC s2) by A3, A7, A9, A6, GRFUNC_1:8 ;
A11: DataPart (Computation s1,0 ) = DataPart s2 by A4, AMI_1:13
.= DataPart (Computation s2,0 ) by AMI_1:13 ;
A12: CurInstr (Computation s1,0 ) = CurInstr s1 by AMI_1:13
.= CurInstr s2 by A10
.= CurInstr (Computation s2,0 ) by AMI_1:13 ;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: S₁[k] ; :: thesis: S₁[k + 1]
set l = IC (Computation s1,(k + 1));
A15: IC (Computation s1,(k + 1)) in dom (stop I) by A1, A8, SCMPDS_6:def 2;
set i = CurInstr (Computation s1,k);
A16: Computation s1,(k + 1) = Following (Computation s1,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s1,k) ;
A17: Computation s2,(k + 1) = Following (Computation s2,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s2,k) by A14 ;
hence IC (Computation s1,(k + 1)) = IC (Computation s2,(k + 1)) by A14, A16, Th23; :: thesis: ( CurInstr (Computation s1,(k + 1)) = CurInstr (Computation s2,(k + 1)) & DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) )
thus CurInstr (Computation s1,(k + 1)) = s1 . (IC (Computation s1,(k + 1))) by AMI_1:54
.= (Initialized (stop I)) . (IC (Computation s1,(k + 1))) by A2, A7, A15, GRFUNC_1:8
.= s2 . (IC (Computation s1,(k + 1))) by A3, A7, A15, GRFUNC_1:8
.= (Computation s2,(k + 1)) . (IC (Computation s1,(k + 1))) by AMI_1:54
.= CurInstr (Computation s2,(k + 1)) by A14, A16, A17, Th23 ; :: thesis: DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1))
thus DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) by A14, A16, A17, Th23; :: thesis: verum

end;

IC (Computation s1,0 ) = IC s1 by AMI_1:13
.= IC (Computation s2,0 ) by A6, AMI_1:13 ;
then A18: S₁[ 0 ] by A12, A11;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A18, A13); :: thesis: verum