:: AMI_1 semantic presentation

theorem Th1: :: AMI_1:1

canceled;

theorem Th2: :: AMI_1:2

for b₁, b₂ being set holds 1 <> [b₁,b₂] by ZFMISC_1:8, CARD_5:1;

theorem Th3: :: AMI_1:3

for b₁, b₂ being set holds 2 <> [b₁,b₂] by ZFMISC_1:10, CARD_5:1;

theorem Th4: :: AMI_1:4

canceled;

theorem Th5: :: AMI_1:5

for b₁, b₂, b₃, b₄ being set st b₁ <> b₂ holds
product (b₁,b₂ --> {b₃},{b₄}) = {(b₁,b₂ --> b₃,b₄)}

proof end;

definition

let c₁ be set ;
attr a₂ is strict;
struct AMI-Struct of c₁ -> 1-sorted ;
aggr AMI-Struct(# carrier, Instruction-Counter, Instruction-Locations, Instruction-Codes, Instructions, Object-Kind, Execution #) -> AMI-Struct of a₁;
sel Instruction-Counter c₂ -> Element of the carrier of a₂;
sel Instruction-Locations c₂ -> Subset of the carrier of a₂;
sel Instruction-Codes c₂ -> non empty set ;
sel Instructions c₂ -> non empty Subset of [:the Instruction-Codes of a₂,(((union a₁) \/ the carrier of a₂) * ):];
sel Object-Kind c₂ -> Function of the carrier of a₂,a₁ \/ {the Instructions of a₂,the Instruction-Locations of a₂};
sel Execution c₂ -> Function of the Instructions of a₂, Funcs (product the Object-Kind of a₂),(product the Object-Kind of a₂);

end;

definition

let c₁ be set ;
canceled;
func Trivial-AMI c₁ -> strict AMI-Struct of a₁ means :Def2: :: AMI_1:def 2
( the carrier of a₂ = {0,1} & the Instruction-Counter of a₂ = 0 & the Instruction-Locations of a₂ = {1} & the Instruction-Codes of a₂ = {0} & the Instructions of a₂ = {[0,{} ]} & the Object-Kind of a₂ = 0,1 --> {1},{[0,{} ]} & the Execution of a₂ = [0,{} ] .--> (id (product (0,1 --> {1},{[0,{} ]}))) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def1 AMI_1:def 1 :

:: deftheorem Def2 defines Trivial-AMI AMI_1:def 2 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is void means :Def3: :: AMI_1:def 3
the Instruction-Locations of a₂ is empty;

end;

:: deftheorem Def3 defines void AMI_1:def 3 :

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster non empty non void AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non void AMI-Struct of c₁;
cluster the Instruction-Locations of a₂ -> non empty ;
coherence by Def3;

end;

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
mode Object of a₂ is Element of a₂;

end;

definition

let c₁ be set ;
let c₂ be non empty non void AMI-Struct of c₁;
mode Instruction-Location of a₂ is Element of the Instruction-Locations of a₂;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
mode Instruction of a₂ is Element of the Instructions of a₂;

end;

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
canceled;
func IC c₂ -> Object of a₂ equals :: AMI_1:def 5
the Instruction-Counter of a₂;
correctness ;

end;

:: deftheorem Def4 AMI_1:def 4 :

:: deftheorem Def5 defines IC AMI_1:def 5 :

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
let c₃ be Object of c₂;
func ObjectKind c₃ -> Element of a₁ \/ {the Instructions of a₂,the Instruction-Locations of a₂} equals :: AMI_1:def 6
the Object-Kind of a₂ . a₃;
correctness ;

end;

:: deftheorem Def6 defines ObjectKind AMI_1:def 6 :

registration

let c₁ be Function;
cluster product a₁ -> functional ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be with_non-empty_elements set ;
let c₃ be Function of c₁,c₂;
cluster product a₃ -> non empty functional ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
mode State of a₂ is Element of product the Object-Kind of a₂;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Instruction of c₂;
let c₄ be State of c₂;
func Exec c₃,c₄ -> State of a₂ equals :: AMI_1:def 7
(the Execution of a₂ . a₃) . a₄;
coherence

proof end;

end;

:: deftheorem Def7 defines Exec AMI_1:def 7 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is halting means :Def8: :: AMI_1:def 8
for b₁ being State of a₂ holds Exec a₃,b₁ = b₁;

end;

:: deftheorem Def8 defines halting AMI_1:def 8 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
attr a₂ is halting means :Def9: :: AMI_1:def 9
ex b₁ being Instruction of a₂ st
( b₁ is halting & ( for b₂ being Instruction of a₂ st b₂ is halting holds
b₁ = b₂ ) );

end;

:: deftheorem Def9 defines halting AMI_1:def 9 :

theorem Th6: :: AMI_1:6

for b₁ being with_non-empty_elements set holds Trivial-AMI b₁ is halting

proof end;

registration

let c₁ be with_non-empty_elements set ;
cluster Trivial-AMI a₁ -> non empty strict non void halting ;
coherence by Th6;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non void halting AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
cluster halting Element of the Instructions of a₂;
existence

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
func halt c₂ -> Instruction of a₂ means :Def10: :: AMI_1:def 10
a₃ is halting Instruction of a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines halt AMI_1:def 10 :

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
cluster halt a₂ -> halting ;
coherence by Def10;

end;

definition

let c₁ be set ;
let c₂ be non empty AMI-Struct of c₁;
attr a₂ is IC-Ins-separated means :Def11: :: AMI_1:def 11
ObjectKind (IC a₂) = the Instruction-Locations of a₂;

end;

:: deftheorem Def11 defines IC-Ins-separated AMI_1:def 11 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is data-oriented means :: AMI_1:def 12
the Object-Kind of a₂ " {the Instructions of a₂} c= the Instruction-Locations of a₂;

end;

:: deftheorem Def12 defines data-oriented AMI_1:def 12 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void AMI-Struct of c₁;
attr a₂ is steady-programmed means :Def13: :: AMI_1:def 13
for b₁ being State of a₂
for b₂ being Instruction of a₂
for b₃ being Instruction-Location of a₂ holds (Exec b₂,b₁) . b₃ = b₁ . b₃;

end;

:: deftheorem Def13 defines steady-programmed AMI_1:def 13 :

definition

let c₁ be set ;
let c₂ be non empty non void AMI-Struct of c₁;
attr a₂ is definite means :Def14: :: AMI_1:def 14
for b₁ being Instruction-Location of a₂ holds ObjectKind b₁ = the Instructions of a₂;

end;

:: deftheorem Def14 defines definite AMI_1:def 14 :

theorem Th7: :: AMI_1:7

for b₁ being set holds Trivial-AMI b₁ is IC-Ins-separated

proof end;

theorem Th8: :: AMI_1:8

for b₁ being set holds Trivial-AMI b₁ is data-oriented

proof end;

theorem Th9: :: AMI_1:9

for b₁ being set
for b₂, b₃ being State of (Trivial-AMI b₁) holds b₂ = b₃

proof end;

theorem Th10: :: AMI_1:10

for b₁ being with_non-empty_elements set holds Trivial-AMI b₁ is steady-programmed

proof end;

theorem Th11: :: AMI_1:11

for b₁ being set holds Trivial-AMI b₁ is definite

proof end;

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void data-oriented ;
coherence by Th8;

end;

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence by Th7, Th11;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster Trivial-AMI a₁ -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite ;
coherence by Th10;

end;

registration

let c₁ be set ;
cluster strict data-oriented AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
cluster non empty strict non void IC-Ins-separated data-oriented definite AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite AMI-Struct of a₁;
existence

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated AMI-Struct of c₁;
let c₃ be State of c₂;
func IC c₃ -> Instruction-Location of a₂ equals :: AMI_1:def 15
a₃ . (IC a₂);
coherence

proof end;

end;

:: deftheorem Def15 defines IC AMI_1:def 15 :

theorem Th12: :: AMI_1:12

canceled;

theorem Th13: :: AMI_1:13

canceled;

theorem Th14: :: AMI_1:14

for b₁, b₂, b₃ being set
for b₄, b₅ being Function st b₄ tolerates b₅ & [b₁,b₂] in b₄ & [b₁,b₃] in b₅ holds
b₂ = b₃

proof end;

theorem Th15: :: AMI_1:15

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Function ) & ( for b₂, b₃ being Function st b₂ in b₁ & b₃ in b₁ holds
b₂ tolerates b₃ ) holds
union b₁ is Function

proof end;

theorem Th16: :: AMI_1:16

canceled;

theorem Th17: :: AMI_1:17

canceled;

theorem Th18: :: AMI_1:18

for b₁, b₂, b₃, b₄ being set holds b₁,b₂ --> b₃,b₄ = (b₁ .--> b₃) +* (b₂ .--> b₄) by FUNCT_4:def 4;

theorem Th19: :: AMI_1:19

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

proof end;

theorem Th20: :: AMI_1:20

for b₁, b₂, b₃ being set holds b₁,b₁ --> b₂,b₃ = b₁ .--> b₃

proof end;

theorem Th21: :: AMI_1:21

canceled;

theorem Th22: :: AMI_1:22

for b₁ being set
for b₂ being Function st b₁ in product b₂ holds
b₁ is Function

proof end;

definition

let c₁ be Function;
func sproduct c₁ -> set means :Def16: :: AMI_1:def 16
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being Function st
( b₁ = b₂ & dom b₂ c= dom a₁ & ( for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ in a₁ . b₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines sproduct AMI_1:def 16 :

registration

let c₁ be Function;
cluster sproduct a₁ -> non empty functional ;
coherence

proof end;

end;

theorem Th23: :: AMI_1:23

canceled;

theorem Th24: :: AMI_1:24

canceled;

theorem Th25: :: AMI_1:25

for b₁, b₂ being Function st b₁ in sproduct b₂ holds
( dom b₁ c= dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ in b₂ . b₃ ) )

proof end;

theorem Th26: :: AMI_1:26

for b₁ being Function holds {} in sproduct b₁

proof end;

theorem Th27: :: AMI_1:27

for b₁ being Function holds product b₁ c= sproduct b₁

proof end;

theorem Th28: :: AMI_1:28

for b₁ being set
for b₂ being Function st b₁ in sproduct b₂ holds
b₁ is PartFunc of dom b₂, union (rng b₂)

proof end;

theorem Th29: :: AMI_1:29

for b₁, b₂, b₃ being Function st b₁ in product b₂ & b₃ in sproduct b₂ holds
b₁ +* b₃ in product b₂

proof end;

theorem Th30: :: AMI_1:30

for b₁, b₂ being Function st product b₁ <> {} holds
( b₂ in sproduct b₁ iff ex b₃ being Function st
( b₃ in product b₁ & b₂ <= b₃ ) )

proof end;

theorem Th31: :: AMI_1:31

for b₁ being Function holds sproduct b₁ c= PFuncs (dom b₁),(union (rng b₁))

proof end;

theorem Th32: :: AMI_1:32

for b₁, b₂ being Function st b₁ c= b₂ holds
sproduct b₁ c= sproduct b₂

proof end;

theorem Th33: :: AMI_1:33

sproduct {} = {{} }

proof end;

theorem Th34: :: AMI_1:34

for b₁, b₂ being set holds PFuncs b₁,b₂ = sproduct (b₁ --> b₂)

proof end;

theorem Th35: :: AMI_1:35

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ holds sproduct b₃ = sproduct (b₃ | { b₄ where B is Element of b₁ : b₃ . b₄ <> {} } )

proof end;

theorem Th36: :: AMI_1:36

for b₁, b₂ being set
for b₃ being Function st b₁ in dom b₃ & b₂ in b₃ . b₁ holds
b₁ .--> b₂ in sproduct b₃

proof end;

theorem Th37: :: AMI_1:37

for b₁ being Function holds
( sproduct b₁ = {{} } iff for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ = {} )

proof end;

theorem Th38: :: AMI_1:38

for b₁ being set
for b₂ being Function st b₁ c= sproduct b₂ & ( for b₃, b₄ being Function st b₃ in b₁ & b₄ in b₁ holds
b₃ tolerates b₄ ) holds
union b₁ in sproduct b₂

proof end;

theorem Th39: :: AMI_1:39

for b₁, b₂, b₃ being Function st b₁ tolerates b₂ & b₁ in sproduct b₃ & b₂ in sproduct b₃ holds
b₁ \/ b₂ in sproduct b₃

proof end;

theorem Th40: :: AMI_1:40

for b₁, b₂, b₃ being Function st b₁ c= b₂ & b₂ in sproduct b₃ holds
b₁ in sproduct b₃

proof end;

theorem Th41: :: AMI_1:41

for b₁ being set
for b₂, b₃ being Function st b₂ in sproduct b₃ holds
b₂ | b₁ in sproduct b₃

proof end;

theorem Th42: :: AMI_1:42

for b₁ being set
for b₂, b₃ being Function st b₂ in sproduct b₃ holds
b₂ | b₁ in sproduct (b₃ | b₁)

proof end;

theorem Th43: :: AMI_1:43

for b₁, b₂, b₃ being Function st b₁ in sproduct (b₂ +* b₃) holds
ex b₄, b₅ being Function st
( b₄ in sproduct b₂ & b₅ in sproduct b₃ & b₁ = b₄ +* b₅ )

proof end;

theorem Th44: :: AMI_1:44

for b₁, b₂, b₃, b₄ being Function st dom b₁ misses (dom b₃) \ (dom b₄) & b₃ in sproduct b₂ & b₄ in sproduct b₁ holds
b₃ +* b₄ in sproduct (b₂ +* b₁)

proof end;

theorem Th45: :: AMI_1:45

for b₁, b₂, b₃, b₄ being Function st dom b₃ misses (dom b₁) \ (dom b₄) & b₃ in sproduct b₂ & b₄ in sproduct b₁ holds
b₃ +* b₄ in sproduct (b₂ +* b₁)

proof end;

theorem Th46: :: AMI_1:46

for b₁, b₂, b₃ being Function st b₁ in sproduct b₂ & b₃ in sproduct b₂ holds
b₁ +* b₃ in sproduct b₂

proof end;

theorem Th47: :: AMI_1:47

for b₁ being Function
for b₂, b₃, b₄, b₅ being set st b₂ in dom b₁ & b₄ in b₁ . b₂ & b₃ in dom b₁ & b₅ in b₁ . b₃ holds
b₂,b₃ --> b₄,b₅ in sproduct b₁

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
func CurInstr c₃ -> Instruction of a₂ equals :: AMI_1:def 17
a₃ . (IC a₃);
coherence

proof end;

end;

:: deftheorem Def17 defines CurInstr AMI_1:def 17 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
func Following c₃ -> State of a₂ equals :: AMI_1:def 18
Exec (CurInstr a₃),a₃;
correctness ;

end;

:: deftheorem Def18 defines Following AMI_1:def 18 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
func Computation c₃ -> Function of NAT , product the Object-Kind of a₂ means :Def19: :: AMI_1:def 19
( a₄ . 0 = a₃ & ( for b₁ being Nat holds a₄ . (b₁ + 1) = Following (a₄ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines Computation AMI_1:def 19 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non void AMI-Struct of c₁;
let c₃ be Function of NAT , product the Object-Kind of c₂;
let c₄ be Nat;
redefine func . as c₃ . c₄ -> State of a₂;
coherence by FUNCT_2:7;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
attr a₃ is halting means :Def20: :: AMI_1:def 20
ex b₁ being Nat st CurInstr ((Computation a₃) . b₁) = halt a₂;

end;

:: deftheorem Def20 defines halting AMI_1:def 20 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is realistic means :Def21: :: AMI_1:def 21
the Instructions of a₂ <> the Instruction-Locations of a₂;

end;

:: deftheorem Def21 defines realistic AMI_1:def 21 :

theorem Th48: :: AMI_1:48

for b₁ being set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁ st b₂ is realistic holds
for b₃ being Instruction-Location of b₂ holds not IC b₂ = b₃

proof end;

theorem Th49: :: AMI_1:49

canceled;

theorem Th50: :: AMI_1:50

canceled;

theorem Th51: :: AMI_1:51

for b₁ being with_non-empty_elements set
for b₂ being Nat
for b₃ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₄ being State of b₃
for b₅ being Nat holds (Computation b₄) . (b₂ + b₅) = (Computation ((Computation b₄) . b₂)) . b₅

proof end;

theorem Th52: :: AMI_1:52

for b₁, b₂ being Nat st b₁ <= b₂ holds
for b₃ being with_non-empty_elements set
for b₄ being non empty non void halting IC-Ins-separated definite AMI-Struct of b₃
for b₅ being State of b₄ st CurInstr ((Computation b₅) . b₁) = halt b₄ holds
(Computation b₅) . b₂ = (Computation b₅) . b₁

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
assume E45: c₃ is halting ;
func Result c₃ -> State of a₂ means :Def22: :: AMI_1:def 22
ex b₁ being Nat st
( a₄ = (Computation a₃) . b₁ & CurInstr a₄ = halt a₂ );
uniqueness

proof end;

correctness

proof end;

end;

:: deftheorem Def22 defines Result AMI_1:def 22 :

theorem Th53: :: AMI_1:53

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Instruction-Location of b₂ holds b₃ . b₄ = (Following b₃) . b₄ by Def13;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void definite AMI-Struct of c₁;
let c₃ be State of c₂;
let c₄ be Instruction-Location of c₂;
redefine func . as c₃ . c₄ -> Instruction of a₂;
coherence

proof end;

end;

theorem Th54: :: AMI_1:54

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Instruction-Location of b₂
for b₅ being Nat holds b₃ . b₄ = ((Computation b₃) . b₅) . b₄

proof end;

theorem Th55: :: AMI_1:55

for b₁ being with_non-empty_elements set
for b₂ being Nat
for b₃ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₄ being State of b₃ holds (Computation b₄) . (b₂ + 1) = Exec (b₄ . (IC ((Computation b₄) . b₂))),((Computation b₄) . b₂)

proof end;

theorem Th56: :: AMI_1:56

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Nat st b₃ . (IC ((Computation b₃) . b₄)) = halt b₂ holds
Result b₃ = (Computation b₃) . b₄

proof end;

theorem Th57: :: AMI_1:57

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being State of b₂ st ex b₄ being Nat st b₃ . (IC ((Computation b₃) . b₄)) = halt b₂ holds
for b₄ being Nat holds Result b₃ = Result ((Computation b₃) . b₄)

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void AMI-Struct of c₁;
let c₃ be Object of c₂;
cluster ObjectKind a₃ -> non empty ;
coherence ;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
func FinPartSt c₂ -> Subset of (sproduct the Object-Kind of a₂) equals :: AMI_1:def 23
{ b₁ where B is Element of sproduct the Object-Kind of a₂ : b₁ is finite } ;
coherence

proof end;

end;

:: deftheorem Def23 defines FinPartSt AMI_1:def 23 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
mode FinPartState of c₂ -> Element of sproduct the Object-Kind of a₂ means :Def24: :: AMI_1:def 24
a₃ is finite;
existence

proof end;

end;

:: deftheorem Def24 defines FinPartState AMI_1:def 24 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
attr a₃ is autonomic means :Def25: :: AMI_1:def 25
for b₁, b₂ being State of a₂ st a₃ c= b₁ & a₃ c= b₂ holds
for b₃ being Nat holds ((Computation b₁) . b₃) | (dom a₃) = ((Computation b₂) . b₃) | (dom a₃);

end;

:: deftheorem Def25 defines autonomic AMI_1:def 25 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
attr a₃ is halting means :Def26: :: AMI_1:def 26
for b₁ being State of a₂ st a₃ c= b₁ holds
b₁ is halting;

end;

:: deftheorem Def26 defines halting AMI_1:def 26 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
attr a₂ is programmable means :Def27: :: AMI_1:def 27
ex b₁ being FinPartState of a₂ st
( not b₁ is empty & b₁ is autonomic );

end;

:: deftheorem Def27 defines programmable AMI_1:def 27 :

theorem Th58: :: AMI_1:58

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃, b₄ being set
for b₅, b₆ being Object of b₂ st ObjectKind b₅ = b₃ & ObjectKind b₆ = b₄ holds
for b₇ being Element of b₃
for b₈ being Element of b₄ holds b₅,b₆ --> b₇,b₈ is FinPartState of b₂

proof end;

theorem Th59: :: AMI_1:59

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃ being set
for b₄ being Object of b₂ st ObjectKind b₄ = b₃ holds
for b₅ being Element of b₃ holds b₄ .--> b₅ is FinPartState of b₂

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be Object of c₂;
let c₄ be Element of ObjectKind c₃;
redefine func .--> as c₃ .--> c₄ -> FinPartState of a₂;
coherence by Th59;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃, c₄ be Object of c₂;
let c₅ be Element of ObjectKind c₃;
let c₆ be Element of ObjectKind c₄;
redefine func --> as c₃,c₄ --> c₅,c₆ -> FinPartState of a₂;
coherence by Th58;

end;

theorem Th60: :: AMI_1:60

for b₁ being set holds Trivial-AMI b₁ is realistic

proof end;

theorem Th61: :: AMI_1:61

for b₁ being with_non-empty_elements set holds Trivial-AMI b₁ is programmable

proof end;

registration

let c₁ be set ;
cluster Trivial-AMI a₁ -> non empty strict non void IC-Ins-separated data-oriented definite realistic ;
coherence by Th60;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster Trivial-AMI a₁ -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic programmable ;
coherence by Th61;

end;

registration

let c₁ be set ;
cluster strict data-oriented realistic AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
cluster non empty strict non void IC-Ins-separated data-oriented definite realistic AMI-Struct of a₁;
existence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite realistic programmable AMI-Struct of a₁;
existence

proof end;

end;

theorem Th62: :: AMI_1:62

for b₁ being with_non-empty_elements set
for b₂ being non void AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being FinPartState of b₂ holds b₃ | (dom b₄) is FinPartState of b₂

proof end;

theorem Th63: :: AMI_1:63

for b₁ being set
for b₂ being AMI-Struct of b₁ holds {} is FinPartState of b₂

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite programmable AMI-Struct of c₁;
cluster non empty autonomic FinPartState of a₂;
existence by Def27;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃, c₄ be FinPartState of c₂;
redefine func +* as c₃ +* c₄ -> FinPartState of a₂;
coherence

proof end;

end;

theorem Th64: :: AMI_1:64

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃ being Instruction-Location of b₂
for b₄ being Element of ObjectKind (IC b₂) st b₄ = b₃ holds
for b₅ being Element of ObjectKind b₃ st b₅ = halt b₂ holds
for b₆ being State of b₂ st (IC b₂),b₃ --> b₄,b₅ c= b₆ holds
CurInstr b₆ = halt b₂

proof end;

theorem Th65: :: AMI_1:65

proof end;

theorem Th66: :: AMI_1:66

proof end;

theorem Th67: :: AMI_1:67

proof end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of c₁;
cluster autonomic halting FinPartState of a₂;
existence

proof end;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of c₁;
mode pre-program of a₂ is autonomic halting FinPartState of a₂;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
assume E62: c₃ is pre-program of c₂ ;
func Result c₃ -> FinPartState of a₂ means :: AMI_1:def 28
for b₁ being State of a₂ st a₃ c= b₁ holds
a₄ = (Result b₁) | (dom a₃);
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def28 defines Result AMI_1:def 28 :

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of c₁;
let c₃ be FinPartState of c₂;
let c₄ be Function;
pred c₃ computes c₄ means :Def29: :: AMI_1:def 29
for b₁ being set st b₁ in dom a₄ holds
ex b₂ being FinPartState of a₂ st
( b₁ = b₂ & a₃ +* b₂ is pre-program of a₂ & a₄ . b₂ c= Result (a₃ +* b₂) );

end;

:: deftheorem Def29 defines computes AMI_1:def 29 :

notation

end;

theorem Th68: :: AMI_1:68

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃ being FinPartState of b₂ holds b₃ computes {}

proof end;

theorem Th69: :: AMI_1:69

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃ being FinPartState of b₂ holds
( b₃ is pre-program of b₂ iff b₃ computes {} .--> (Result b₃) )

proof end;

theorem Th70: :: AMI_1:70

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of c₁;
let c₃ be PartFunc of FinPartSt c₂, FinPartSt c₂;
attr a₃ is computable means :Def30: :: AMI_1:def 30
ex b₁ being FinPartState of a₂ st b₁ computes a₃;

end;

:: deftheorem Def30 defines computable AMI_1:def 30 :

theorem Th71: :: AMI_1:71

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃ being PartFunc of FinPartSt b₂, FinPartSt b₂ st b₃ = {} holds
b₃ is computable

proof end;

theorem Th72: :: AMI_1:72

proof end;

theorem Th73: :: AMI_1:73

for b₁ being with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of b₁
for b₃ being pre-program of b₂
for b₄ being PartFunc of FinPartSt b₂, FinPartSt b₂ st b₄ = {} .--> (Result b₃) holds
b₄ is computable

proof end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of c₁;
let c₃ be PartFunc of FinPartSt c₂, FinPartSt c₂;
assume E70: c₃ is computable ;
mode Program of c₃ -> FinPartState of a₂ means :: AMI_1:def 31
a₄ computes a₃;
existence by E70, Def30;

end;

:: deftheorem Def31 defines Program AMI_1:def 31 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
mode InsType of a₂ is Element of the Instruction-Codes of a₂;

end;

theorem Th74: :: AMI_1:74

proof end;

theorem Th75: :: AMI_1:75

proof end;

theorem Th76: :: AMI_1:76

proof end;