let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ;
A4: IC (Comput (P2,s,k)) in dom (stop I) by ;
for m being Nat st m < k holds
IC (Comput (P2,s,m)) in dom (stop I) by ;
hence A5: Comput (P1,s,k) = Comput (P2,s,k) by ; :: 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
.= P1 . (IC (Comput (P1,s,k))) by
.= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; :: thesis: verum