let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Element of 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 Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Element of 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 Program of SCM+FSA; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies for k being Element of 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 A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not DataPart s1 = DataPart s2 or for k being Element of 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;
A2: I c= P1 +* I by FUNCT_4:25;
A3: I c= P2 +* I by FUNCT_4:25;
assume A5: I is_halting_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Element of 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 A6: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of 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 Element of 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))) )
A7: IC (Comput ((P1 +* I),(Initialize s1),k)) in dom I by A1, SCMFSA7B:def 6;
I is_closed_on s2,P2 by A1, A5, A6, SCMFSA8B:5;
then A8: for m being Element of NAT st m < k holds
IC (Comput ((P2 +* I),(Initialize s2),m)) in dom I by SCMFSA7B:def 6;
Initialize s1 = Initialize s2 by A6, SCMFSA8B:4;
hence Comput ((P1 +* I),(Initialize s1),k) = Comput ((P2 +* I),(Initialize s2),k) by A8, A2, A3, AMISTD_2:10; :: thesis: CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k)))
then A9: IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) ;
I is_closed_on s2,P2 by A1, A5, A6, SCMFSA8B:5;
then A10: IC (Comput ((P2 +* I),(Initialize s2),k)) in dom I by SCMFSA7B:def 6;
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 A10, A3, GRFUNC_1:2
.= (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),k))) by A9, A7, A2, GRFUNC_1:2
.= CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) by PBOOLE:143 ; :: thesis: verum