:: A Tree of Execution of a Macroinstruction
::  by Artur Korni{\l}owicz
::
:: Received December 10, 2003
:: Copyright (c) 2003-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, RELAT_1, FUNCOP_1, FUNCT_1, CARD_1, WELLORD2,
      XBOOLE_0, TARSKI, SUBSET_1, ZFMISC_1, WELLORD1, ORDINAL2, FINSEQ_2,
      FINSEQ_1, TREES_1, TREES_2, NAT_1, XXREAL_0, ARYTM_3, ORDINAL4, GOBOARD5,
      AMI_1, AMISTD_1, GLIB_000, AMISTD_2, AMISTD_3, PARTFUN1, EXTPRO_1,
      QUANTAL1, MEMSTR_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, ORDINAL2,
      NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      BINOP_1, WELLORD1, WELLORD2, FUNCOP_1, FINSEQ_1, FINSEQ_2, TREES_1,
      TREES_2, VALUED_1, MEASURE6, STRUCT_0, MEMSTR_0, COMPOS_1, EXTPRO_1,
      AMISTD_1;
 constructors WELLORD2, BINOP_1, AMISTD_2, RELSET_1, TREES_2, PRE_POLY,
      AMISTD_1, FUNCOP_1, DOMAIN_1, NUMBERS, TREES_3;
 registrations RELAT_1, ORDINAL1, FUNCOP_1, XXREAL_0, CARD_1, MEMBERED,
      FINSEQ_1, TREES_2, FINSEQ_6, VALUED_0, FINSEQ_2, CARD_5, TREES_1,
      AMISTD_2, COMPOS_1, EXTPRO_1, MEASURE6;
 requirements BOOLE, SUBSET, NUMERALS;


begin

reserve x, y, z, X for set,
  m, n for Nat,
  O for Ordinal,
  R, S for Relation;

reserve
  N for with_zero set,
  S for
  standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
  L, l1 for Nat,
  J for Instruction of S,
  F for Subset of NAT;

:: LocSeq

definition
  let N be with_zero set,
  S be standard IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N, M be Subset of NAT;
  func LocSeq(M,S) -> Sequence of NAT means
:: AMISTD_3:def 1

  dom it = card M & for m
being set st m in card M holds it.m = (canonical_isomorphism_of (RelIncl
  order_type_of RelIncl M, RelIncl M).m);
end;

theorem :: AMISTD_3:1
  F = {n} implies LocSeq(F,S) = 0 .--> n;

registration
  let N be with_zero set,
  S be standard IC-Ins-separated
 non empty with_non-empty_values AMI-Struct over N, M be Subset of NAT;
  cluster LocSeq(M,S) -> one-to-one;
end;

:: Tree of Execution

definition  let N be with_zero set,
  S be standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N,
  M be non empty preProgram of S;
  func ExecTree(M) -> DecoratedTree of NAT means
:: AMISTD_3:def 2

  it.{} = FirstLoc(M) &
  for t being Element of dom it holds
  succ t = { t^<*k*> where k is Nat: k in card NIC(M/.(it.t),it.t) }
   & for m being Nat st m in card
  NIC(M/.(it.t),it.t) holds it.(t^<*m*>) = (LocSeq(NIC(M/.(it.t),it.t),S)).m;
end;

theorem :: AMISTD_3:2
  for S being standard halting IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N holds ExecTree Stop S =
  TrivialInfiniteTree --> 0;