:: A Tree of Execution of a Macroinstruction
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem Th1: :: AMISTD_3:1
theorem Th2: :: AMISTD_3:2
theorem :: AMISTD_3:3
canceled;
theorem :: AMISTD_3:4
canceled;
theorem Th5: :: AMISTD_3:5
theorem Th6: :: AMISTD_3:6
theorem Th7: :: AMISTD_3:7
theorem :: AMISTD_3:8
theorem Th9: :: AMISTD_3:9
theorem Th10: :: AMISTD_3:10
theorem :: AMISTD_3:11
theorem :: AMISTD_3:12
Lm1:
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
theorem Th13: :: AMISTD_3:13
theorem Th14: :: AMISTD_3:14
theorem Th15: :: AMISTD_3:15
theorem Th16: :: AMISTD_3:16
theorem :: AMISTD_3:17
theorem Th18: :: AMISTD_3:18
:: deftheorem defines TrivialInfiniteTree AMISTD_3:def 1 :
theorem Th19: :: AMISTD_3:19
theorem Th20: :: AMISTD_3:20
:: deftheorem Def2 defines FirstLoc AMISTD_3:def 2 :
theorem Th21: :: AMISTD_3:21
theorem :: AMISTD_3:22
theorem Th23: :: AMISTD_3:23
theorem :: AMISTD_3:24
:: deftheorem defines LocNums AMISTD_3:def 3 :
theorem Th25: :: AMISTD_3:25
theorem Th26: :: AMISTD_3:26
theorem Th27: :: AMISTD_3:27
theorem Th28: :: AMISTD_3:28
theorem Th29: :: AMISTD_3:29
theorem :: AMISTD_3:30
definition
let N be
with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard AMI-Struct of
NAT ,
N;
let M be
IL-Subset of
S;
deffunc H1(
set )
-> Instruction-Location of
S =
il. S,
((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M)))),(RelIncl (LocNums M))) . $1);
set Z =
NAT ;
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
ex b1 being T-Sequence of NAT st
( dom b1 = card M & ( for m being set st m in card M holds
b1 . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M)))),(RelIncl (LocNums M))) . m) ) )
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 = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M)))),(RelIncl (LocNums M))) . m) ) & dom b2 = card M & ( for m being set st m in card M holds
b2 . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M)))),(RelIncl (LocNums M))) . m) ) holds
b1 = b2
end;
:: deftheorem Def4 defines LocSeq AMISTD_3:def 4 :
theorem :: AMISTD_3:31
definition
let N be
with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite standard AMI-Struct of
NAT ,
N;
let M be
programmed 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
ex b1 being IL-DecoratedTree of S st
( b1 . {} = FirstLoc M & ( for t being Element of dom b1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(b1 . t)),(b1 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(b1 . t)),(b1 . t)) holds
b1 . (t ^ <*m*>) = (LocSeq (NIC (pi M,(b1 . t)),(b1 . t))) . m ) ) ) )
uniqueness
for b1, b2 being IL-DecoratedTree of S st b1 . {} = FirstLoc M & ( for t being Element of dom b1 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(b1 . t)),(b1 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(b1 . t)),(b1 . t)) holds
b1 . (t ^ <*m*>) = (LocSeq (NIC (pi M,(b1 . t)),(b1 . t))) . m ) ) ) & b2 . {} = FirstLoc M & ( for t being Element of dom b2 holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in card (NIC (pi M,(b2 . t)),(b2 . t)) } & ( for m being Element of NAT st m in card (NIC (pi M,(b2 . t)),(b2 . t)) holds
b2 . (t ^ <*m*>) = (LocSeq (NIC (pi M,(b2 . t)),(b2 . t))) . m ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines ExecTree AMISTD_3:def 5 :
theorem :: AMISTD_3:32