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

A5: 0 in dom (stop I) by COMPOS_1:36;
then A6: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:24;
defpred S1[ 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)) );
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
reconsider m = IC (Comput (P1,s1,k)) as Nat ;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A9: 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))) ;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Nat ;
A10: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by ;
then A11: l + n in dom (Shift ((stop I),n)) by VALUED_1:24;
A12: 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))) ;
A13: IC (Comput (P1,s1,k)) in dom (stop I) by ;
A14: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,k))) by ;
then A15: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by ;
A16: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by ;
hence A17: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, Th26; :: 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)) . (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 A8, A9, A12, A15, A16, Th26; :: thesis: verum
end;
A18: P1 . (IC s1) = P1 . 0 by MEMSTR_0:def 11
.= (stop I) . 0 by ;
let i be Nat; :: thesis: ( (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)) )
A19: DataPart (Comput (P1,s1,0)) = DataPart s2 by A4
.= DataPart (Comput (P2,s2,0)) ;
A20: IC (Comput (P1,s1,0)) = IC s1
.= 0 by MEMSTR_0:def 11 ;
A21: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A22: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1)
.= (Shift ((stop I),n)) . (0 + n) by
.= CurInstr (P2,(Comput (P2,s2,0))) by ;
then A23: S1[ 0 ] by A3, A20, A19;
for k being Nat holds S1[k] from NAT_1:sch 2(A23, A7);
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: verum