:: AMI_1 semantic presentation

definition
let IL, N be set ;
attr c3 is strict;
struct AMI-Struct of IL,N -> 1-sorted ;
aggr AMI-Struct(# carrier, Instruction-Counter, Instructions, Object-Kind, Execution #) -> AMI-Struct of IL,N;
sel Instruction-Counter c3 -> Element of the carrier of c3;
sel Instructions c3 -> non empty set ;
sel Object-Kind c3 -> Function of the carrier of c3,N \/ {the Instructions of c3,IL};
sel Execution c3 -> Function of the Instructions of c3, Funcs (product the Object-Kind of c3),(product the Object-Kind of c3);
end;

definition
let IL, N be set ;
canceled;
func Trivial-AMI IL,N -> strict AMI-Struct of IL,N means :Def2: :: AMI_1:def 2
( the carrier of it = succ IL & the Instruction-Counter of it = IL & the Instructions of it = {[0 ,{} ]} & the Object-Kind of it = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of it = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) );
existence
ex b1 being strict AMI-Struct of IL,N st
( the carrier of b1 = succ IL & the Instruction-Counter of b1 = IL & the Instructions of b1 = {[0 ,{} ]} & the Object-Kind of b1 = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of b1 = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct of IL,N st the carrier of b1 = succ IL & the Instruction-Counter of b1 = IL & the Instructions of b1 = {[0 ,{} ]} & the Object-Kind of b1 = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of b1 = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) & the carrier of b2 = succ IL & the Instruction-Counter of b2 = IL & the Instructions of b2 = {[0 ,{} ]} & the Object-Kind of b2 = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of b2 = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) holds
b1 = b2 ;
end;

:: deftheorem AMI_1:def 1 :
canceled;

:: deftheorem Def2 defines Trivial-AMI AMI_1:def 2 :
for IL, N being set
for b3 being strict AMI-Struct of IL,N holds
( b3 = Trivial-AMI IL,N iff ( the carrier of b3 = succ IL & the Instruction-Counter of b3 = IL & the Instructions of b3 = {[0 ,{} ]} & the Object-Kind of b3 = (IL --> {[0 ,{} ]}) +* (IL .--> IL) & the Execution of b3 = [0 ,{} ] .--> (id (product ((IL --> {[0 ,{} ]}) +* (IL .--> IL)))) ) );

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
attr S is stored-program means :Def3: :: AMI_1:def 3
IL c= the carrier of S;
end;

:: deftheorem Def3 defines stored-program AMI_1:def 3 :
for IL, N being set
for S being AMI-Struct of IL,N holds
( S is stored-program iff IL c= the carrier of S );

registration
let IL, N be set ;
cluster Trivial-AMI IL,N -> non empty strict stored-program ;
coherence
( not Trivial-AMI IL,N is empty & Trivial-AMI IL,N is stored-program )
proof end;
end;

registration
let IL, N be set ;
cluster non empty stored-program AMI-Struct of IL,N;
existence
ex b1 being AMI-Struct of IL,N st
( not b1 is empty & b1 is stored-program )
proof end;
end;

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

definition
let IL be non empty set ;
let N be set ;
let S be AMI-Struct of IL,N;
mode Instruction-Location of S -> set means :Def4: :: AMI_1:def 4
it in IL;
existence
ex b1 being set st b1 in IL by XBOOLE_0:def 1;
end;

:: deftheorem Def4 defines Instruction-Location AMI_1:def 4 :
for IL being non empty set
for N being set
for S being AMI-Struct of IL,N
for b4 being set holds
( b4 is Instruction-Location of S iff b4 in IL );

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

definition
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
func IC S -> Object of S equals :: AMI_1:def 5
the Instruction-Counter of S;
correctness
coherence
the Instruction-Counter of S is Object of S;
;
end;

:: deftheorem defines IC AMI_1:def 5 :
for IL, N being set
for S being non empty AMI-Struct of IL,N holds IC S = the Instruction-Counter of S;

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

:: deftheorem defines ObjectKind AMI_1:def 6 :
for IL, N being set
for S being non empty AMI-Struct of IL,N
for o being Object of S holds ObjectKind o = the Object-Kind of S . o;

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

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be AMI-Struct of IL,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
(the Execution of S . I) . s is State of S
proof end;
end;

:: deftheorem defines Exec AMI_1:def 7 :
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for I being Instruction of S
for s being State of S holds Exec I,s = (the Execution of S . I) . s;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be AMI-Struct of IL,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 :
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for I being Instruction of S holds
( I is halting iff for s being State of S holds Exec I,s = s );

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be AMI-Struct of IL,N;
attr S is halting means :Def9: :: AMI_1:def 9
 ex I being Instruction of S st I is halting;
end;

:: deftheorem Def9 defines halting AMI_1:def 9 :
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N holds
( S is halting iff ex I being Instruction of S st I is halting );

theorem :: AMI_1:1
canceled;

theorem :: AMI_1:2
canceled;

theorem :: AMI_1:3
canceled;

theorem :: AMI_1:4
canceled;

theorem :: AMI_1:5
canceled;

theorem Th6: :: AMI_1:6
for IL being non empty set
for N being with_non-empty_elements set holds Trivial-AMI IL,N is halting
proof end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster Trivial-AMI IL,N -> strict halting ;
coherence
Trivial-AMI IL,N is halting by Th6;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster halting AMI-Struct of IL,N;
existence
ex b1 being AMI-Struct of IL,N st b1 is halting
proof end;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of IL,N;
cluster halting Element of the Instructions of S;
existence
ex b1 being Instruction of S st b1 is halting by Def9;
end;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of IL,N;
func halt S -> Instruction of S equals :: AMI_1:def 10
 choose { I where I is Instruction of S : I is halting } ;
coherence
choose { I where I is Instruction of S : I is halting } is Instruction of S
proof end;
end;

:: deftheorem defines halt AMI_1:def 10 :
for IL being non empty set
for N being with_non-empty_elements set
for S being halting AMI-Struct of IL,N holds halt S = choose { I where I is Instruction of S : I is halting } ;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of IL,N;
cluster halt S -> halting ;
coherence
halt S is halting
proof end;
end;

definition
let IL, N be set ;
let IT be non empty AMI-Struct of IL,N;
attr IT is IC-Ins-separated means :Def11: :: AMI_1:def 11
 ObjectKind (IC IT) = IL;
end;

:: deftheorem Def11 defines IC-Ins-separated AMI_1:def 11 :
for IL, N being set
for IT being non empty AMI-Struct of IL,N holds
( IT is IC-Ins-separated iff ObjectKind (IC IT) = IL );

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let IT be non empty AMI-Struct of IL,N;
canceled;
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 AMI_1:def 12 :
canceled;

:: deftheorem Def13 defines steady-programmed AMI_1:def 13 :
for IL being non empty set
for N being with_non-empty_elements set
for IT being non empty AMI-Struct of IL,N holds
( IT is steady-programmed iff 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 );

definition
let IL be non empty set ;
let N be set ;
let IT be non empty stored-program AMI-Struct of IL,N;
:: original: Instruction-Location
redefine mode Instruction-Location of IT -> Element of IT;
coherence
for b1 being Instruction-Location of IT holds b1 is Element of IT
proof end;
end;

definition
let IL be non empty set ;
let N be set ;
let IT be non empty stored-program AMI-Struct of IL,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 :
for IL being non empty set
for N being set
for IT being non empty stored-program AMI-Struct of IL,N holds
( IT is definite iff for l being Instruction-Location of IT holds ObjectKind l = the Instructions of IT );

theorem Th7: :: AMI_1:7
for IL being non empty set
for E being set holds Trivial-AMI IL,E is IC-Ins-separated
proof end;

theorem :: AMI_1:8
canceled;

theorem Th9: :: AMI_1:9
for IL being non empty set
for N being with_non-empty_elements set
for s being State of (Trivial-AMI IL,N)
for i being Instruction of (Trivial-AMI IL,N) holds Exec i,s = s
proof end;

theorem Th10: :: AMI_1:10
for IL being non empty set
for N being with_non-empty_elements set holds Trivial-AMI IL,N is steady-programmed
proof end;

theorem Th11: :: AMI_1:11
for IL being non empty set
for E being set holds Trivial-AMI IL,E is definite
proof end;

registration
let IL be non empty set ;
let E be set ;
cluster Trivial-AMI IL,E -> strict IC-Ins-separated definite ;
coherence
( Trivial-AMI IL,E is IC-Ins-separated & Trivial-AMI IL,E is definite ) by Th7, Th11;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster Trivial-AMI IL,N -> strict steady-programmed ;
coherence
Trivial-AMI IL,N is steady-programmed by Th10;
end;

registration
let IL, E be set ;
cluster strict AMI-Struct of IL,E;
existence
ex b1 being AMI-Struct of IL,E st b1 is strict
proof end;
end;

registration
let IL be non empty set ;
let M be set ;
cluster non empty strict stored-program IC-Ins-separated definite AMI-Struct of IL,M;
existence
ex b1 being non empty stored-program AMI-Struct of IL,M st
( b1 is IC-Ins-separated & b1 is definite & b1 is strict )
proof end;
end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster non empty strict stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N;
existence
ex b1 being non empty stored-program AMI-Struct of IL,N st
( b1 is IC-Ins-separated & b1 is halting & b1 is steady-programmed & b1 is definite & b1 is strict )
proof end;
end;

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

:: deftheorem defines IC AMI_1:def 15 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for s being State of S holds IC s = s . (IC S);

theorem :: AMI_1:12
for IL being non empty set
for N being with_non-empty_elements set
for s1, s2 being State of (Trivial-AMI IL,N) st IC s1 = IC s2 holds
s1 = s2
proof end;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated AMI-Struct of IL,N;
let s be State of S;
:: original: IC
redefine func IC s -> Instruction-Location of S;
coherence
IC s is Instruction-Location of S ;
end;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
canceled;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N;
let s be State of S;
func CurInstr s -> Instruction of S equals :: AMI_1:def 17
s . (IC s);
coherence
s . (IC s) is Instruction of S
proof end;
end;

:: deftheorem AMI_1:def 16 :
canceled;

:: deftheorem defines CurInstr AMI_1:def 17 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for s being State of S holds CurInstr s = s . (IC s);

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

:: deftheorem defines Following AMI_1:def 18 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for s being State of S holds Following s = Exec (CurInstr s),s;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,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 Element of NAT holds it . (i + 1) = Following (it . i) ) );
existence
ex b1 being Function of NAT , product the Object-Kind of S st
( b1 . 0 = s & ( for i being Element of NAT holds b1 . (i + 1) = Following (b1 . i) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , product the Object-Kind of S st b1 . 0 = s & ( for i being Element of NAT holds b1 . (i + 1) = Following (b1 . i) ) & b2 . 0 = s & ( for i being Element of NAT holds b2 . (i + 1) = Following (b2 . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines Computation AMI_1:def 19 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for s being State of S
for b5 being Function of NAT , product the Object-Kind of S holds
( b5 = Computation s iff ( b5 . 0 = s & ( for i being Element of NAT holds b5 . (i + 1) = Following (b5 . i) ) ) );

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

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

:: deftheorem Def20 defines halting AMI_1:def 20 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of IL,N
for IT being State of S holds
( IT is halting iff ex k being Element of NAT st CurInstr ((Computation IT) . k) = halt S );

definition
let IL, N be set ;
let IT be AMI-Struct of IL,N;
attr IT is realistic means :Def21: :: AMI_1:def 21
not the Instruction-Counter of IT in IL;
end;

:: deftheorem Def21 defines realistic AMI_1:def 21 :
for IL, N being set
for IT being AMI-Struct of IL,N holds
( IT is realistic iff not the Instruction-Counter of IT in IL );

theorem :: AMI_1:13
canceled;

theorem :: AMI_1:14
canceled;

theorem :: AMI_1:15
canceled;

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 :: AMI_1:25
canceled;

theorem :: AMI_1:26
canceled;

theorem :: AMI_1:27
canceled;

theorem :: AMI_1:28
canceled;

theorem :: AMI_1:29
canceled;

theorem :: AMI_1:30
canceled;

theorem :: AMI_1:31
canceled;

theorem :: AMI_1:32
canceled;

theorem :: AMI_1:33
canceled;

theorem :: AMI_1:34
canceled;

theorem :: AMI_1:35
canceled;

theorem :: AMI_1:36
canceled;

theorem :: AMI_1:37
canceled;

theorem :: AMI_1:38
canceled;

theorem :: AMI_1:39
canceled;

theorem :: AMI_1:40
canceled;

theorem :: AMI_1:41
canceled;

theorem :: AMI_1:42
canceled;

theorem :: AMI_1:43
canceled;

theorem :: AMI_1:44
canceled;

theorem :: AMI_1:45
canceled;

theorem :: AMI_1:46
canceled;

theorem :: AMI_1:47
canceled;

theorem Th48: :: AMI_1:48
for IL being non empty set
for E being set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,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 IL being non empty set
for N being with_non-empty_elements set
for i being Element of NAT
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for s being State of S
for k being Element of NAT holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k
proof end;

theorem Th52: :: AMI_1:52
for i, j being Element of NAT st i <= j holds
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite AMI-Struct of IL,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 IL be non empty set ;
l