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 and
A3: I is_halting_on s1,P1 ; :: thesis:
B1: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:29;
let n be Element of NAT ; :: thesis:
A7: card I > 0 ;
assume that
A6: Shift (I,n) c= P2 and
A8: IC s2 = n and
A9: DataPart s1 = DataPart s2 ; :: thesis:
defpred S₁[ Element of NAT ] means ( $1 < LifeSpan (P1,s1) implies ( (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)) ) );
A11: s1 = Initialize s1 by B1, FUNCT_4:98;
A12: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A13: S₁[k] ; :: thesis:

now

reconsider m = IC (Comput (P1,s1,k)) as Element of NAT ;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A14: k <= k + 1 by NAT_1:11;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Element of NAT ;
A16: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,k)))),(Comput (P1,s1,k))) ;
assume A17: k + 1 < LifeSpan (P1,s1) ; :: thesis:
then A19: l + n in dom (Shift (I,n)) by VALUED_1:24, A1, A2, A3, Th33;
A21: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,k)))),(Comput (P2,s2,k))) ;
XX: P1 +* (stop I) = P1 by A1, FUNCT_4:98;
then A22: IC (Comput (P1,s1,k)) in dom (stop I) by A2, A11, SCMPDS_6:def 2;
A24: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A22, GRFUNC_1:2 ;
then A25: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 by A22, SCMPDS_4:def 9;
A26: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A2, A11, XX, SCMPDS_6:def 2;
A27: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A22, A24, SCMPDS_4:def 9;
A28: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 by A22, A24, SCMPDS_4:def 9;
hence A29: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A13, A17, A14, A16, A21, A25, A27, SCMPDS_4:28, XXREAL_0:2; :: thesis:
CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . l by PBOOLE:143
.= (stop I) . l by A1, A26, GRFUNC_1:2 ;
hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (l + n) by A26, VALUED_1:def 12
.= (Shift (I,n)) . (IC (Comput (P2,s2,(k + 1)))) by A29, A17, A1, A2, A3, Th33, COMPOS_1:65
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A6, A29, A19, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;
:: thesis:
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A13, A17, A14, A16, A21, A28, A25, A27, SCMPDS_4:28, XXREAL_0:2; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

let i be Element of NAT ; :: thesis:
A32: 0 in dom (stop I) by COMPOS_1:36;
A33: 0 in dom I by A7, AFINSQ_1:66;
A34: S₁[ 0 ]

proof

assume 0 < LifeSpan (P1,s1) ; :: thesis:
A35: 0 + n in dom (Shift (I,n)) by A33, VALUED_1:24;
A37: P1 . (IC s1) = P1 . 0 by MEMSTR_0:def 8
.= (stop I) . 0 by A1, A32, GRFUNC_1:2 ;
IC (Comput (P1,s1,0)) = IC s1 by EXTPRO_1:2
.= 0 by MEMSTR_0:def 8 ;
hence (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) by A8, EXTPRO_1:2; :: thesis:
A40: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A41: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
thus CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by EXTPRO_1:2
.= (Shift ((stop I),n)) . (0 + n) by A32, A37, A40, VALUED_1:def 12
.= (Shift (I,n)) . n by COMPOS_1:66
.= CurInstr (P2,s2) by A6, A8, A35, A41, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,0))) by EXTPRO_1:2 ; :: thesis:
thus DataPart (Comput (P1,s1,0)) = DataPart s2 by A9, EXTPRO_1:2
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A34, A12);
hence ( i < LifeSpan (P1,s1) implies ( (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: