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 Association of Mizar Users

begin

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 F be FinPartState of S;
assume A1: ( not F is empty & F is NAT -defined ) ;
func FirstLoc F -> Element of NAT means :Def2: :: AMISTD_3:def 1
ex M being non empty Subset of NAT st
( M = { (locnum l,S) where l is Element of NAT : l in dom F } & it = il. S,(min M) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines FirstLoc AMISTD_3:def 1 :

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 Th21: :: AMISTD_3:21

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of holds FirstLoc F in dom F

proof end;

theorem :: AMISTD_3:22

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F, G being NAT -defined non empty FinPartState of st F c= G holds
FirstLoc G <= FirstLoc F,S

proof end;

theorem Th23: :: AMISTD_3:23

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for l1 being Element of NAT
for F being NAT -defined non empty FinPartState of st l1 in dom F holds
FirstLoc F <= l1,S

proof end;

theorem :: AMISTD_3:24

proof 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 F be Subset of NAT ;
func LocNums F,S -> Subset of NAT equals :: AMISTD_3:def 2
{ (locnum l,S) where l is Element of NAT : l in F } ;
coherence

proof end;

end;

:: deftheorem defines LocNums AMISTD_3:def 2 :

theorem Th25: :: AMISTD_3:25

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for l1 being Element of NAT
for F being Subset of NAT holds
( locnum l1,S in LocNums F,S iff l1 in F )

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 F be empty Subset of NAT ;
cluster LocNums F,S -> empty ;
coherence

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N;
let F be non empty Subset of NAT ;
cluster LocNums F,S -> non empty ;
coherence

proof end;

end;

theorem Th26: :: AMISTD_3:26

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 steady-programmed definite standard AMI-Struct of N
for F being Subset of NAT st F = {(il. S,n)} holds
LocNums F,S = {n}

proof end;

theorem Th27: :: AMISTD_3:27

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F being Subset of NAT holds F, LocNums F,S are_equipotent

proof end;

theorem Th28: :: AMISTD_3:28

proof end;

theorem Th29: :: AMISTD_3:29

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for L being Element of NAT
for J being Instruction of S st S is realistic & J is halting holds
LocNums (NIC J,L),S = {(locnum L,S)}

proof end;

theorem :: AMISTD_3:30

proof end;

definition

set Z = NAT ;
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 ) -> Element of NAT = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . $1);
func LocSeq M,S -> T-Sequence of NAT means :Def4: :: AMISTD_3:def 3
( 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,S)))),(RelIncl (LocNums M,S))) . m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines LocSeq AMISTD_3:def 3 :

theorem :: AMISTD_3:31

proof end;

registration

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ExecTree AMISTD_3:def 4 :

theorem :: AMISTD_3:32

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

proof end;