:: On the compositions of macro instructions, Part II
::  by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, AMI_1, SCMFSA_2, FSM_1, CARD_1, TARSKI,
      SCMFSA6A, FUNCT_4, RELAT_1, XBOOLE_0, FUNCT_1, MSUALG_1, CIRCUIT2, AMI_3,
      ARYTM_3, XXREAL_0, NAT_1, SF_MASTR, GRAPHSP, AMISTD_2, STRUCT_0,
      VALUED_1, FUNCOP_1, SCMFSA6B, PARTFUN1, EXTPRO_1, RELOC, SCMFSA6C,
      COMPOS_1, AMISTD_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XXREAL_0, NAT_1, FUNCT_7, INT_1, RELAT_1, FUNCT_1, PARTFUN1,
      AFINSQ_1, PBOOLE, FINSEQ_1, FUNCOP_1, FUNCT_4, VALUED_1, STRUCT_0,
      MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, SCMFSA_2, AMISTD_1, AMISTD_2,
      SCMFSA6A, SF_MASTR, SCMFSA_M;
 constructors XXREAL_0, SCMFSA6A, SF_MASTR, AMISTD_1, AMISTD_2, MEMSTR_0,
      RELSET_1, PRE_POLY, AMISTD_5, DOMAIN_1, PBOOLE, AMI_3, FUNCT_7, SCMFSA_1,
      SCMFSA_M;
 registrations ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, COMPOS_1,
      EXTPRO_1, SCMFSA_4, PRE_POLY, FUNCT_7, FUNCT_4, STRUCT_0, MEMSTR_0,
      AMI_3, COMPOS_0, SCMFSA_M, AMISTD_1, AFINSQ_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin ::  General theory

reserve m, n for Nat,
  x for set,
  i for Instruction of SCM+FSA,
  I for Program of SCM+FSA,
  a for Int-Location,
  f for FinSeq-Location,
  l, l1 for Nat,
  s,s1,s2 for State of SCM+FSA,
  P,P1,P2 for Instruction-Sequence of SCM+FSA;

definition
  let I be Program of SCM+FSA, s be State of SCM+FSA;
  let P be Instruction-Sequence of SCM+FSA;
  func IExec(I,P,s) -> State of SCM+FSA equals
:: SCMFSA6B:def 1
  Result(P+*I,Initialized s);
end;

definition
  let I be Program of SCM+FSA;
::$CD 2
  attr I is keeping_0 means
:: SCMFSA6B:def 4

  for s being 0-started State of SCM+FSA
  for P being Instruction-Sequence of SCM+FSA st I c= P
  for k being Nat holds Comput(P,s,k).intloc 0 = s.intloc 0;
end;

registration
 cluster Stop SCM+FSA -> parahalting keeping_0;
end;

registration
  cluster really-closed parahalting keeping_0 for MacroInstruction of SCM+FSA;
end;

theorem :: SCMFSA6B:1
  for s being 0-started State of SCM+FSA
  for I being parahalting Program of SCM+FSA
  for P being Instruction-Sequence of SCM+FSA
   st I c= P
  holds P halts_on s;

theorem :: SCMFSA6B:2
  for s being State of SCM+FSA
  for I being parahalting Program of SCM+FSA
   st Initialize((intloc 0).-->1) c= s
  for P being Instruction-Sequence of SCM+FSA
   st I c= P
  holds P halts_on s;

theorem :: SCMFSA6B:3
  for I being really-closed parahalting Program of SCM+FSA,
      a being read-write Int-Location
  holds not a in UsedILoc I implies IExec(I,P,s).a = s.a;

theorem :: SCMFSA6B:4
  for I being parahalting really-closed Program of SCM+FSA
   holds not f in UsedI*Loc I implies (IExec(I,P,s)).f = s.f;

theorem :: SCMFSA6B:5
  IC s = l & P.l = goto l implies not P halts_on s;

registration
  cluster parahalting -> non empty for Program of SCM+FSA;
end;

theorem :: SCMFSA6B:6
 for s1 being 0-started State of SCM+FSA
 for P,Q being Instruction-Sequence of SCM+FSA
for J being parahalting really-closed Program of SCM+FSA st J c= P
 for n being Nat st Reloc(J,n) c= Q
  & IC s2 = n & DataPart s1 = DataPart s2
 for i being Nat holds
  IC Comput(P,s1,i) + n = IC Comput(Q,s2,i) &
  IncAddr(CurInstr(P,Comput(P,s1,i)),n) = CurInstr(Q,Comput(Q,s2,i)) &
  DataPart Comput(P,s1,i) = DataPart Comput(Q,s2,i);

theorem :: SCMFSA6B:7
  for s being 0-started State of SCM+FSA
  for I being parahalting really-closed Program of SCM+FSA st I c= P1 & 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));

theorem :: SCMFSA6B:8
  for s being 0-started State of SCM+FSA
  for I being parahalting really-closed Program of SCM+FSA
    st I c= P1 & I c= P2
  holds LifeSpan(P1,s) = LifeSpan(P2,s) & Result(P1,s) =  Result(P2,s);

::$CT 2

theorem :: SCMFSA6B:11
  for I being keeping_0 parahalting Program of SCM+FSA
   holds IExec(I,P,s).intloc 0 = 1;

begin :: The composition of macroinstructions

theorem :: SCMFSA6B:12
  for s being 0-started State of SCM+FSA
  for I being really-closed Program of SCM+FSA, J being Program of SCM+FSA
  for P being Instruction-Sequence of SCM+FSA
   st I c= P & P halts_on s
 for m st m <= LifeSpan(P,s)
  holds  Comput(P,s,m) =  Comput(P+*(I ";" J),s,m);

theorem :: SCMFSA6B:13
 for s being 0-started State of SCM+FSA
 for P being Instruction-Sequence of SCM+FSA
  for I being really-closed Program of SCM+FSA
   st P+*I halts_on s & Directed I c= P
 holds IC Comput(P,s,LifeSpan(P+*I,s) + 1) =  card I;

theorem :: SCMFSA6B:14
 for s being 0-started State of SCM+FSA
  for P being Instruction-Sequence of SCM+FSA
  for I being really-closed Program of SCM+FSA
   st P+*I halts_on s & Directed I c= P
 holds DataPart Comput(P,s,LifeSpan(P+*I,s))
   = DataPart Comput(P,s,LifeSpan(P+*I,s)+ 1);

theorem :: SCMFSA6B:15
  for I being parahalting really-closed Program of SCM+FSA st
   I c= P & Initialize((intloc 0).-->1) c= s
holds for k being Nat st k <= LifeSpan(P,s)
 holds CurInstr(P+*Directed I,
 Comput(P+*Directed I,s,k)) <> halt SCM+FSA;

theorem :: SCMFSA6B:16
 for s being 0-started State of SCM+FSA
 for P being Instruction-Sequence of SCM+FSA
 for I being really-closed Program of SCM+FSA st P+*I halts_on s
 for J being Program of SCM+FSA, k being Nat
     st k <= LifeSpan(P+*I,s)
   holds Comput(P+*I,s,k) = Comput(P+*(I ";" J), s,k);

registration
  let I, J be parahalting really-closed Program of SCM+FSA;
  cluster I ";" J -> parahalting;
end;

theorem :: SCMFSA6B:17
  for s being 0-started State of SCM+FSA
  for I being keeping_0 really-closed Program of SCM+FSA
   st not P+* I halts_on s
   for J being Program of SCM+FSA, k being Nat holds
    Comput(P+*I,s,k) =  Comput(P+*(I ";" J),s,k);

theorem :: SCMFSA6B:18
 for s being 0-started State of SCM+FSA
  for I being keeping_0 really-closed Program of SCM+FSA st P+*I halts_on s
for J being really-closed Program of SCM+FSA st I ";" J c= P
 for k being Element of NAT holds
   IncIC(Comput(P+*I+*J, Initialize Result(P+*I,s),k),card I)
  = Comput(P+*(I ";" J),s,(LifeSpan(P+*I,s)+1+k));

registration
  let I, J be keeping_0 really-closed Program of SCM+FSA;
  cluster I ";" J -> keeping_0;
end;

theorem :: SCMFSA6B:19
  for I being keeping_0 parahalting really-closed Program of SCM+FSA,
      J being parahalting really-closed Program of SCM+FSA holds
   LifeSpan(P+*(I ";" J),s +* Initialize((intloc 0).-->1)) =
  LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1 + LifeSpan(P+*I+*J,
   Result(P+*I,s +* Initialize((intloc 0).-->1)) +*
    Initialize((intloc 0).-->1));

theorem :: SCMFSA6B:20
  for I being keeping_0 parahalting really-closed Program of SCM+FSA,
      J being parahalting really-closed Program of SCM+FSA
 holds IExec(I ";" J,P,s) = IncIC(IExec(J,P,IExec(I,P,s)),card I);

theorem :: SCMFSA6B:21
 for P being Instruction-Sequence of SCM+FSA
   holds not P +*(IC s, goto IC s) halts_on s;