let s2 be State of SCMPDS; :: thesis:
let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis:
let s1 be 0 -started State of SCMPDS; :: thesis:
let I be shiftable Program of SCMPDS; :: thesis:
set SI = stop I;
assume that
A1: stop I c= P1 and
A2: I is_closed_on s1,P1 ; :: thesis:
A0: Initialize s1 = s1 by MEMSTR_0:44;
let n be Element of NAT ; :: thesis:
defpred S₁[ Element of NAT ] means ( (IC (Comput (P1,s1,$1))) + n = IC (Comput (P2,s2,$1)) & CurInstr (P1,(Comput (P1,s1,$1))) = CurInstr (P2,(Comput (P2,s2,$1))) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) );
assume that
A5: Shift ((stop I),n) c= P2 and
A6: IC s2 = n and
A7: DataPart s1 = DataPart s2 ; :: thesis:
let i be Element of NAT ; :: thesis:
A8: DataPart (Comput (P1,s1,0)) = DataPart s2 by A7, EXTPRO_1:2
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ;
A9: 0 in dom (stop I) by COMPOS_1:36;
then A10: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:24;
A12: P1 . (IC s1) = P1 . (IC (Initialize s1)) by A0
.= P1 . 0 by MEMSTR_0:def 8
.= (stop I) . 0 by A1, A9, GRFUNC_1:2 ;
A14: P1 = P1 +* (stop I) by A1, FUNCT_4:98;
A15: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A16: S₁[k] ; :: thesis:
reconsider m = IC (Comput (P1,s1,k)) as Element of NAT ;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A18: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Element of NAT ;
A19: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A2, A14, Def2, A0;
then A20: l + n in dom (Shift ((stop I),n)) by VALUED_1:24;
A22: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3;
A23: IC (Comput (P1,s1,k)) in dom (stop I) by A2, A14, Def2, A0;
A24: P1 /. (IC (Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143;
A25: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by A24
.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A23, GRFUNC_1:2 ;
then A26: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by A23, SCMPDS_4:def 9;
A27: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A23, A25, SCMPDS_4:def 9;
hence A28: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A16, A18, A22, A26, SCMPDS_4:28; :: thesis:
A29: P1 /. (IC (Comput (P1,s1,(k + 1)))) = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:143;
A30: P2 /. (IC (Comput (P2,s2,(k + 1)))) = P2 . (IC (Comput (P2,s2,(k + 1)))) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . l by A29
.= (stop I) . l by A1, A19, GRFUNC_1:2
.= (stop I) . l ;
hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (IC (Comput (P2,s2,(k + 1)))) by A28, A19, VALUED_1:def 12
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A5, A28, A20, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by A30 ;
:: thesis:
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A16, A18, A22, A26, A27, SCMPDS_4:28; :: thesis:

end;

A31: IC (Comput (P1,s1,0)) = IC s1 by EXTPRO_1:2
.= IC (Initialize s1) by A0
.= 0 by MEMSTR_0:def 8 ;
A32: Comput (P1,s1,0) = s1 by EXTPRO_1:2;
A33: Comput (P2,s2,0) = s2 by EXTPRO_1:2;
A34: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A35: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by A32
.= (Shift ((stop I),n)) . (0 + n) by A9, A12, A35, VALUED_1:def 12
.= CurInstr (P2,s2) by A5, A6, A10, A34, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,0))) by A33 ;
then A36: S₁[ 0 ] by A6, A31, A8, EXTPRO_1:2;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A36, A15);
hence ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ; :: thesis: