let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

let s1, s2 be State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

let I be Program of ; :: thesis: ( I is_closed_on s1,P1 & DataPart s1 = DataPart s2 implies for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) ) )

assume A1: I is_closed_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) ) )

set pI = stop I;

set ss1 = Initialize s1;

set PP1 = P1 +* (stop I);

set ss2 = Initialize s2;

set PP2 = P2 +* (stop I);

A2: stop I c= P2 +* (stop I) by FUNCT_4:25;

A3: stop I c= P1 +* (stop I) by FUNCT_4:25;

assume A4: DataPart s1 = DataPart s2 ; :: thesis: for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

let k be Nat; :: thesis: ( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

A5: IC (Comput ((P1 +* (stop I)),(Initialize s1),k)) in dom (stop I) by A1, SCMPDS_6:def 2;

A6: I is_closed_on s2,P2 by A1, A4, SCMPDS_6:22;

then A7: for m being Nat st m < k holds

IC (Comput ((P2 +* (stop I)),(Initialize s2),m)) in dom (stop I) by SCMPDS_6:def 2;

Initialize s1 = Initialize s2 by A4, MEMSTR_0:80;

hence A8: Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) by A3, A2, A7, SCMPDS_4:21; :: thesis: CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k)))

A9: IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I) by A6, SCMPDS_6:def 2;

thus CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) = (P2 +* (stop I)) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by PBOOLE:143

.= (stop I) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by A2, A9, GRFUNC_1:2

.= (P1 +* (stop I)) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),k))) by A3, A8, A5, GRFUNC_1:2

.= CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) by PBOOLE:143 ; :: thesis: verum

for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

let s1, s2 be State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

let I be Program of ; :: thesis: ( I is_closed_on s1,P1 & DataPart s1 = DataPart s2 implies for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) ) )

assume A1: I is_closed_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) ) )

set pI = stop I;

set ss1 = Initialize s1;

set PP1 = P1 +* (stop I);

set ss2 = Initialize s2;

set PP2 = P2 +* (stop I);

A2: stop I c= P2 +* (stop I) by FUNCT_4:25;

A3: stop I c= P1 +* (stop I) by FUNCT_4:25;

assume A4: DataPart s1 = DataPart s2 ; :: thesis: for k being Nat holds

( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

let k be Nat; :: thesis: ( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )

A5: IC (Comput ((P1 +* (stop I)),(Initialize s1),k)) in dom (stop I) by A1, SCMPDS_6:def 2;

A6: I is_closed_on s2,P2 by A1, A4, SCMPDS_6:22;

then A7: for m being Nat st m < k holds

IC (Comput ((P2 +* (stop I)),(Initialize s2),m)) in dom (stop I) by SCMPDS_6:def 2;

Initialize s1 = Initialize s2 by A4, MEMSTR_0:80;

hence A8: Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) by A3, A2, A7, SCMPDS_4:21; :: thesis: CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k)))

A9: IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I) by A6, SCMPDS_6:def 2;

thus CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) = (P2 +* (stop I)) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by PBOOLE:143

.= (stop I) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by A2, A9, GRFUNC_1:2

.= (P1 +* (stop I)) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),k))) by A3, A8, A5, GRFUNC_1:2

.= CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) by PBOOLE:143 ; :: thesis: verum