let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),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),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) )
set D = Data-Locations SCM+FSA;
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),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),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),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ) )
set ss2 = s2 +* (Initialize I);
set PP2 = P2 +* I;
set ss1 = s1 +* (Initialize I);
set PP1 = P1 +* I;
A2: I c= P1 +* I by FUNCT_4:26;
A3: I c= P2 +* I by FUNCT_4:26;
A4: ProgramPart I = I by RELAT_1:209;
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),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ) )
assume A6: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds
( Comput ((P1 +* I),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) )
let k be Element of NAT ; :: thesis: ( Comput ((P1 +* I),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) )
A7: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) in dom I by A1, SCMFSA7B:def 7, A4;
I is_closed_on s2,P2 by A1, A5, A6, SCMFSA8B:8;
then A8: for m being Element of NAT st m < k holds
IC (Comput ((P2 +* I),(s2 +* (Initialize I)),m)) in dom I by SCMFSA7B:def 7, A4;
s1 +* (Initialize I),s2 +* (Initialize I) equal_outside NAT by A6, SCMFSA8B:7;
hence Comput ((P1 +* I),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT by A8, AMISTD_2:66, A2, A3; :: thesis: CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k)))
then A9: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) by COMPOS_1:24;
I is_closed_on s2,P2 by A1, A5, A6, SCMFSA8B:8;
then A10: IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I by SCMFSA7B:def 7, A4;
A11: (P2 +* I) /. (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k))) by PBOOLE:158;
A12: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by PBOOLE:158;
thus CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k))) by A11
.= I . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k))) by A10, GRFUNC_1:8, A3
.= (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by A9, A7, GRFUNC_1:8, A2
.= CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by A12 ; :: thesis: verum