let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Nat holds
( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
let s1, s2 be State of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Nat holds
( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
set D = Data-Locations ;
let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies for k being Nat holds
( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) ) )
set ss2 = Initialize s2;
set PP2 = P2 +* I;
set ss1 = Initialize s1;
set PP1 = P1 +* I;
A1: I c= P1 +* I by FUNCT_4:25;
A2: I c= P2 +* I by FUNCT_4:25;
assume I is_halting_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Nat holds
( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) ) )
assume A3: DataPart s1 = DataPart s2 ; :: thesis: for k being Nat holds
( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
let k be Nat; :: thesis: ( Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
IC (Initialize s1) = 0 by MEMSTR_0:def 11;
then IC (Initialize s1) in dom I by AFINSQ_1:65;
then A4: IC (Comput ((P1 +* I),(Initialize s1),k)) in dom I by A1, AMISTD_1:21;
IC (Initialize s2) = 0 by MEMSTR_0:def 11;
then A5: IC (Initialize s2) in dom I by AFINSQ_1:65;
then A6: for m being Nat st m < k holds
IC (Comput ((P2 +* I),(Initialize s2),m)) in dom I by AMISTD_1:21, A2;
Initialize s1 = Initialize s2 by A3, MEMSTR_0:80;
hence Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) by A6, A1, A2, AMISTD_2:10; :: thesis: CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k)))
then A7: IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) ;
A8: IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I by AMISTD_1:21, A5, A2;
thus CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),k))) by PBOOLE:143
.= I . (IC (Comput ((P2 +* I),(Initialize s2),k))) by A8, A2, GRFUNC_1:2
.= (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),k))) by A7, A4, A1, GRFUNC_1:2
.= CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) by PBOOLE:143 ; :: thesis: verum