:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received February 22, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

theorem Th1: :: SCMFSA_5:1

for k being Nat

for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function

for p being non empty b_{2} -autonomic FinPartState of SCM+FSA

for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )

for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function

for p being non empty b

for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )

proof end;