let P1, P2 be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let s be State of SCM+FSA; for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let I be really-closed InitHalting Program of SCM+FSA; ( Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 implies for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) )
assume that
A1:
Initialize ((intloc 0) .--> 1) c= s
and
A2:
I c= P1
and
A3:
I c= P2
; for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
let k be Nat; ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
IC s = 0
by A1, MEMSTR_0:47;
then A4:
IC s in dom I
by AFINSQ_1:65;
then A5:
IC (Comput (P1,s,k)) in dom I
by A2, AMISTD_1:21;
A6:
IC (Comput (P2,s,k)) in dom I
by A3, AMISTD_1:21, A4;
for m being Nat st m < k holds
IC (Comput (P2,s,m)) in dom I
by A3, A4, AMISTD_1:21;
hence
Comput (P1,s,k) = Comput (P2,s,k)
by A2, A3, AMISTD_2:10; CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k)))
then A7:
IC (Comput (P1,s,k)) = IC (Comput (P2,s,k))
;
thus CurInstr (P2,(Comput (P2,s,k))) =
P2 . (IC (Comput (P2,s,k)))
by PBOOLE:143
.=
I . (IC (Comput (P2,s,k)))
by A6, A3, GRFUNC_1:2
.=
P1 . (IC (Comput (P1,s,k)))
by A7, A5, A2, GRFUNC_1:2
.=
CurInstr (P1,(Comput (P1,s,k)))
by PBOOLE:143
; verum