let P1, P2 be Instruction-Sequence of SCM+FSA; for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
for k being Element of 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 0 -started State of SCM+FSA; for I being parahalting Program of st I c= P1 & I c= P2 holds
for k being Element of 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 parahalting Program of ; ( I c= P1 & I c= P2 implies for k being Element of 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:
I c= P1
and
A2:
I c= P2
; for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
hereby verum
let k be
Element of
NAT ;
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P2,(Comput (P2,s,k))) = CurInstr (P1,(Comput (P1,s,k))) )A6:
IC (Comput (P1,s,k)) in dom I
by A1, AMISTD_1:def 10;
A7:
IC (Comput (P2,s,k)) in dom I
by A2, AMISTD_1:def 10;
for
m being
Element of
NAT st
m < k holds
IC (Comput (P2,s,m)) in dom I
by A2, AMISTD_1:def 10;
hence A8:
Comput (
P1,
s,
k)
= Comput (
P2,
s,
k)
by A1, A2, AMISTD_2:10;
CurInstr (P2,(Comput (P2,s,k))) = CurInstr (P1,(Comput (P1,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 A7, A2, GRFUNC_1:2
.=
P1 . (IC (Comput (P1,s,k)))
by A8, A6, A1, GRFUNC_1:2
.=
CurInstr (
P1,
(Comput (P1,s,k)))
by PBOOLE:143
;
verum
end;