:: AMI_1 semantic presentation

theorem :: AMI_1:1

canceled;

theorem :: AMI_1:2

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

theorem :: AMI_1:3

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

definition

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

end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem AMI_1:def 1 :

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

definition

let N be set ;
let S be AMI-Struct of N;
attr S is void means :Def3: :: AMI_1:def 3
the Instruction-Locations of S is empty;

end;

:: deftheorem Def3 defines void AMI_1:def 3 :

registration

let N be set ;
cluster Trivial-AMI N -> non empty strict non void ;
coherence

proof end;

end;

registration

let N be set ;
cluster non empty non void AMI-Struct of N;
existence

proof end;

end;

registration

let N be set ;
let S be non void AMI-Struct of N;
cluster the Instruction-Locations of S -> non empty ;
coherence by Def3;

end;

definition

let N be set ;
let S be non empty AMI-Struct of N;
mode Object of S is Element of S;

end;

definition

let N be set ;
let S be non empty non void AMI-Struct of N;
mode Instruction-Location of S is Element of the Instruction-Locations of S;

end;

definition

let N be set ;
let S be AMI-Struct of N;
mode Instruction of S is Element of the Instructions of S;

end;

definition

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

end;

:: deftheorem AMI_1:def 4 :

:: deftheorem defines IC AMI_1:def 5 :

definition

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

end;

:: deftheorem defines ObjectKind AMI_1:def 6 :

definition

let N be set ;
let S be AMI-Struct of N;
mode State of S is Element of product the Object-Kind of S;

end;

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
let I be Instruction of S;
let s be State of S;
func Exec I,s -> State of S equals :: AMI_1:def 7
(the Execution of S . I) . s;
coherence

proof end;

end;

:: deftheorem defines Exec AMI_1:def 7 :

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
let I be Instruction of S;
attr I is halting means :Def8: :: AMI_1:def 8
for s being State of S holds Exec I,s = s;

end;

:: deftheorem Def8 defines halting AMI_1:def 8 :

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
attr S is halting means :Def9: :: AMI_1:def 9
ex I being Instruction of S st
( I is halting & ( for J being Instruction of S st J is halting holds
I = J ) );

end;

:: deftheorem Def9 defines halting AMI_1:def 9 :

theorem :: AMI_1:4

canceled;

theorem :: AMI_1:5

canceled;

theorem Th6: :: AMI_1:6

for N being with_non-empty_elements set holds Trivial-AMI N is halting

proof end;

registration

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

end;

registration

let N be with_non-empty_elements set ;
cluster non void halting AMI-Struct of N;
existence

proof end;

end;

registration

let N be with_non-empty_elements set ;
let S be non void halting AMI-Struct of N;
cluster halting Element of the Instructions of S;
existence

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non void halting AMI-Struct of N;
func halt S -> Instruction of S means :Def10: :: AMI_1:def 10
it is halting Instruction of S;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines halt AMI_1:def 10 :

registration

let N be with_non-empty_elements set ;
let S be non void halting AMI-Struct of N;
cluster halt S -> halting ;
coherence by Def10;

end;

definition

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

end;

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

definition

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

end;

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

definition

let N be with_non-empty_elements set ;
let IT be non empty non void AMI-Struct of N;
attr IT is steady-programmed means :Def13: :: AMI_1:def 13
for s being State of IT
for i being Instruction of IT
for l being Instruction-Location of IT holds (Exec i,s) . l = s . l;

end;

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

definition

let N be set ;
let IT be non empty non void AMI-Struct of N;
attr IT is definite means :Def14: :: AMI_1:def 14
for l being Instruction-Location of IT holds ObjectKind l = the Instructions of IT;

end;

:: deftheorem Def14 defines definite AMI_1:def 14 :

theorem Th7: :: AMI_1:7

for E being set holds Trivial-AMI E is IC-Ins-separated

proof end;

theorem Th8: :: AMI_1:8

for E being set holds Trivial-AMI E is data-oriented

proof end;

theorem Th9: :: AMI_1:9

for E being set
for s1, s2 being State of (Trivial-AMI E) holds s1 = s2

proof end;

theorem Th10: :: AMI_1:10

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

proof end;

theorem Th11: :: AMI_1:11

for E being set holds Trivial-AMI E is definite

proof end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

let E be set ;
cluster strict data-oriented AMI-Struct of E;
existence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated AMI-Struct of N;
let s be State of S;
func IC s -> Instruction-Location of S equals :: AMI_1:def 15
s . (IC S);
coherence

proof end;

end;

:: deftheorem defines IC AMI_1:def 15 :

theorem :: AMI_1:12

canceled;

theorem :: AMI_1:13

canceled;

theorem Th14: :: AMI_1:14

for x, y, z being set
for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds
y = z

proof end;

theorem Th15: :: AMI_1:15

for A being set st ( for x being set st x in A holds
x is Function ) & ( for f, g being Function st f in A & g in A holds
f tolerates g ) holds
union A is Function

proof end;

Lm1: for x1, x2, y1, y2 being set holds x1,x2 --> y1,y2 = (x1 .--> y1) +* (x2 .--> y2)
by FUNCT_4:def 4;

Lm2: for x, y being set holds x .--> y = {[x,y]}
by CQC_LANG:45;

definition

let f be Function;
func sproduct f -> set means :Def16: :: AMI_1:def 16
for x being set holds
( x in it iff ex g being Function st
( x = g & dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines sproduct AMI_1:def 16 :

registration

let f be Function;
cluster sproduct f -> non empty functional ;
coherence

proof end;

end;

theorem :: AMI_1:16

canceled;

theorem :: AMI_1:17

canceled;

theorem :: AMI_1:18

canceled;

theorem :: AMI_1:19

canceled;

theorem :: AMI_1:20

canceled;

theorem :: AMI_1:21

canceled;

theorem :: AMI_1:22

canceled;

theorem :: AMI_1:23

canceled;

theorem :: AMI_1:24

canceled;

theorem Th25: :: AMI_1:25

for g, f being Function st g in sproduct f holds
( dom g c= dom f & ( for x being set st x in dom g holds
g . x in f . x ) )

proof end;

theorem Th26: :: AMI_1:26

for f being Function holds {} in sproduct f

proof end;

theorem Th27: :: AMI_1:27

for f being Function holds product f c= sproduct f

proof end;

theorem Th28: :: AMI_1:28

for x being set
for f being Function st x in sproduct f holds
x is PartFunc of dom f, union (rng f)

proof end;

theorem Th29: :: AMI_1:29

for g, f, h being Function st g in product f & h in sproduct f holds
g +* h in product f

proof end;

theorem Th30: :: AMI_1:30

for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f & g <= h ) )

proof end;

theorem Th31: :: AMI_1:31

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

proof end;

theorem Th32: :: AMI_1:32

for f, g being Function st f c= g holds
sproduct f c= sproduct g

proof end;

theorem Th33: :: AMI_1:33

sproduct {} = {{} }

proof end;

theorem :: AMI_1:34

for A, B being set holds PFuncs A,B = sproduct (A --> B)

proof end;

theorem :: AMI_1:35

for A, B being non empty set
for f being Function of A,B holds sproduct f = sproduct (f | { x where x is Element of A : f . x <> {} } )

proof end;

theorem Th36: :: AMI_1:36

for x, y being set
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f

proof end;

theorem :: AMI_1:37

for f being Function holds
( sproduct f = {{} } iff for x being set st x in dom f holds
f . x = {} )

proof end;

theorem Th38: :: AMI_1:38

for A being set
for f being Function st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f

proof end;

theorem :: AMI_1:39

for g, h, f being Function st g tolerates h & g in sproduct f & h in sproduct f holds
g \/ h in sproduct f

proof end;

theorem Th40: :: AMI_1:40

for g, h, f being Function st g c= h & h in sproduct f holds
g in sproduct f

proof end;

theorem Th41: :: AMI_1:41

for A being set
for g, f being Function st g in sproduct f holds
g | A in sproduct f

proof end;

theorem Th42: :: AMI_1:42

for A being set
for g, f being Function st g in sproduct f holds
g | A in sproduct (f | A)

proof end;

theorem :: AMI_1:43

for h, f, g being Function st h in sproduct (f +* g) holds
ex f', g' being Function st
( f' in sproduct f & g' in sproduct g & h = f' +* g' )

proof end;

theorem Th44: :: AMI_1:44

for g, f, f', g' being Function st dom g misses (dom f') \ (dom g') & f' in sproduct f & g' in sproduct g holds
f' +* g' in