:: AMISTD_3 semantic presentation

registration

let D be set ;
let f be PartFunc of D, NAT ;
let n be set ;
cluster f . n -> natural ;
coherence

proof end;

end;

registration

let R be empty Relation;
let X be set ;
cluster R | X -> empty ;
coherence

proof end;

end;

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

proof end;

end;

registration

cluster infinite set ;
existence

proof end;

end;

registration

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

proof end;

end;

theorem Th3: :: AMISTD_3:3

for R being Relation st field R is finite holds
R is finite

proof end;

registration

let R be infinite Relation;
cluster field R -> infinite ;
coherence by Th3;

end;

theorem :: AMISTD_3:4

for R being Relation st dom R is finite & rng R is finite holds
R is finite

proof 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 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 -> non empty 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 Th17: :: AMISTD_3:17

for n being natural number
for T being Tree
for t being Element of T holds t | (Seg n) in T

proof end;

theorem Th18: :: AMISTD_3:18

for T1, T2 being Tree st ( for n being 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 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 -> non empty infinite Tree-like ;
coherence by Th19, CARD_1:68;

end;

theorem Th20: :: AMISTD_3:20

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

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be FinPartState of S;
assume that
A1: not F is empty and
A2: F is programmed ;
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 Element of the Instruction-Locations 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 non void IC-Ins-separated definite standard AMI-Struct of N
for F being non empty programmed 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 non void IC-Ins-separated definite standard AMI-Struct of N
for F, G being non empty programmed 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 non void IC-Ins-separated definite standard AMI-Struct of N
for l1 being Instruction-Location of S
for F being non empty programmed 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 non void IC-Ins-separated definite standard AMI-Struct of N
for F being non empty programmed 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 non void IC-Ins-separated definite standard AMI-Struct of N;
let F be Subset of the Instruction-Locations 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 non void IC-Ins-separated definite standard AMI-Struct of N
for l1 being Instruction-Location of S
for F being Subset of the Instruction-Locations 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 non void IC-Ins-separated definite standard AMI-Struct of N;
let F be empty Subset of the Instruction-Locations of S;
cluster LocNums F -> empty ;
coherence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let F be non empty Subset of the Instruction-Locations 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 non void IC-Ins-separated definite standard AMI-Struct of N
for F being Subset of the Instruction-Locations 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 non void IC-Ins-separated definite standard AMI-Struct of N
for F being Subset of the Instruction-Locations of S holds F, LocNums F are_equipotent

proof end;

theorem Th28: :: AMISTD_3:28

proof end;

theorem Th29: :: AMISTD_3:29

for N being with_non-empty_elements set
for S being non empty non void 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

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let M be Subset of the Instruction-Locations of S;
deffunc H₁( set ) -> Element of the Instruction-Locations of S = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M)))),(RelIncl (LocNums M))) . $1);
set Z = the Instruction-Locations of S;
func LocSeq M -> T-Sequence of the Instruction-Locations of S 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

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite standard AMI-Struct of N;
let M be FinPartState of S;
func ExecTree M -> DecoratedTree of the Instruction-Locations 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 Nat : k in Card (NIC (pi M,(it . t)),(it . t)) } & ( for m being 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 non void halting IC-Ins-separated definite realistic standard AMI-Struct of N holds ExecTree (Stop S) = TrivialInfiniteTree --> (il. S,0)

proof end;