begin
theorem Th1:
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem
Lm1:
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
:: deftheorem defines TrivialInfiniteTree AMISTD_3:def 1 :
theorem Th19:
theorem Th20:
:: deftheorem Def2 defines FirstLoc AMISTD_3:def 2 :
theorem Th21:
theorem
theorem Th23:
theorem
:: deftheorem defines LocNums AMISTD_3:def 3 :
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
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 H1(
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:
(
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
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 ;
func ExecTree M -> IL-DecoratedTree of
S means :
Def5:
(
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