let P1, P2 be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being parahalting Program of st stop I c= P1 & stop I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let s be 0 -started State of SCMPDS; for I being parahalting Program of st stop I c= P1 & stop I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let I be parahalting Program of ; ( stop I c= P1 & stop I c= P2 implies for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )
set SI = stop I;
assume that
A1:
stop I c= P1
and
A2:
stop I c= P2
; for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let k be Nat; ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
A3:
IC (Comput (P1,s,k)) in dom (stop I)
by A1, SCMPDS_4:def 6;
A4:
IC (Comput (P2,s,k)) in dom (stop I)
by A2, SCMPDS_4:def 6;
for m being Nat st m < k holds
IC (Comput (P2,s,m)) in dom (stop I)
by A2, SCMPDS_4:def 6;
hence A5:
Comput (P1,s,k) = Comput (P2,s,k)
by A1, A2, SCMPDS_4:21; CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k)))
thus CurInstr (P2,(Comput (P2,s,k))) =
P2 . (IC (Comput (P2,s,k)))
by PBOOLE:143
.=
(stop I) . (IC (Comput (P2,s,k)))
by A2, A4, GRFUNC_1:2
.=
P1 . (IC (Comput (P1,s,k)))
by A1, A5, A3, GRFUNC_1:2
.=
CurInstr (P1,(Comput (P1,s,k)))
by PBOOLE:143
; verum