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


begin

:: 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 H1( set ) ->  set = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . $1;
func LocSeq (M,S) ->  T-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 ) );
existence
 ex b1 being T-Sequence of NAT st
( dom b1 = card M & ( for m being set st m in card M holds
b1 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) )
proofend;
uniqueness
 for b1, b2 being T-Sequence of NAT st dom b1 = card M & ( for m being set st m in card M holds
b1 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) & dom b2 = card M & ( for m being set st m in card M holds
b2 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines LocSeq AMISTD_3:def_1_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for M being Subset of NAT
for b4 being T-Sequence of NAT holds
( b4 = LocSeq (M,S) iff ( dom b4 = card M & ( for m being set st m in card M holds
b4 . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) ) );

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
proofend;

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 ;
coherence
 LocSeq (M,S) is one-to-one
proofend;
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 Element of NAT : k in card (NIC ((M /. (it . t)),(it . t)))  }  &amp; ( for m being Element of NAT st m in card (NIC ((M /. (it . t)),(it . t))) holds
it . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (it . t)),(it . t))),S)) . m ) ) ) );
existence
 ex b1 being DecoratedTree of NAT st
( b1 . {} = FirstLoc M &amp; ( for t being Element of dom b1 holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b1 . t)),(b1 . t)))  }  &amp; ( for m being Element of NAT st m in card (NIC ((M /. (b1 . t)),(b1 . t))) holds
b1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b1 . t)),(b1 . t))),S)) . m ) ) ) )
proofend;
uniqueness
 for b1, b2 being DecoratedTree of NAT st b1 . {} = FirstLoc M &amp; ( for t being Element of dom b1 holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b1 . t)),(b1 . t)))  }  &amp; ( for m being Element of NAT st m in card (NIC ((M /. (b1 . t)),(b1 . t))) holds
b1 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b1 . t)),(b1 . t))),S)) . m ) ) ) &amp; b2 . {} = FirstLoc M &amp; ( for t being Element of dom b2 holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b2 . t)),(b2 . t)))  }  &amp; ( for m being Element of NAT st m in card (NIC ((M /. (b2 . t)),(b2 . t))) holds
b2 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b2 . t)),(b2 . t))),S)) . m ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ExecTree AMISTD_3:def_2_:_
 for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for M being non empty preProgram of S
for b4 being DecoratedTree of NAT holds
( b4 = ExecTree M iff ( b4 . {} = FirstLoc M &amp; ( for t being Element of dom b4 holds
( succ t =  {  (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b4 . t)),(b4 . t)))  }  &amp; ( for m being Element of NAT st m in card (NIC ((M /. (b4 . t)),(b4 . t))) holds
b4 . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b4 . t)),(b4 . t))),S)) . m ) ) ) ) );

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
proofend;