AMISTD_3: A Tree of Execution of a Macroinstruction

:: A Tree of Execution of a Macroinstruction
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions RELAT_1, TARSKI, XBOOLE_0, FUNCT_1;
theorems AMISTD_1, NAT_1, ORDINAL1, CARD_1, TREES_2, TREES_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_3, FINSEQ_5, TARSKI, CARD_5, FINSEQ_2, FUNCOP_1, XXREAL_0, PARTFUN1, TREES_9, VALUED_1;
schemes TREES_2, NAT_1, HILBERT2, ORDINAL2, BINOP_1;
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, XCMPLX_0, NAT_1;
constructors HIDDEN, WELLORD2, BINOP_1, AMISTD_2, RELSET_1, TREES_2, PRE_POLY, AMISTD_1, FUNCOP_1, DOMAIN_1, NUMBERS, TREES_3;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities FINSEQ_2, FUNCOP_1, AFINSQ_1, COMPOS_1, CARD_1, ORDINAL1;
expansions TARSKI, FUNCT_1;

:: LocSeq

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;
let M be Subset of NAT;
deffunc H₁( object ) -> set = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . $1;

func LocSeq (M,S) -> Sequence of NAT means :Def1: :: 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 ) );

proof end;

proof end;

end;

:: deftheorem Def1 defines LocSeq AMISTD_3:def 1 :

theorem :: AMISTD_3:1

for n being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n

proof end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;
let M be Subset of NAT;

cluster LocSeq (M,S) -> one-to-one ;

proof end;

end;

:: Tree of Execution

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;
let M be non empty preProgram of S;

func ExecTree M -> DecoratedTree of NAT means :Def2: :: 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 ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def2 defines ExecTree AMISTD_3:def 2 :

theorem :: AMISTD_3:2

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0

proof end;