let P1, P2 be Instruction-Sequence of SCM+FSA; for s1, s2 being 0 -started State of SCM+FSA
for I being really-closed Program of SCM+FSA st I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let s1, s2 be 0 -started State of SCM+FSA; for I being really-closed Program of SCM+FSA st I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let J be really-closed Program of SCM+FSA; ( J c= P1 & J c= P2 & DataPart s1 = DataPart s2 implies for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
assume that
A1:
J c= P1
and
A2:
J c= P2
and
A3:
DataPart s1 = DataPart s2
; for i being Nat holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A4:
Start-At (0,SCM+FSA) c= s2
by MEMSTR_0:29;
A5:
Reloc (J,0) = J
;
let i be Nat; ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A6:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
A7:
(IC (Comput (P1,s1,i))) + 0 = IC (Comput (P1,s1,i))
;
A8: IC s2 =
IC (Initialize s2)
by A4, FUNCT_4:98
.=
IC (Start-At (0,SCM+FSA))
by A6, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),0) = CurInstr (P1,(Comput (P1,s1,i)))
by COMPOS_0:3;
hence
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
by A3, A7, A8, Th8, A1, A2, A5; verum