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 ; :: thesis:
set SI = stop I;
assume that
A1: stop I c= P1 and
A2: I is_closed_on s1,P1 ; :: thesis:
A3: Initialize s1 = s1 by MEMSTR_0:44;
let n be Nat; :: thesis:
defpred S₁[ 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
A4: Shift ((stop I),n) c= P2 and
A5: IC s2 = n and
A6: DataPart s1 = DataPart s2 ; :: thesis:
let i be Nat; :: thesis:
A7: DataPart (Comput (P1,s1,0)) = DataPart s2 by A6, EXTPRO_1:2
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ;
A8: 0 in dom (stop I) by COMPOS_1:36;
then A9: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:24;
A10: P1 . (IC s1) = P1 . (IC (Initialize s1)) by A3
.= P1 . 0 by MEMSTR_0:def 11
.= (stop I) . 0 by A1, A8, GRFUNC_1:2 ;
A11: P1 = P1 +* (stop I) by A1, FUNCT_4:98;
A12: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A13: S₁[k] ; :: thesis:
reconsider m = IC (Comput (P1,s1,k)) as Nat ;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A14: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Nat ;
A15: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A2, A11, A3;
then A16: l + n in dom (Shift ((stop I),n)) by VALUED_1:24;
A17: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3;
A18: IC (Comput (P1,s1,k)) in dom (stop I) by A2, A11, A3;
A19: P1 /. (IC (Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143;
A20: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by A19
.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A18, GRFUNC_1:2 ;
then A21: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by A18, SCMPDS_4:def 9;
A22: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A18, A20, SCMPDS_4:def 9;
hence A23: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A13, A14, A17, A21, SCMPDS_4:28; :: thesis:
A24: P1 /. (IC (Comput (P1,s1,(k + 1)))) = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:143;
A25: 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 A24
.= (stop I) . l by A1, A15, 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 A23, A15, VALUED_1:def 12
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A4, A23, A16, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by A25 ;
:: thesis:
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A13, A14, A17, A21, A22, SCMPDS_4:28; :: thesis:

end;

A26: IC (Comput (P1,s1,0)) = IC s1 by EXTPRO_1:2
.= IC (Initialize s1) by A3
.= 0 by MEMSTR_0:def 11 ;
A27: Comput (P1,s1,0) = s1 by EXTPRO_1:2;
A28: Comput (P2,s2,0) = s2 by EXTPRO_1:2;
A29: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A30: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by A27
.= (Shift ((stop I),n)) . (0 + n) by A8, A10, A30, VALUED_1:def 12
.= CurInstr (P2,s2) by A4, A5, A9, A29, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,0))) by A28 ;
then A31: S₁[ 0 ] by A5, A26, A7, EXTPRO_1:2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A31, A12);
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: