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

begin

theorem :: AMISTD_3:1

canceled;

theorem :: AMISTD_3:2

canceled;

theorem :: AMISTD_3:3

canceled;

theorem :: AMISTD_3:4

canceled;

theorem :: AMISTD_3:5

canceled;

theorem :: AMISTD_3:6

canceled;

theorem :: AMISTD_3:7

canceled;

theorem :: AMISTD_3:8

canceled;

theorem :: AMISTD_3:9

canceled;

theorem :: AMISTD_3:10

canceled;

theorem :: AMISTD_3:11

canceled;

theorem :: AMISTD_3:12

canceled;

theorem :: AMISTD_3:13

canceled;

theorem :: AMISTD_3:14

canceled;

theorem :: AMISTD_3:15

canceled;

theorem :: AMISTD_3:16

canceled;

theorem :: AMISTD_3:17

canceled;

theorem :: AMISTD_3:18

canceled;

theorem :: AMISTD_3:19

canceled;

theorem :: AMISTD_3:20

canceled;

theorem :: AMISTD_3:21

canceled;

theorem :: AMISTD_3:22

canceled;

theorem :: AMISTD_3:23

canceled;

theorem :: AMISTD_3:24

canceled;

definition

canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
let M be Subset of NAT;
deffunc H₁( set ) -> set = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . $1;
func LocSeq (M,S) -> T-Sequence of NAT means :Def3: :: AMISTD_3:def 3
( 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 b₁ being T-Sequence of NAT st
( dom b₁ = card M & ( for m being set st m in card M holds
b₁ . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) )

proof end;

uniqueness
for b₁, b₂ being T-Sequence of NAT st dom b₁ = card M & ( for m being set st m in card M holds
b₁ . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) & dom b₂ = card M & ( for m being set st m in card M holds
b₂ . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) holds
b₁ = b₂

proof end;

end;

:: deftheorem AMISTD_3:def 1 :
canceled;

:: deftheorem AMISTD_3:def 2 :
canceled;

:: deftheorem Def3 defines LocSeq AMISTD_3:def 3 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for M being Subset of NAT
for b₄ being T-Sequence of NAT holds
( b₄ = LocSeq (M,S) iff ( dom b₄ = card M & ( for m being set st m in card M holds
b₄ . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) ) );

theorem :: AMISTD_3:25

canceled;

theorem :: AMISTD_3:26

canceled;

theorem :: AMISTD_3:27

canceled;

theorem :: AMISTD_3:28

canceled;

theorem :: AMISTD_3:29

canceled;

theorem :: AMISTD_3:30

canceled;

theorem :: AMISTD_3:31

for n being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being Subset of NAT st F = {n} holds
LocSeq (F,S) = 0 .--> n

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
let M be Subset of NAT;
cluster LocSeq (M,S) -> one-to-one ;
coherence
LocSeq (M,S) is one-to-one

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
let M be NAT -defined the Instructions of S -valued non empty FinPartState of ;
func ExecTree M -> DecoratedTree of NAT means :Def4: :: AMISTD_3:def 4
( 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))) } & ( 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 b₁ being DecoratedTree of NAT st
( b₁ . {} = FirstLoc M & ( for t being Element of dom b₁ holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b₁ . t)),(b₁ . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b₁ . t)),(b₁ . t))) holds
b₁ . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b₁ . t)),(b₁ . t))),S)) . m ) ) ) )

proof end;

uniqueness
for b₁, b₂ being DecoratedTree of NAT st b₁ . {} = FirstLoc M & ( for t being Element of dom b₁ holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b₁ . t)),(b₁ . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b₁ . t)),(b₁ . t))) holds
b₁ . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b₁ . t)),(b₁ . t))),S)) . m ) ) ) & b₂ . {} = FirstLoc M & ( for t being Element of dom b₂ holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b₂ . t)),(b₂ . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b₂ . t)),(b₂ . t))) holds
b₂ . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b₂ . t)),(b₂ . t))),S)) . m ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines ExecTree AMISTD_3:def 4 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for M being NAT -defined the Instructions of b₂ -valued non empty FinPartState of
for b₄ being DecoratedTree of NAT holds
( b₄ = ExecTree M iff ( b₄ . {} = FirstLoc M & ( for t being Element of dom b₄ holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC ((M /. (b₄ . t)),(b₄ . t))) } & ( for m being Element of NAT st m in card (NIC ((M /. (b₄ . t)),(b₄ . t))) holds
b₄ . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b₄ . t)),(b₄ . t))),S)) . m ) ) ) ) );

theorem :: AMISTD_3:32

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting standard AMI-Struct of N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0

proof end;