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 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)) );
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[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 A1, Def6;
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 A1, Def6;
A14: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A13, GRFUNC_1:2 ;
then A15: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by A13, Def9;
A16: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A13, A14, Def9;
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 A1, A10, GRFUNC_1:2 ;
hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (IC (Comput (P2,s2,(k + 1)))) by A17, A10, VALUED_1:def 12
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A2, A17, A11, GRFUNC_1:2
.= 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 A1, A5, GRFUNC_1:2 ;
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 A5, A18, A22, VALUED_1:def 12
.= CurInstr (P2,(Comput (P2,s2,0))) by A2, A3, A6, A21, GRFUNC_1:2 ;
then A23: S₁[ 0 ] by A3, A20, A19;
for k being Nat holds S₁[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