:: AMI_1 semantic presentation

theorem :: AMI_1:1

canceled;

theorem Th2: :: 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;

theorem :: AMI_1:4

canceled;

theorem Th5: :: AMI_1:5

for a, b, c, d being set st a <> b holds
product (a,b --> {c},{d}) = {(a,b --> c,d)}

proof end;

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 :

registration

let f be Function;
cluster product f -> functional ;
coherence

proof end;

end;

registration

let A be set ;
let B be with_non-empty_elements set ;
let f be Function of A,B;
cluster product f -> non empty functional ;
coherence

proof end;

end;

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 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;

theorem :: AMI_1:16

canceled;

theorem :: AMI_1:17

canceled;

theorem Th18: :: AMI_1:18

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

theorem Th19: :: AMI_1:19

for x, y being set holds x .--> y = {[x,y]}

proof end;

theorem Th20: :: AMI_1:20

for a, b, c being set holds a,a --> b,c = a .--> c

proof end;

theorem :: AMI_1:21

canceled;

theorem :: AMI_1:22

for x being set
for f being Function st x in product f holds
x is Function

proof end;

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: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 sproduct (f +* g)

proof end;

theorem :: AMI_1:45

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

proof end;

theorem Th46: :: AMI_1:46

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

proof end;

theorem :: AMI_1:47

for f being Function
for x1, x2, y1, y2 being set st x1 in dom f & y1 in f . x1 & x2 in dom f & y2 in f . x2 holds
x1,x2 --> y1,y2 in sproduct f

proof end;

definition

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

proof end;

end;

:: deftheorem defines CurInstr AMI_1:def 17 :

definition

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

end;

:: deftheorem defines Following AMI_1:def 18 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines Computation AMI_1:def 19 :

definition

let N be with_non-empty_elements set ;
let S be non void AMI-Struct of N;
let f be Function of NAT , product the Object-Kind of S;
let k be Nat;
:: original: .
redefine func f . k -> State of S;
coherence by FUNCT_2:7;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite AMI-Struct of N;
let IT be State of S;
attr IT is halting means :Def20: :: AMI_1:def 20
ex k being Nat st CurInstr ((Computation IT) . k) = halt S;

end;

:: deftheorem Def20 defines halting AMI_1:def 20 :

definition

let N be set ;
let IT be AMI-Struct of N;
attr IT is realistic means :Def21: :: AMI_1:def 21
the Instructions of IT <> the Instruction-Locations of IT;

end;

:: deftheorem Def21 defines realistic AMI_1:def 21 :

theorem Th48: :: AMI_1:48

for E being set
for S being non empty non void IC-Ins-separated definite AMI-Struct of E st S is realistic holds
for l being Instruction-Location of S holds not IC S = l

proof end;

theorem :: AMI_1:49

canceled;

theorem :: AMI_1:50

canceled;

theorem Th51: :: AMI_1:51

for N being with_non-empty_elements set
for i being Nat
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for s being State of S
for k being Nat holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k

proof end;

theorem Th52: :: AMI_1:52

for i, j being Nat st i <= j holds
for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite AMI-Struct of N
for s being State of S st CurInstr ((Computation s) . i) = halt S holds
(Computation s) . j = (Computation s) . i

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite AMI-Struct of N;
let s be State of S;
assume A1: s is halting ;
func Result s -> State of S means :Def22: :: AMI_1:def 22
ex k being Nat st
( it = (Computation s) . k & CurInstr it = halt S );
uniqueness

proof end;

correctness

proof end;

end;

:: deftheorem Def22 defines Result AMI_1:def 22 :

theorem :: AMI_1:53

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for i being Instruction-Location of S holds s . i = (Following s) . i by Def13;

definition

let N be with_non-empty_elements set ;
let S be non empty non void definite AMI-Struct of N;
let s be State of S;
let l be Instruction-Location of S;
:: original: .
redefine func s . l -> Instruction of S;
coherence

proof end;

end;

theorem Th54: :: AMI_1:54

proof end;

theorem :: AMI_1:55

for N being with_non-empty_elements set
for k being Nat
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S holds (Computation s) . (k + 1) = Exec (s . (IC ((Computation s) . k))),((Computation s) . k)

proof end;

theorem Th56: :: AMI_1:56

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for k being Nat st s . (IC ((Computation s) . k)) = halt S holds
Result s = (Computation s) . k

proof end;

theorem :: AMI_1:57

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S st ex k being Nat st s . (IC ((Computation s) . k)) = halt S holds
for i being Nat holds Result s = Result ((Computation s) . i)

proof end;

registration

let N be with_non-empty_elements set ;
let S be non empty non void AMI-Struct of N;
let o be Object of S;
cluster ObjectKind o -> non empty ;
coherence ;

end;

definition

let N be set ;
let S be AMI-Struct of N;
func FinPartSt S -> Subset of (sproduct the Object-Kind of S) equals :: AMI_1:def 23
{ p where p is Element of sproduct the Object-Kind of S : p is finite } ;
coherence

proof end;

end;

:: deftheorem defines FinPartSt AMI_1:def 23 :

definition

let N be set ;
let S be AMI-Struct of N;
mode FinPartState of S -> Element of sproduct the Object-Kind of S means :Def24: :: AMI_1:def 24
it is finite;
existence

proof end;

end;

:: deftheorem Def24 defines FinPartState AMI_1:def 24 :

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let IT be FinPartState of S;
attr IT is autonomic means :Def25: :: AMI_1:def 25
for s1, s2 being State of S st IT c= s1 & IT c= s2 holds
for i being Nat holds ((Computation s1) . i) | (dom IT) = ((Computation s2) . i) | (dom IT);

end;

:: deftheorem Def25 defines autonomic AMI_1:def 25 :

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite AMI-Struct of N;
let IT be FinPartState of S;
attr IT is halting means :Def26: :: AMI_1:def 26
for s being State of S st IT c= s holds
s is halting;

end;

:: deftheorem Def26 defines halting AMI_1:def 26 :

definition

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

end;

:: deftheorem Def27 defines programmable AMI_1:def 27 :

theorem Th58: :: AMI_1:58

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for A, B being set
for la, lb being Object of S st ObjectKind la = A & ObjectKind lb = B holds
for a being Element of A
for b being Element of B holds la,lb --> a,b is FinPartState of S

proof end;

theorem Th59: :: AMI_1:59

for N being with_non-empty_elements set
for S being non empty non void IC-Ins-separated definite AMI-Struct of N
for A being set
for la being Object of S st ObjectKind la = A holds
for a being Element of A holds la .--> a is FinPartState of S

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let la be Object of S;
let a be Element of ObjectKind la;
:: original: .-->
redefine func la .--> a -> FinPartState of S;
coherence by Th59;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let la, lb be Object of S;
let a be Element of ObjectKind la;
let b be Element of ObjectKind lb;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of S;
coherence by Th58;

end;

theorem Th60: :: AMI_1:60

for E being set holds Trivial-AMI E is realistic

proof end;

theorem Th61: :: AMI_1:61

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

proof end;

registration

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

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 realistic programmable ;
coherence by Th61;

end;

registration

let E be set ;
cluster strict data-oriented realistic 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 realistic 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 realistic programmable AMI-Struct of N;
existence

proof end;

end;

theorem Th62: :: AMI_1:62

for N being with_non-empty_elements set
for S being non void AMI-Struct of N
for s being State of S
for p being FinPartState of S holds s | (dom p) is FinPartState of S

proof end;

theorem Th63: :: AMI_1:63

for N being set
for S being AMI-Struct of N holds {} is FinPartState of S

proof end;

registration

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

end;

definition

let N be set ;
let S be AMI-Struct of N;
let f, g be FinPartState of S;
:: original: +*
redefine func f +* g -> FinPartState of S;
coherence

proof end;

end;

theorem Th64: :: AMI_1:64

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N
for loc being Instruction-Location of S
for l being Element of ObjectKind (IC S) st l = loc holds
for h being Element of ObjectKind loc st h = halt S holds
for s being State of S st (IC S),loc --> l,h c= s holds
CurInstr s = halt S

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 N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N;
cluster autonomic halting FinPartState of S;
existence

proof end;

end;

definition

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

end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N;
let s be FinPartState of S;
assume A1: s is pre-program of S ;
func Result s -> FinPartState of S means :: AMI_1:def 28
for s' being State of S st s c= s' holds
it = (Result s') | (dom s);
existence

proof end;

correctness

proof end;

end;

:: deftheorem defines Result AMI_1:def 28 :

definition

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

end;

:: deftheorem Def29 defines computes AMI_1:def 29 :

notation

end;

theorem Th68: :: AMI_1:68

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S holds p computes {}

proof end;

theorem Th69: :: AMI_1:69

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

proof end;

theorem Th70: :: AMI_1:70

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N;
let IT be PartFunc of FinPartSt S, FinPartSt S;
attr IT is computable means :Def30: :: AMI_1:def 30
ex p being FinPartState of S st p computes IT;

end;

:: deftheorem Def30 defines computable AMI_1:def 30 :

theorem Th71: :: AMI_1:71

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

proof end;

theorem Th72: :: AMI_1:72

proof end;

theorem Th73: :: AMI_1:73

for N being with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N
for p being pre-program of S
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> (Result p) holds
F is computable

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty non void halting IC-Ins-separated definite realistic AMI-Struct of N;
let F be PartFunc of FinPartSt S, FinPartSt S;
assume A1: F is computable ;
mode Program of F -> FinPartState of S means :: AMI_1:def 31
it computes F;
existence by A1, Def30;

end;

:: deftheorem defines Program AMI_1:def 31 :

definition

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

end;

theorem :: AMI_1:74

proof end;

theorem :: AMI_1:75

proof end;

theorem :: AMI_1:76

proof end;