The abstract of the Mizar article:

A Tree of Execution of a Macroinstruction

by

Artur Kornilowicz

Received December 10, 2003

MML identifier: AMISTD_3

[ Mizar article, MML identifier index ]

environ

 vocabulary AMISTD_3, AMI_1, TREES_2, GOBOARD5, AMI_3, RELAT_1, FINSET_1,
      FUNCT_1, AMISTD_1, SQUARE_1, WAYBEL_0, BOOLE, ORDINAL1, FINSEQ_1, CARD_1,
      CARD_3, ORDINAL2, ARYTM, PARTFUN1, TREES_1, TARSKI, WELLORD1, WELLORD2,
      AMISTD_2, FRECHET, FINSEQ_2, CAT_1, FUNCOP_1, MEMBERED;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1, NUMBERS,
      ORDINAL1, ORDINAL2, MEMBERED, XREAL_0, CQC_SIM1, NAT_1, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, WELLORD1, WELLORD2, FUNCOP_1, CQC_LANG, FINSEQ_1,
      FINSEQ_2, TREES_1, TREES_2, STRUCT_0, AMI_1, AMI_3, AMI_5, AMISTD_1,
      AMISTD_2;
 constructors AMISTD_2, CQC_SIM1, WELLORD1, ORDERS_2, AMI_5, PRE_CIRC,
      POLYNOM1, WELLORD2;
 clusters AMI_1, AMISTD_1, FINSET_1, RELSET_1, TREES_2, ARYTM_3, FINSEQ_6,
      FUNCT_7, HEYTING2, NECKLACE, CARD_5, WAYBEL12, RELAT_1, FUNCOP_1,
      FINSEQ_5, SCMFSA_4, XREAL_0, CARD_1, ORDINAL1, MEMBERED, FINSEQ_1,
      PRELAMB;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin

:: Preliminaries

reserve x, y, X for set,
        m, n for natural number,
        O for Ordinal,
        R, S for Relation;

definition
  let D be set, f be PartFunc of D,NAT, n be set;
  cluster f.n -> natural;
end;

definition
  let R be empty Relation, X be set;
  cluster R|X -> empty;
end;

theorem :: AMISTD_3:1
  dom R = {x} & rng R = {y} implies R = x .--> y;

theorem :: AMISTD_3:2
  field {[x,x]} = {x};

definition
  let X be infinite set, a be set;
  cluster X --> a -> infinite;
end;

definition
  cluster infinite Function;
end;

definition
  let R be finite Relation;
  cluster field R -> finite;
end;

theorem :: AMISTD_3:3
  field R is finite implies R is finite;

definition
  let R be infinite Relation;
  cluster field R -> infinite;
end;

theorem :: AMISTD_3:4
  dom R is finite & rng R is finite implies R is finite;

definition
  cluster RelIncl {} -> empty;
end;

definition
  let X be non empty set;
  cluster RelIncl X -> non empty;
end;

theorem :: AMISTD_3:5
  RelIncl {x} = {[x,x]};

theorem :: AMISTD_3:6
  RelIncl X c= [:X,X:];

definition
  let X be finite set;
  cluster RelIncl X -> finite;
end;

theorem :: AMISTD_3:7
  RelIncl X is finite implies X is finite;

definition
  let X be infinite set;
  cluster RelIncl X -> infinite;
end;

theorem :: AMISTD_3:8
  R,S are_isomorphic & R is well-ordering implies S is well-ordering;

theorem :: AMISTD_3:9
  R,S are_isomorphic & R is finite implies S is finite;

theorem :: AMISTD_3:10
  x .--> y is_isomorphism_of {[x,x]},{[y,y]};

theorem :: AMISTD_3:11
  {[x,x]}, {[y,y]} are_isomorphic;

definition
  cluster order_type_of {} -> empty;
end;

theorem :: AMISTD_3:12
  order_type_of RelIncl O = O;

theorem :: AMISTD_3:13
  for X being finite set st X c= O holds order_type_of RelIncl X = card X;

theorem :: AMISTD_3:14
  {x} c= O implies order_type_of RelIncl {x} = 1;

theorem :: AMISTD_3:15
  {x} c= O implies
  canonical_isomorphism_of (RelIncl order_type_of RelIncl {x}, RelIncl {x})
    = 0 .--> x;

definition
  let O be Ordinal,
      X be Subset of O,
      n be set;
  cluster canonical_isomorphism_of
              (RelIncl order_type_of RelIncl X,RelIncl X).n
          -> ordinal;
end;

definition
  let X be natural-membered set,
      n be set;
  cluster canonical_isomorphism_of
              (RelIncl order_type_of RelIncl X,RelIncl X).n
          -> natural;
end;

:: Trees

theorem :: AMISTD_3:16
  n |-> x = m |-> x implies n = m;

theorem :: AMISTD_3:17
  for T being Tree, t being Element of T holds t|Seg n in T;

theorem :: AMISTD_3:18
  for T1, T2 being Tree st
    for n being Nat holds T1-level n = T2-level n holds
  T1 = T2;

definition
  func TrivialInfiniteTree equals
:: AMISTD_3:def 1
  { k |-> 0 where k is Nat: not contradiction };
end;

definition
  cluster TrivialInfiniteTree -> non empty Tree-like;
end;

theorem :: AMISTD_3:19
  NAT,TrivialInfiniteTree are_equipotent;

definition
  cluster TrivialInfiniteTree -> infinite;
end;

theorem :: AMISTD_3:20
  for n being Nat holds TrivialInfiniteTree-level n = { n |-> 0 };

:: First Location

reserve
  N for with_non-empty_elements set,
  S for standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over N)),
  L, l1 for Instruction-Location of S,
  J for Instruction of S,
  F for Subset of the Instruction-Locations of S;

definition
  let N be with_non-empty_elements set;
  let S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N));
  let F be FinPartState of S such that
   F is non empty and
   F is programmed;
  func FirstLoc F -> Instruction-Location of S means
:: AMISTD_3:def 2
  ex M being non empty Subset of NAT st
     M = { locnum l where l is Element of the Instruction-Locations of S
                        : l in dom F } &
     it = il.(S, min M);
end;

theorem :: AMISTD_3:21
  for F being non empty programmed FinPartState of S holds
   FirstLoc F in dom F;

theorem :: AMISTD_3:22
  for F, G being non empty programmed FinPartState of S st F c= G holds
   FirstLoc G <= FirstLoc F;

theorem :: AMISTD_3:23
  for F being non empty programmed FinPartState of S st l1 in dom F holds
   FirstLoc F <= l1;

theorem :: AMISTD_3:24
  for F being lower non empty programmed FinPartState of S holds
   FirstLoc F = il.(S,0);

:: LocNums

definition
 let N be with_non-empty_elements set,
     S be standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over N)),
    F be Subset of the Instruction-Locations of S;
 func LocNums F -> Subset of NAT equals
:: AMISTD_3:def 3
  {locnum l where l is Instruction-Location of S : l in F};
end;

theorem :: AMISTD_3:25
  locnum l1 in LocNums F iff l1 in F;

definition
 let N be with_non-empty_elements set,
     S be standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over N)),
     F be empty Subset of the Instruction-Locations of S;
 cluster LocNums F -> empty;
end;

definition
 let N be with_non-empty_elements set,
     S be standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over N)),
     F be non empty Subset of the Instruction-Locations of S;
 cluster LocNums F -> non empty;
end;

theorem :: AMISTD_3:26
  F = {il.(S,n)} implies LocNums F = {n};

theorem :: AMISTD_3:27
  F, LocNums F are_equipotent;

theorem :: AMISTD_3:28
  Card F c= order_type_of RelIncl LocNums F;

theorem :: AMISTD_3:29
  S is realistic & J is halting implies LocNums NIC(J,L) = {locnum L};

theorem :: AMISTD_3:30
  S is realistic & J is sequential implies
   LocNums NIC(J,L) = {locnum NextLoc L};

:: LocSeq

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be Subset of the Instruction-Locations of S;
  func LocSeq M -> T-Sequence of the Instruction-Locations of S means
:: AMISTD_3:def 4
   dom it = Card M &
   for m being set st m in Card M holds
    it.m = il.(S, canonical_isomorphism_of
                  (RelIncl order_type_of RelIncl LocNums M,
                   RelIncl LocNums M).m);
end;

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

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be Subset of the Instruction-Locations of S;
  cluster LocSeq M -> one-to-one;
end;

:: Tree of Execution

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be FinPartState of S;
  func ExecTree(M) -> DecoratedTree of the Instruction-Locations of S means
:: AMISTD_3:def 5

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

theorem :: AMISTD_3:32
  for S being standard halting realistic
        (IC-Ins-separated definite (non empty non void AMI-Struct over N))
  holds
  ExecTree Stop S = TrivialInfiniteTree --> il.(S,0);