:: AMISTD_3 semantic presentation

registration

let c₁ be set ;
let c₂ be PartFunc of c₁, NAT ;
let c₃ be set ;
cluster a₂ . a₃ -> natural ;
coherence

proof end;

end;

registration

let c₁ be empty Relation;
let c₂ be set ;
cluster a₁ | a₂ -> empty ;
coherence

proof end;

end;

theorem Th1: :: AMISTD_3:1

for b₁, b₂ being set
for b₃ being Relation st dom b₃ = {b₁} & rng b₃ = {b₂} holds
b₃ = b₁ .--> b₂

proof end;

theorem Th2: :: AMISTD_3:2

for b₁ being set holds field {[b₁,b₁]} = {b₁}

proof end;

registration

let c₁ be infinite set ;
let c₂ be set ;
cluster a₁ --> a₂ -> infinite ;
coherence

proof end;

end;

registration

cluster infinite set ;
existence

proof end;

end;

registration

let c₁ be finite Relation;
cluster field a₁ -> finite ;
coherence

proof end;

end;

theorem Th3: :: AMISTD_3:3

for b₁ being Relation st field b₁ is finite holds
b₁ is finite

proof end;

registration

let c₁ be infinite Relation;
cluster field a₁ -> infinite ;
coherence by Th3;

end;

theorem Th4: :: AMISTD_3:4

for b₁ being Relation st dom b₁ is finite & rng b₁ is finite holds
b₁ is finite

proof end;

registration

cluster RelIncl {} -> empty ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster RelIncl a₁ -> non empty ;
coherence

proof end;

end;

theorem Th5: :: AMISTD_3:5

for b₁ being set holds RelIncl {b₁} = {[b₁,b₁]}

proof end;

theorem Th6: :: AMISTD_3:6

for b₁ being set holds RelIncl b₁ c= [:b₁,b₁:]

proof end;

registration

let c₁ be finite set ;
cluster RelIncl a₁ -> finite ;
coherence

proof end;

end;

theorem Th7: :: AMISTD_3:7

for b₁ being set st RelIncl b₁ is finite holds
b₁ is finite

proof end;

registration

let c₁ be infinite set ;
cluster RelIncl a₁ -> non empty infinite ;
coherence by Th7;

end;

theorem Th8: :: AMISTD_3:8

for b₁, b₂ being Relation st b₁,b₂ are_isomorphic & b₁ is well-ordering holds
b₂ is well-ordering

proof end;

theorem Th9: :: AMISTD_3:9

for b₁, b₂ being Relation st b₁,b₂ are_isomorphic & b₁ is finite holds
b₂ is finite

proof end;

theorem Th10: :: AMISTD_3:10

for b₁, b₂ being set holds b₁ .--> b₂ is_isomorphism_of {[b₁,b₁]},{[b₂,b₂]}

proof end;

theorem Th11: :: AMISTD_3:11

for b₁, b₂ being set holds {[b₁,b₁]},{[b₂,b₂]} are_isomorphic

proof end;

registration

cluster order_type_of {} -> empty ;
coherence

proof end;

end;

theorem Th12: :: AMISTD_3:12

for b₁ being Ordinal holds order_type_of (RelIncl b₁) = b₁

proof end;

Lemma9: for b₁ being Ordinal
for b₂ being finite set st b₂ c= b₁ holds
order_type_of (RelIncl b₂) is finite

proof end;

theorem Th13: :: AMISTD_3:13

for b₁ being Ordinal
for b₂ being finite set st b₂ c= b₁ holds
order_type_of (RelIncl b₂) = card b₂

proof end;

theorem Th14: :: AMISTD_3:14

for b₁ being set
for b₂ being Ordinal st {b₁} c= b₂ holds
order_type_of (RelIncl {b₁}) = 1

proof end;

theorem Th15: :: AMISTD_3:15

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

proof end;

registration

let c₁ be Ordinal;
let c₂ be Subset of c₁;
let c₃ be set ;
cluster (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl a₂))),(RelIncl a₂)) . a₃ -> ordinal ;
coherence

proof end;

end;

registration

let c₁ be natural-membered set ;
let c₂ be set ;
cluster (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl a₁))),(RelIncl a₁)) . a₂ -> natural ;
coherence

proof end;

end;

theorem Th16: :: AMISTD_3:16

for b₁ being set
for b₂, b₃ being natural number st b₂ |-> b₁ = b₃ |-> b₁ holds
b₂ = b₃

proof end;

theorem Th17: :: AMISTD_3:17

for b₁ being natural number
for b₂ being Tree
for b₃ being Element of b₂ holds b₃ | (Seg b₁) in b₂

proof end;

theorem Th18: :: AMISTD_3:18

for b₁, b₂ being Tree st ( for b₃ being Nat holds b₁ -level b₃ = b₂ -level b₃ ) holds
b₁ = b₂

proof end;

definition

func TrivialInfiniteTree -> set equals :: AMISTD_3:def 1
{ (b₁ |-> 0) where B is Nat : verum } ;
coherence ;

end;

:: deftheorem Def1 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 -> non empty infinite Tree-like ;
coherence by Th19, CARD_1:68;

end;

theorem Th20: :: AMISTD_3:20

for b₁ being Nat holds TrivialInfiniteTree -level b₁ = {(b₁ |-> 0)}

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
assume that
E18: not c₃ is empty and
E19: c₃ is programmed ;
func FirstLoc c₃ -> Instruction-Location of a₂ means :Def2: :: AMISTD_3:def 2
ex b₁ being non empty Subset of NAT st
( b₁ = { (locnum b₂) where B is Element of the Instruction-Locations of a₂ : b₂ in dom a₃ } & a₄ = il. a₂,(min b₁) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines FirstLoc AMISTD_3:def 2 :

theorem Th21: :: AMISTD_3:21

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being non empty programmed FinPartState of b₂ holds FirstLoc b₃ in dom b₃

proof end;

theorem Th22: :: AMISTD_3:22

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃, b₄ being non empty programmed FinPartState of b₂ st b₃ c= b₄ holds
FirstLoc b₄ <= FirstLoc b₃

proof end;

theorem Th23: :: AMISTD_3:23

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being non empty programmed FinPartState of b₂ st b₃ in dom b₄ holds
FirstLoc b₄ <= b₃

proof end;

theorem Th24: :: AMISTD_3:24

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being non empty programmed lower FinPartState of b₂ holds FirstLoc b₃ = il. b₂,0

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be Subset of the Instruction-Locations of c₂;
func LocNums c₃ -> Subset of NAT equals :: AMISTD_3:def 3
{ (locnum b₁) where B is Instruction-Location of a₂ : b₁ in a₃ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines LocNums AMISTD_3:def 3 :

theorem Th25: :: AMISTD_3:25

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Subset of the Instruction-Locations of b₂ holds
( locnum b₃ in LocNums b₄ iff b₃ in b₄ )

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be empty Subset of the Instruction-Locations of c₂;
cluster LocNums a₃ -> empty ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be non empty Subset of the Instruction-Locations of c₂;
cluster LocNums a₃ -> non empty ;
coherence

proof end;

end;

theorem Th26: :: AMISTD_3:26

for b₁ being natural number
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₂
for b₄ being Subset of the Instruction-Locations of b₃ st b₄ = {(il. b₃,b₁)} holds
LocNums b₄ = {b₁}

proof end;

theorem Th27: :: AMISTD_3:27

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Subset of the Instruction-Locations of b₂ holds b₃, LocNums b₃ are_equipotent

proof end;

theorem Th28: :: AMISTD_3:28

proof end;

theorem Th29: :: AMISTD_3:29

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Instruction of b₂ st b₂ is realistic & b₄ is halting holds
LocNums (NIC b₄,b₃) = {(locnum b₃)}

proof end;

theorem Th30: :: AMISTD_3:30

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Instruction of b₂ st b₂ is realistic & b₄ is sequential holds
LocNums (NIC b₄,b₃) = {(locnum (NextLoc b₃))}

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be Subset of the Instruction-Locations of c₂;
deffunc H₁( set ) -> Element of the Instruction-Locations of c₂ = il. c₂,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums c₃)))),(RelIncl (LocNums c₃))) . a₁);
set c₄ = the Instruction-Locations of c₂;
func LocSeq c₃ -> T-Sequence of the Instruction-Locations of a₂ means :Def4: :: AMISTD_3:def 4
( dom a₄ = Card a₃ & ( for b₁ being set st b₁ in Card a₃ holds
a₄ . b₁ = il. a₂,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums a₃)))),(RelIncl (LocNums a₃))) . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines LocSeq AMISTD_3:def 4 :

theorem Th31: :: AMISTD_3:31

proof end;

registration

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
func ExecTree c₃ -> DecoratedTree of the Instruction-Locations of a₂ means :Def5: :: AMISTD_3:def 5
( a₄ . {} = FirstLoc a₃ & ( for b₁ being Element of dom a₄ holds
( succ b₁ = { (b₁ ^ <*b₂*>) where B is Nat : b₂ in Card (NIC (pi a₃,(a₄ . b₁)),(a₄ . b₁)) } & ( for b₂ being Nat st b₂ in Card (NIC (pi a₃,(a₄ . b₁)),(a₄ . b₁)) holds
a₄ . (b₁ ^ <*b₂*>) = (LocSeq (NIC (pi a₃,(a₄ . b₁)),(a₄ . b₁))) . b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ExecTree AMISTD_3:def 5 :

theorem Th32: :: AMISTD_3:32

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic standard AMI-Struct of b₁ holds ExecTree (Stop b₂) = TrivialInfiniteTree --> (il. b₂,0)

proof end;