let s2 be State of SCMPDS; :: thesis: for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) )

let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1 being 0 -started State of SCMPDS
for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) )

let s1 be 0 -started State of SCMPDS; :: thesis: for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) )

let I be shiftable Program of ; :: thesis: ( stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) ) )

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: for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) )

A4: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:29;
let n be Nat; :: thesis: ( Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) ) )

assume that
A6: Shift (I,n) c= P2 and
A7: IC s2 = n and
A8: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat st i < LifeSpan (P1,s1) holds
( (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)) )

defpred S1[ 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)) ) );
A9: s1 = Initialize s1 by ;
A10: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 < LifeSpan (P1,s1) implies ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) ) )
reconsider m = IC (Comput (P1,s1,k)) as Nat ;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A12: k <= k + 1 by NAT_1:11;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Nat ;
A13: 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 A14: k + 1 < LifeSpan (P1,s1) ; :: thesis: ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
then A15: l + n in dom (Shift (I,n)) by ;
A16: 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))) ;
A17: P1 +* (stop I) = P1 by ;
then A18: IC (Comput (P1,s1,k)) in dom (stop I) by ;
A19: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,k))) by ;
then A20: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 by ;
A21: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by ;
A22: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by ;
A23: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 by ;
hence A24: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by ; :: thesis: ( CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . l by PBOOLE:143
.= (stop I) . l by ;
hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (l + n) by
.= (Shift (I,n)) . (IC (Comput (P2,s2,(k + 1)))) by
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;
:: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
let i be Nat; :: thesis: ( 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)) ) )
A25: 0 in dom (stop I) by COMPOS_1:36;
A26: 0 in dom I by AFINSQ_1:66;
A27: S1[ 0 ]
proof
assume 0 < LifeSpan (P1,s1) ; :: thesis: ( (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) & CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )
A28: 0 + n in dom (Shift (I,n)) by ;
A29: P1 . (IC s1) = P1 . 0 by MEMSTR_0:def 11
.= (stop I) . 0 by ;
IC (Comput (P1,s1,0)) = 0 by MEMSTR_0:def 11;
hence (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) by A7; :: thesis: ( CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )
A30: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A31: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
thus CurInstr (P1,(Comput (P1,s1,0))) = (Shift ((stop I),n)) . (0 + n) by
.= (Shift (I,n)) . n by COMPOS_1:66
.= CurInstr (P2,(Comput (P2,s2,0))) by ; :: thesis: DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0))
thus DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) by A8; :: thesis: verum
end;
for k being Nat holds S1[k] from 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: verum