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 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; :: 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, 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 ; :: thesis: verum

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 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; :: 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, 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 ; :: thesis: verum