:: On the Composition of Macro Instructions of Standard Computers
::  by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-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, ORDINAL1, SETFAM_1, ARYTM_1, ARYTM_3, CARD_1, SUBSET_1,
      AMI_1, XBOOLE_0, RELAT_1, TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1,
      FUNCT_1, CARD_3, FRECHET, STRUCT_0, FSM_1, FUNCT_4, TURING_1, CIRCUIT2,
      AMISTD_2, PARTFUN1, EXTPRO_1, NAT_1, RELOC, XXREAL_0, COMPOS_1, QUANTAL1,
      GOBRD13, MEMSTR_0;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED,
      RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, CARD_1, NUMBERS,
      XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D, FUNCT_7,
      VALUED_0, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1,
      MEASURE6, EXTPRO_1, AMISTD_1;
 constructors WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY,
      AFINSQ_1, ORDINAL4, VALUED_1, NAT_1, FUNCT_7, PBOOLE, FUNCT_4, MEMSTR_0,
      RELSET_1, MEASURE6, XTUPLE_0;
 registrations RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED,
      CARD_3, STRUCT_0, AMISTD_1, FUNCT_4, EXTPRO_1, MEMSTR_0, MEASURE6,
      COMPOS_0, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin  :: Properties of AMI-Struct

reserve k, m for Nat,
  x, x1, x2, x3, y, y1, y2, y3, X,Y,Z for set,
  N for with_zero set;

theorem :: AMISTD_2:1
  for I being Instruction of STC N holds JumpPart I = 0;

definition
  let N be with_zero set,
  S be IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, I be Instruction of S;
  attr I is with_explicit_jumps means
:: AMISTD_2:def 1
 JUMP I = rng JumpPart I;
end;

definition
  let N be with_zero set,
  S be IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
  attr S is with_explicit_jumps means
:: AMISTD_2:def 2
 for I being Instruction of S holds I is with_explicit_jumps;

end;

registration
  let N be with_zero set;
  cluster standard for IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N;
end;

theorem :: AMISTD_2:2
  for S being standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, I being Instruction of S
  st for f being Element of NAT holds NIC(I,f)={f+1}
  holds JUMP I is empty;

registration
  let N be with_zero set,
  I be Instruction of STC N;
  cluster JUMP I -> empty;
end;

theorem :: AMISTD_2:3
  for T being InsType of the InstructionsF of STC N holds JumpParts T = {0};

registration
  let N be with_zero set;
  cluster STC N -> with_explicit_jumps;
end;

registration
  let N be with_zero set;
  cluster standard
   halting with_explicit_jumps for IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N;
end;

registration
  let N be with_zero set,
  I be Instruction of Trivial-AMI N;
  cluster JUMP I -> empty;
end;

registration
  let N be with_zero set;
  cluster Trivial-AMI N -> with_explicit_jumps;
end;

registration
  let N be with_zero set;
  cluster with_explicit_jumps halting
    for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
end;

registration
  let N be with_zero set;
  let S be with_explicit_jumps IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
  cluster -> with_explicit_jumps for Instruction of S;
end;

theorem :: AMISTD_2:4
  for S being IC-Ins-separated non empty with_non-empty_values
  AMI-Struct over N,
  I being Instruction of S st I is halting holds JUMP I is empty;

registration

  let N be with_zero set,
  S be halting
  IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
  I be halting Instruction of S;
  cluster JUMP I -> empty;
end;

theorem :: AMISTD_2:5
  for S being halting with_explicit_jumps
  IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N,
  I being Instruction of S st I is ins-loc-free holds JUMP I is empty;

registration
  let N be with_zero set,
  S be with_explicit_jumps
   IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
  cluster halting -> ins-loc-free for Instruction of S;
end;

registration
  let N be with_zero set,
  S be with_explicit_jumps
    IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
  cluster sequential -> ins-loc-free for Instruction of S;
end;

begin  :: On the composition of macro instructions

registration
  let N be with_zero set,
  S be halting with_explicit_jumps IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N,
  I be halting Instruction of S, k be Nat;
  cluster IncAddr(I,k) -> halting;
end;

theorem :: AMISTD_2:6
  for S being standard halting
  with_explicit_jumps IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N,
  I being Instruction of S st I is sequential
  holds IncAddr(I,k) is sequential;

definition

  let N be with_zero set,
  S be halting
   IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
   I be Instruction of S;
  attr I is IC-relocable means
:: AMISTD_2:def 3

  for j,k being Nat, s being State of S
  holds IC Exec(IncAddr(I,j),s) + k = IC Exec(IncAddr(I,j+k),IncIC(s,k));
end;

definition
  let N be with_zero set,
  S be halting IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N;
  attr S is IC-relocable means
:: AMISTD_2:def 4

  for I being Instruction of S holds I is IC-relocable;
end;

registration
  let N be with_zero set,
  S be with_explicit_jumps IC-Ins-separated halting
  non empty with_non-empty_values AMI-Struct over N;
  cluster sequential -> IC-relocable for Instruction of S;
end;

registration
  let N be with_zero set,
  S be with_explicit_jumps IC-Ins-separated halting
  non empty with_non-empty_values AMI-Struct over N;
  cluster halting -> IC-relocable for Instruction of S;
end;

registration
  let N be with_zero set;
  cluster STC N -> IC-relocable;
end;

registration
  let N be with_zero set;
  cluster halting with_explicit_jumps
    for standard IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N;
end;

registration
  let N be with_zero set;
  cluster IC-relocable for
    with_explicit_jumps halting
    standard IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N;
end;

registration
  let N be with_zero set,
  S be IC-relocable IC-Ins-separated halting
  non empty with_non-empty_values AMI-Struct over N;
  cluster -> IC-relocable for Instruction of S;
end;

registration
  let N be with_zero set,
  S be with_explicit_jumps IC-Ins-separated halting
  non empty with_non-empty_values AMI-Struct over N;
 cluster IC-relocable for Instruction of S;
end;

theorem :: AMISTD_2:7
  for S be halting
  with_explicit_jumps
   IC-Ins-separated non empty with_non-empty_values
   AMI-Struct over N,
  I being IC-relocable Instruction of S
  for k being Nat, s being State of S
  holds IC Exec(I,s) + k = IC Exec(IncAddr(I,k),IncIC(s,k));

registration
  let N be with_zero set,
  S be IC-relocable standard with_explicit_jumps
  halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
  F, G be really-closed Program of S;
  cluster F ';' G -> really-closed;
end;

theorem :: AMISTD_2:8
  for I being Instruction of Trivial-AMI N holds JumpPart I = 0;

theorem :: AMISTD_2:9
  for T being InsType of the InstructionsF of Trivial-AMI N
    holds JumpParts T = {0};

reserve n,m for Nat;

theorem :: AMISTD_2:10
 for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
 for s being State of S, I being Program of S
 for P1,P2 being Instruction-Sequence of S
  st I c= P1 & I c= P2 &
     for m st m < n holds IC Comput(P2,s,m) in dom I
 for m st m <= n holds Comput(P1,s,m) =  Comput(P2,s,m);

theorem :: AMISTD_2:11
 for S being IC-Ins-separated halting non empty with_non-empty_values
  AMI-Struct over N,
  P being Instruction-Sequence of S,
  s being State of S st  s =  Following(P,s)
  holds for n holds Comput(P,s,n) =  s;