let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds
for k being Element of 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; :: thesis: for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds
for k being Element of 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 SCMPDS; :: thesis: ( stop I c= P1 & stop I c= P2 implies for k being Element of 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 ; :: thesis: for k being Element of 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 Element of NAT ; :: thesis: ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
A4: IC (Comput (P1,s,k)) in dom (stop I) by A1, SCMPDS_4:def 6;
A5: IC (Comput (P2,s,k)) in dom (stop I) by A2, SCMPDS_4:def 6;
for m being Element of NAT st m < k holds
IC (Comput (P2,s,m)) in dom (stop I) by A2, SCMPDS_4:def 6;
hence K: Comput (P1,s,k) = Comput (P2,s,k) by A1, A2, SCMPDS_4:21; :: thesis: 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, A5, GRFUNC_1:2
.= P1 . (IC (Comput (P1,s,k))) by A1, K, A4, GRFUNC_1:2
.= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; :: thesis: verum