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

theorem Th1: :: AMISTD_3:1

for x, y being set
for R being Relation st dom R = {x} & rng R = {y} holds
R = x .--> y

proof end;

theorem Th2: :: AMISTD_3:2

for x being set holds field {[x,x]} = {x}

proof end;

registration

let X be infinite set ;
let a be set ;
cluster X --> a -> infinite ;
coherence ;

end;

registration

cluster infinite set ;
existence

proof end;

end;

registration

let R be finite Relation;
cluster field R -> finite ;
coherence ;

end;

registration

let R be infinite Relation;
cluster field R -> infinite ;
coherence by ORDERS_1:196;

end;

registration

cluster RelIncl {} -> empty ;
coherence

proof end;

end;

registration

let X be non empty set ;
cluster RelIncl X -> non empty ;
coherence

proof end;

end;

theorem :: AMISTD_3:3

canceled;

theorem :: AMISTD_3:4

canceled;

theorem Th5: :: AMISTD_3:5

for x being set holds RelIncl {x} = {[x,x]}

proof end;

theorem Th6: :: AMISTD_3:6

for X being set holds RelIncl X c= [:X,X:]

proof end;

registration

let X be finite set ;
cluster RelIncl X -> finite ;
coherence

proof end;

end;

theorem Th7: :: AMISTD_3:7

for X being set st RelIncl X is finite holds
X is finite

proof end;

registration

let X be infinite set ;
cluster RelIncl X -> infinite ;
coherence by Th7;

end;

theorem :: AMISTD_3:8

for R, S being Relation st R,S are_isomorphic & R is well-ordering holds
S is well-ordering

proof end;

theorem Th9: :: AMISTD_3:9

for R, S being Relation st R,S are_isomorphic & R is finite holds
S is finite

proof end;

theorem Th10: :: AMISTD_3:10

for x, y being set holds x .--> y is_isomorphism_of {[x,x]},{[y,y]}

proof end;

theorem :: AMISTD_3:11

for x, y being set holds {[x,x]},{[y,y]} are_isomorphic

proof end;

registration

cluster order_type_of {} -> empty ;
coherence

proof end;

end;

theorem :: AMISTD_3:12

for O being Ordinal holds order_type_of (RelIncl O) = O

proof end;

Lm1: for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite

proof end;

theorem Th13: :: AMISTD_3:13

for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X

proof end;

theorem Th14: :: AMISTD_3:14

for x being set
for O being Ordinal st {x} c= O holds
order_type_of (RelIncl {x}) = 1

proof end;

theorem Th15: :: AMISTD_3:15

for x being set
for O being Ordinal st {x} c= O holds
canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {x}))),(RelIncl {x}) = 0 .--> x

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th16: :: AMISTD_3:16

for x being set
for n, m being natural number st n |-> x = m |-> x holds
n = m

proof end;

theorem :: AMISTD_3:17

for n being natural number
for T being Tree
for t being Element of T holds t | (Seg n) in T by RELAT_1:88, TREES_1:45;

theorem Th18: :: AMISTD_3:18

for T1, T2 being Tree st ( for n being Element of NAT holds T1 -level n = T2 -level n ) holds
T1 = T2

proof end;

definition

func TrivialInfiniteTree -> set equals :: AMISTD_3:def 1
{ (k |-> 0 ) where k is Element of NAT : verum } ;
coherence ;

end;

:: deftheorem defines TrivialInfiniteTree AMISTD_3:def 1 :

registration

cluster TrivialInfiniteTree -> non empty Tree-like ;
coherence

proof end;

end;

theorem Th19: :: AMISTD_3:19

NAT , TrivialInfiniteTree are_equipotent

proof end;

registration

cluster TrivialInfiniteTree -> infinite ;
coherence by Th19, CARD_1:68;

end;

theorem Th20: :: AMISTD_3:20

for n being Element of NAT holds TrivialInfiniteTree -level n = {(n |-> 0 )}

proof end;

definition

let N be 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 -> Instruction-Location of S means :Def2: :: AMISTD_3:def 2
ex M being non empty Subset of NAT st
( M = { (locnum l) where l is Instruction-Location of S : l in dom F } & it = il. S,(min M) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines FirstLoc AMISTD_3:def 2 :

theorem Th21: :: AMISTD_3:21

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

proof end;

theorem :: AMISTD_3:22

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

proof end;

theorem Th23: :: AMISTD_3:23

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

proof end;

theorem :: AMISTD_3:24

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined non empty lower FinPartState of S holds FirstLoc F = il. S,0

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
let F be IL-Subset 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 } ;
coherence

proof end;

end;

:: deftheorem defines LocNums AMISTD_3:def 3 :

theorem Th25: :: AMISTD_3:25

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for l1 being Instruction-Location of S
for F being IL-Subset of S holds
( locnum l1 in LocNums F iff l1 in F )

proof end;

registration

let N be 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 IL-Subset of S;
cluster LocNums F -> empty ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th26: :: AMISTD_3:26

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

proof end;

theorem Th27: :: AMISTD_3:27

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

proof end;

theorem Th28: :: AMISTD_3:28

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being IL-Subset of S holds card F c= order_type_of (RelIncl (LocNums F))

proof end;

theorem Th29: :: AMISTD_3:29

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

proof end;

theorem :: AMISTD_3:30

proof end;

definition

set Z = NAT ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
let M be IL-Subset of S;
deffunc H₁( set ) -> Instruction-Location of S = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M)))),(RelIncl (LocNums M))) . $1);
func LocSeq M -> T-Sequence of NAT means :Def4: :: 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) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines LocSeq AMISTD_3:def 4 :

theorem :: AMISTD_3:31

proof end;

registration

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

proof end;

end;

definition

let N be 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 FinPartState of S;
func ExecTree M -> IL-DecoratedTree of S means :Def5: :: AMISTD_3:def 5
( 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 (pi M,(it . t)),(it . t)) } & ( for m being Element of 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 ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ExecTree AMISTD_3:def 5 :

theorem :: AMISTD_3:32

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

proof end;