:: A Mathematical Model of CPU
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received October 14, 1992
:: Copyright (c) 1992 Association of Mizar Users


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 be non empty set ;
let N be set ;
let S be AMI-Struct of IL,N;
:: original: Instruction-Location
redefine mode Instruction-Location of S -> Element of IL;
coherence
for b1 being Instruction-Location of S holds b1 is Element of IL by Def4;
end;

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;
deffunc H1( set , Element of product the Object-Kind of S) -> State of S = Following $2;
let s be State of S;
let k be Nat;
func Computation s,k -> State of S means :Def19: :: AMI_1:def 19
 ex f being Function of NAT , product the Object-Kind of S st
( it = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) );
existence
ex b1 being State of S ex f being Function of NAT , product the Object-Kind of S st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) )
proof end;
uniqueness
for b1, b2 being State of S st ex f being Function of NAT , product the Object-Kind of S st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . i) ) ) & ex f being Function of NAT , product the Object-Kind of S st
( b2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . 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 k being Nat
for b6 being State of S holds
( b6 = Computation s,k iff ex f being Function of NAT , product the Object-Kind of S st
( b6 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (f . 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 Tx0: :: AMI_1:13
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 Computation s,0 = s
proof end;

theorem Tx1: :: AMI_1:14
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 k being Nat holds Computation s,(k + 1) = Following (Computation s,k)
proof end;

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 IC-Ins-separated AMI-Struct of IL,E st S is realistic holds
for l being Instruction-Location of S holds not IC S = l by Def21;

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 ;
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 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 Element of NAT st
( it = Computation s,k & CurInstr it = halt S );
uniqueness
for b1, b2 being State of S st ex k being Element of NAT st
( b1 = Computation s,k & CurInstr b1 = halt S ) & ex k being Element of NAT st
( b2 = Computation s,k & CurInstr b2 = halt S ) holds
b1 = b2
proof end;
correctness
existence
ex b1 being State of S ex k being Element of NAT st
( b1 = Computation s,k & CurInstr b1 = halt S );
proof end;
end;

:: deftheorem Def22 defines Result AMI_1:def 22 :
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 s is halting holds
for b5 being State of S holds
( b5 = Result s iff ex k being Element of NAT st
( b5 = Computation s,k & CurInstr b5 = halt S ) );

theorem :: AMI_1:53
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for i being Instruction-Location of S holds s . i = (Following s) . i by Def13;

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

theorem Th54: :: AMI_1:54
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for i being Instruction-Location of S
for k being Element of NAT holds s . i = (Computation s,k) . i
proof end;

theorem :: AMI_1:55
for IL being non empty set
for N being with_non-empty_elements set
for k being Element of NAT
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,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 IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for k being Element of NAT st s . (IC (Computation s,k)) = halt S holds
Result s = Computation s,k
proof end;

theorem Th57: :: AMI_1:57
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S st ex k being Element of NAT st s . (IC (Computation s,k)) = halt S holds
for i being Element of NAT holds Result s = Result (Computation s,i)
proof end;

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty AMI-Struct of IL,N;
let o be Object of S;
cluster ObjectKind o -> non empty ;
coherence
not ObjectKind o is empty ;
end;

definition
let IL, N be set ;
let S be AMI-Struct of IL,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
{ p where p is Element of sproduct the Object-Kind of S : p is finite } is Subset of (sproduct the Object-Kind of S)
proof end;
end;

:: deftheorem defines FinPartSt AMI_1:def 23 :
for IL, N being set
for S being AMI-Struct of IL,N holds FinPartSt S = { p where p is Element of sproduct the Object-Kind of S : p is finite } ;

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster finite Element of sproduct the Object-Kind of S;
existence
ex b1 being Element of sproduct the Object-Kind of S st b1 is finite
proof end;
end;

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

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
mode FinPartState of S is finite PartState of S;
end;

definition
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
func Data-Locations S -> set equals :: AMI_1:def 24
the carrier of S \ ({(IC S)} \/ IL);
coherence
the carrier of S \ ({(IC S)} \/ IL) is set ;
end;

:: deftheorem defines Data-Locations AMI_1:def 24 :
for IL, N being set
for S being non empty AMI-Struct of IL,N holds Data-Locations S = the carrier of S \ ({(IC S)} \/ IL);

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 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 Element of NAT holds (Computation s1,i) | (dom IT) = (Computation s2,i) | (dom IT);
end;

:: deftheorem Def25 defines autonomic AMI_1:def 25 :
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 IT being FinPartState of S holds
( IT is autonomic iff for s1, s2 being State of S st IT c= s1 & IT c= s2 holds
for i being Element of NAT holds (Computation s1,i) | (dom IT) = (Computation s2,i) | (dom IT) );

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 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 :
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 FinPartState of S holds
( IT is halting iff for s being State of S st IT c= s holds
s is halting );

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let IT be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,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 :
for IL being non empty set
for N being with_non-empty_elements set
for IT being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N holds
( IT is programmable iff ex s being FinPartState of IT st
( not s is empty & s is autonomic ) );

theorem Th58: :: AMI_1:58
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,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 IL being non empty set
for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,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 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 la be Object of S;
let a be Element of ObjectKind la;
:: original: .-->
redefine func la .--> a -> FinPartState of S;
coherence
la .--> a is FinPartState of S by Th59;
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 definite AMI-Struct of IL,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
la,lb --> a,b is FinPartState of S by Th58;
end;

theorem Th60: :: AMI_1:60
for IL being non empty set
for E being set holds Trivial-AMI IL,E is realistic
proof end;

theorem Th61: :: AMI_1:61
for IL being non empty set
for N being with_non-empty_elements set holds Trivial-AMI IL,N is programmable
proof end;

registration
let IL be non empty set ;
let E be set ;
cluster Trivial-AMI IL,E -> strict realistic ;
coherence
Trivial-AMI IL,E is realistic by Th60;
end;

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

registration
let IL be non empty set ;
let E be set ;
cluster strict realistic AMI-Struct of IL,E;
existence
ex b1 being AMI-Struct of IL,E st
( b1 is realistic & 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 realistic AMI-Struct of IL,M;
existence
ex b1 being non empty stored-program AMI-Struct of IL,M st
( b1 is realistic & b1 is strict & b1 is IC-Ins-separated & b1 is definite )
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 realistic programmable AMI-Struct of IL,N;
existence
ex b1 being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N st
( b1 is halting & b1 is steady-programmed & b1 is realistic & b1 is programmable & b1 is strict )
proof end;
end;

theorem Th62: :: AMI_1:62
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for s being State of S
for p being FinPartState of S holds s | (dom p) is FinPartState of S
proof end;

registration
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 programmable AMI-Struct of IL,N;
cluster non empty autonomic Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st
( not b1 is empty & b1 is autonomic ) by Def27;
end;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
let f, g be PartState of S;
:: original: +*
redefine func f +* g -> PartState of S;
coherence
f +* g is PartState of S by CARD_3:86;
end;

theorem :: AMI_1:63
canceled;

theorem Th64: :: AMI_1:64
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 realistic AMI-Struct of IL,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
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 realistic AMI-Struct of IL,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
(IC S),loc --> l,h is halting
proof end;

theorem Th66: :: AMI_1:66
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 realistic AMI-Struct of IL,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
for i being Element of NAT holds Computation s,i = s
proof end;

theorem Th67: :: AMI_1:67
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 realistic AMI-Struct of IL,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
(IC S),loc --> l,h is autonomic
proof end;

registration
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 realistic AMI-Struct of IL,N;
cluster autonomic halting Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st
( b1 is autonomic & b1 is halting )
proof end;
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 realistic AMI-Struct of IL,N;
mode pre-program of S is autonomic halting FinPartState of S;
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 realistic AMI-Struct of IL,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
ex b1 being FinPartState of S st
for s' being State of S st s c= s' holds
b1 = (Result s') | (dom s)
proof end;
correctness
uniqueness
for b1, b2 being FinPartState of S st ( for s' being State of S st s c= s' holds
b1 = (Result s') | (dom s) ) & ( for s' being State of S st s c= s' holds
b2 = (Result s') | (dom s) ) holds
b1 = b2;
proof end;
end;

:: deftheorem defines Result AMI_1:def 28 :
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 realistic AMI-Struct of IL,N
for s being FinPartState of S st s is pre-program of S holds
for b5 being FinPartState of S holds
( b5 = Result s iff for s' being State of S st s c= s' holds
b5 = (Result s') | (dom s) );

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 realistic AMI-Struct of IL,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 :
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 realistic AMI-Struct of IL,N
for p being FinPartState of S
for F being Function holds
( p computes F iff 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) ) );

notation
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 realistic AMI-Struct of IL,N;
let p be FinPartState of S;
let F be Function;
antonym p does_not_compute F for p computes F;
end;

theorem Th68: :: AMI_1:68
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 realistic AMI-Struct of IL,N
for p being FinPartState of S holds p computes {}
proof end;

theorem Th69: :: AMI_1:69
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 realistic AMI-Struct of IL,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
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 realistic AMI-Struct of IL,N
for p being FinPartState of S holds
( p is pre-program of S iff p computes {} .--> {} )
proof 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 realistic AMI-Struct of IL,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 :
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 realistic AMI-Struct of IL,N
for IT being PartFunc of FinPartSt S, FinPartSt S holds
( IT is computable iff ex p being FinPartState of S st p computes IT );

theorem Th71: :: AMI_1:71
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 realistic AMI-Struct of IL,N
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} holds
F is computable
proof end;

theorem Th72: :: AMI_1:72
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 realistic AMI-Struct of IL,N
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {} holds
F is computable
proof end;

theorem Th73: :: AMI_1:73
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 realistic AMI-Struct of IL,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 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 realistic AMI-Struct of IL,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
ex b1 being FinPartState of S st b1 computes F by A1, Def30;
end;

:: deftheorem defines Program AMI_1:def 31 :
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 realistic AMI-Struct of IL,N
for F being PartFunc of FinPartSt S, FinPartSt S st F is computable holds
for b5 being FinPartState of S holds
( b5 is Program of F iff b5 computes F );

theorem :: AMI_1:74
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 realistic AMI-Struct of IL,N
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} holds
for p being FinPartState of S holds p is Program of F
proof end;

theorem :: AMI_1:75
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 realistic AMI-Struct of IL,N
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> {} holds
for p being pre-program of S holds p is Program of F
proof end;

theorem :: AMI_1:76
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 realistic AMI-Struct of IL,N
for p being pre-program of S
for F being PartFunc of FinPartSt S, FinPartSt S st F = {} .--> (Result p) holds
p is Program of F
proof end;

notation
let x be set ;
synonym InsCode x for x `1 ;
synonym AddressPart x for x `2 ;
end;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
attr S is standard-ins means :Def32: :: AMI_1:def 32
the Instructions of S c= [:NAT ,(((union N) \/ the carrier of S) * ):];
end;

:: deftheorem Def32 defines standard-ins AMI_1:def 32 :
for IL, N being set
for S being AMI-Struct of IL,N holds
( S is standard-ins iff the Instructions of S c= [:NAT ,(((union N) \/ the carrier of S) * ):] );

registration
let IL, N be set ;
cluster Trivial-AMI IL,N -> strict standard-ins ;
coherence
Trivial-AMI IL,N is standard-ins
proof end;
end;

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

registration
let IL be non empty set ;
let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard-ins 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 definite & b1 is standard-ins )
proof end;
end;

registration
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
cluster the Instructions of S -> non empty Relation-like ;
coherence
the Instructions of S is Relation-like
proof end;
end;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
func InsCodes S -> set equals :: AMI_1:def 33
 dom the Instructions of S;
correctness
coherence
dom the Instructions of S is set ;
;
end;

:: deftheorem defines InsCodes AMI_1:def 33 :
for IL, N being set
for S being standard-ins AMI-Struct of IL,N holds InsCodes S = dom the Instructions of S;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
mode InsType of S is Element of InsCodes S;
end;

definition
let IL, N be set ;
let S be standard-ins AMI-Struct of IL,N;
let I be Element of the Instructions of S;
:: original: InsCode
redefine func InsCode I -> InsType of S;
coherence
InsCode I is InsType of S by MCART_1:91;
end;

theorem :: AMI_1:77
for IL, N being set
for S being AMI-Struct of IL,N
for x being finite Element of sproduct the Object-Kind of S holds x in FinPartSt S ;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
mode IL-FinSequence of S -> FinSequence of IL means :Def34: :: AMI_1:def 34
verum;
existence
ex b1 being FinSequence of IL st verum ;
end;

:: deftheorem Def34 defines IL-FinSequence AMI_1:def 34 :
for IL, N being set
for S being AMI-Struct of IL,N
for b4 being FinSequence of IL holds
( b4 is IL-FinSequence of S iff verum );

definition
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
let f be IL-FinSequence of S;
let x be set ;
func f /. x -> Instruction-Location of S equals :: AMI_1:def 35
f /. x;
coherence
f /. x is Instruction-Location of S by Def4;
end;

:: deftheorem defines /. AMI_1:def 35 :
for IL being non empty set
for N being set
for S being non empty AMI-Struct of IL,N
for f being IL-FinSequence of S
for x being set holds f /. x = f /. x;

definition
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
let l1 be Instruction-Location of S;
:: original: <*
redefine func <*l1*> -> IL-FinSequence of S;
coherence
<*l1*> is IL-FinSequence of S
proof end;
let l2 be Instruction-Location of S;
:: original: <*
redefine func <*l1,l2*> -> IL-FinSequence of S;
coherence
<*l1,l2*> is IL-FinSequence of S
proof end;
end;

registration
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
cluster non empty IL-FinSequence of S;
existence
not for b1 being IL-FinSequence of S holds b1 is empty
proof end;
end;

definition
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
let f1, f2 be IL-FinSequence of S;
:: original: ^'
redefine func f1 ^' f2 -> IL-FinSequence of S;
coherence
f1 ^' f2 is IL-FinSequence of S
proof end;
end;

definition
let D be set ;
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
mode IL-Function of D,S -> Function of D,IL means :: AMI_1:def 36
verum;
existence
ex b1 being Function of D,IL st verum ;
end;

:: deftheorem defines IL-Function AMI_1:def 36 :
for D being set
for IL being non empty set
for N being set
for S being non empty AMI-Struct of IL,N
for b5 being Function of D,IL holds
( b5 is IL-Function of D,S iff verum );

definition
let D, IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
let f be IL-Function of D,S;
let d be Element of D;
:: original: .
redefine func f . d -> Instruction-Location of S;
correctness
coherence
f . d is Instruction-Location of S;
proof end;
end;

definition
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
mode IL-DecoratedTree of S -> DecoratedTree of IL means :: AMI_1:def 37
verum;
existence
ex b1 being DecoratedTree of IL st verum ;
end;

:: deftheorem defines IL-DecoratedTree AMI_1:def 37 :
for IL being non empty set
for N being set
for S being non empty AMI-Struct of IL,N
for b4 being DecoratedTree of IL holds
( b4 is IL-DecoratedTree of S iff verum );

definition
let IL be non empty set ;
let N be set ;
let S be non empty AMI-Struct of IL,N;
let T be IL-DecoratedTree of S;
let x be set ;
assume A1: x in dom T ;
func T . x -> Instruction-Location of S equals :: AMI_1:def 38
T . x;
coherence
T . x is Instruction-Location of S
proof end;
end;

:: deftheorem defines . AMI_1:def 38 :
for IL being non empty set
for N being set
for S being non empty AMI-Struct of IL,N
for T being IL-DecoratedTree of S
for x being set st x in dom T holds
T . x = T . x;

scheme :: AMI_1:sch 1
ILFraenkelFin{ F1() -> non empty set , F2() -> set , F3() -> non empty stored-program AMI-Struct of F1(),F2(), F4() -> set , F5( set ) -> set } :
{ F5(w) where w is Instruction-Location of F3() : w in F4() } is finite
provided
A1: F4() is finite
proof end;

scheme :: AMI_1:sch 2
Sch2{ F1() -> non empty set , F2() -> set , F3() -> set , F4() -> non empty stored-program AMI-Struct of F1(),F2(), F5( set ) -> set , F6() -> Instruction-Location of F4(), P1[ set , set ] } :
{ F5(i) where i is Element of F3() : ex l being Instruction-Location of F4() st
( l = F6() & P1[i,l] ) } = { F5(j) where j is Element of F3() : P1[j,F6()] }
proof end;

registration
let IL be non empty set ;
let N be set ;
let S be AMI-Struct of IL,N;
cluster FinPartSt S -> non empty ;
coherence
not FinPartSt S is empty
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 l be Instruction-Location of S;
func Start-At l -> FinPartState of S equals :: AMI_1:def 39
(IC S) .--> l;
correctness
coherence
(IC S) .--> l is FinPartState of S;
proof end;
end;

:: deftheorem defines Start-At AMI_1:def 39 :
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 l being Instruction-Location of S holds Start-At l = (IC S) .--> l;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
let IT be PartState of S;
attr IT is programmed means :Def40: :: AMI_1:def 40
 dom IT c= IL;
end;

:: deftheorem Def40 defines programmed AMI_1:def 40 :
for IL, N being set
for S being AMI-Struct of IL,N
for IT being PartState of S holds
( IT is programmed iff dom IT c= IL );

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
cluster programmed Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st b1 is programmed
proof end;
end;

theorem Th78: :: AMI_1:78
for IL being non empty set
for N being set
for S being AMI-Struct of IL,N
for p1, p2 being programmed PartState of S holds p1 +* p2 is programmed
proof end;

theorem Th79: :: AMI_1:79
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for s being State of S holds dom s = the carrier of S
proof end;

theorem Th80: :: AMI_1:80
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for p being PartState of S holds dom p c= the carrier of S
proof end;

theorem Th81: :: AMI_1:81
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for p being programmed FinPartState of S
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Computation s,k
proof 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;
let l be Element of IL;
pred s starts_at l means :: AMI_1:def 41
 IC s = l;
end;

:: deftheorem defines starts_at AMI_1:def 41 :
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
for l being Element of IL holds
( s starts_at l iff IC s = l );

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be non empty halting IC-Ins-separated AMI-Struct of IL,N;
let s be State of S;
let l be set ;
pred s halts_at l means :Def42: :: AMI_1:def 42
s . l = halt S;
end;

:: deftheorem Def42 defines halts_at AMI_1:def 42 :
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of IL,N
for s being State of S
for l being set holds
( s halts_at l iff s . l = halt S );

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 p be FinPartState of S;
assume A1: IC S in dom p ;
func IC p -> Instruction-Location of S equals :Def43: :: AMI_1:def 43
p . (IC S);
coherence
p . (IC S) is Instruction-Location of S
proof end;
end;

:: deftheorem Def43 defines IC AMI_1:def 43 :
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 p being FinPartState of S st IC S in dom p holds
IC p = p . (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 p be FinPartState of S;
let l be Element of IL;
pred p starts_at l means :: AMI_1:def 44
( IC S in dom p & IC p = l );
end;

:: deftheorem defines starts_at AMI_1:def 44 :
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 p being FinPartState of S
for l being Element of IL holds
( p starts_at l iff ( IC S in dom p & IC p = l ) );

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 p be FinPartState of S;
let l be set ;
pred p halts_at l means :: AMI_1:def 45
( l in dom p & p . l = halt S );
end;

:: deftheorem defines halts_at AMI_1:def 45 :
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 p being FinPartState of S
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );

theorem :: AMI_1:82
canceled;

theorem Th83: :: AMI_1:83
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S holds
( s is halting iff ex k being Element of NAT st s halts_at IC (Computation s,k) )
proof end;

theorem :: AMI_1:84
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S
for p being FinPartState of S
for l being Instruction-Location of S st p c= s & p halts_at l holds
s halts_at l
proof end;

theorem Th85: :: AMI_1:85
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S
for k being Element of NAT st s is halting holds
( Result s = Computation s,k iff s halts_at IC (Computation s,k) )
proof end;

theorem :: AMI_1:86
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for p being programmed FinPartState of S
for k being Element of NAT holds
( p c= s iff p c= Computation s,k )
proof end;

theorem Th87: :: AMI_1:87
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S
for k being Element of NAT st s halts_at IC (Computation s,k) holds
Result s = Computation s,k
proof end;

theorem Th88: :: AMI_1:88
for i, j being Element of NAT
for IL being non empty set
for N being with_non-empty_elements set st i <= j holds
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S st s halts_at IC (Computation s,i) holds
s halts_at IC (Computation s,j)
proof end;

theorem :: AMI_1:89
for i, j being Element of NAT
for IL being non empty set
for N being with_non-empty_elements set st i <= j holds
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S st s halts_at IC (Computation s,i) holds
Computation s,j = Computation s,i
proof end;

theorem :: AMI_1:90
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S st ex k being Element of NAT st s halts_at IC (Computation s,k) holds
for i being Element of NAT holds Result s = Result (Computation s,i)
proof end;

theorem :: AMI_1:91
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 steady-programmed definite AMI-Struct of IL,N
for s being State of S
for l being Instruction-Location of S
for k being Element of NAT holds
( s halts_at l iff Computation s,k halts_at l )
proof end;

theorem :: AMI_1:92
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 p being FinPartState of S
for l being Element of IL st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
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 definite AMI-Struct of IL,N;
let l be Instruction-Location of S;
let I be Element of the Instructions of S;
:: original: .-->
redefine func l .--> I -> programmed FinPartState of S;
coherence
l .--> I is programmed FinPartState of S
proof end;
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 s be State of S;
assume A1: s is halting ;
func LifeSpan s -> Element of NAT means :Def46: :: AMI_1:def 46
( CurInstr (Computation s,it) = halt S & ( for k being Element of NAT st CurInstr (Computation s,k) = halt S holds
it <= k ) );
existence
ex b1 being Element of NAT st
( CurInstr (Computation s,b1) = halt S & ( for k being Element of NAT st CurInstr (Computation s,k) = halt S holds
b1 <= k ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st CurInstr (Computation s,b1) = halt S & ( for k being Element of NAT st CurInstr (Computation s,k) = halt S holds
b1 <= k ) & CurInstr (Computation s,b2) = halt S & ( for k being Element of NAT st CurInstr (Computation s,k) = halt S holds
b2 <= k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def46 defines LifeSpan AMI_1:def 46 :
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 s is halting holds
for b5 being Element of NAT holds
( b5 = LifeSpan s iff ( CurInstr (Computation s,b5) = halt S & ( for k being Element of NAT st CurInstr (Computation s,k) = halt S holds
b5 <= k ) ) );

theorem :: AMI_1:93
for IL being non empty set
for N being non empty 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
for m being Element of NAT holds
( s is halting iff Computation s,m is halting )
proof end;

theorem Th94: :: AMI_1:94
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 in dom s
proof end;

theorem :: AMI_1:95
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 Start-At (IC s) = s | {(IC S)}
proof end;

theorem :: AMI_1:96
canceled;

theorem :: AMI_1:97
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 p being FinPartState of S
for s being State of S st IC S in dom p & p c= s holds
IC p = IC s
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 definite AMI-Struct of IL,N;
let p be programmed FinPartState of S;
let loc be set ;
assume A1: loc in dom p ;
func pi p,loc -> Instruction of S equals :: AMI_1:def 47
p . loc;
coherence
p . loc is Instruction of S
proof end;
end;

:: deftheorem defines pi AMI_1:def 47 :
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 p being programmed FinPartState of S
for loc being set st loc in dom p holds
pi p,loc = p . loc;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
let p be PartState of S;
func ProgramPart p -> set equals :: AMI_1:def 48
p | IL;
coherence
p | IL is set ;
end;

:: deftheorem defines ProgramPart AMI_1:def 48 :
for IL, N being set
for S being AMI-Struct of IL,N
for p being PartState of S holds ProgramPart p = p | IL;

definition
let IL, N be set ;
let S be AMI-Struct of IL,N;
let p be PartState of S;
:: original: ProgramPart
redefine func ProgramPart p -> PartState of S;
coherence
ProgramPart p is PartState of S by CARD_3:80, RELAT_1:88;
end;

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
let p be FinPartState of S;
cluster ProgramPart p -> finite ;
coherence
ProgramPart p is finite by FINSET_1:13, RELAT_1:88;
end;

registration
let IL, N be set ;
let S be AMI-Struct of IL,N;
let p be PartState of S;
cluster ProgramPart p -> programmed PartState of S;
coherence
ProgramPart p is programmed PartState of S
proof end;
end;

definition
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
let p be PartState of S;
func DataPart p -> PartState of S equals :: AMI_1:def 49
p | (Data-Locations S);
coherence
p | (Data-Locations S) is PartState of S by CARD_3:80, RELAT_1:88;
projectivity
for b1, b2 being PartState of S st b1 = b2 | (Data-Locations S) holds
b1 = b1 | (Data-Locations S) by RELAT_1:101;
end;

:: deftheorem defines DataPart AMI_1:def 49 :
for IL, N being set
for S being non empty AMI-Struct of IL,N
for p being PartState of S holds DataPart p = p | (Data-Locations S);

registration
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
let p be FinPartState of S;
cluster DataPart p -> finite ;
coherence
DataPart p is finite by FINSET_1:13, RELAT_1:88;
end;

definition
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
let IT be PartState of S;
attr IT is data-only means :Def50: :: AMI_1:def 50
 dom IT misses {(IC S)} \/ IL;
end;

:: deftheorem Def50 defines data-only AMI_1:def 50 :
for IL, N being set
for S being non empty AMI-Struct of IL,N
for IT being PartState of S holds
( IT is data-only iff dom IT misses {(IC S)} \/ IL );

registration
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
cluster data-only Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st b1 is data-only
proof end;
end;

theorem :: AMI_1:98
canceled;

theorem :: AMI_1:99
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for p being FinPartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Computation s,i
proof end;

theorem Th100: :: AMI_1:100
for IL, N being set
for S being non empty AMI-Struct of IL,N
for p being FinPartState of S holds not IC S in dom (DataPart p)
proof end;

theorem Th101: :: AMI_1:101
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 realistic AMI-Struct of IL,N
for p being FinPartState of S holds not IC S in dom (ProgramPart p)
proof end;

theorem :: AMI_1:102
for IL, N being set
for S being non empty AMI-Struct of IL,N
for p being FinPartState of S holds {(IC S)} misses dom (DataPart p) by Th100, ZFMISC_1:56;

theorem :: AMI_1:103
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 realistic AMI-Struct of IL,N
for p being FinPartState of S holds {(IC S)} misses dom (ProgramPart p) by Th101, ZFMISC_1:56;

theorem Th104: :: AMI_1:104
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 p, q being FinPartState of S holds dom (DataPart p) misses dom (ProgramPart q)
proof end;

theorem Th105: :: AMI_1:105
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 p being programmed FinPartState of S holds ProgramPart p = p
proof end;

theorem :: AMI_1:106
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 p being FinPartState of S
for l being Instruction-Location of S st l in dom p holds
l in dom (ProgramPart p)
proof end;

theorem :: AMI_1:107
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 p being data-only FinPartState of S
for q being FinPartState of S holds
( p c= q iff p c= DataPart q )
proof end;

theorem :: AMI_1:108
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 realistic AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)
proof 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 IT be PartFunc of FinPartSt S, FinPartSt S;
attr IT is data-only means :: AMI_1:def 51
for p being FinPartState of S st p in dom IT holds
( p is data-only & ( for q being FinPartState of S st q = IT . p holds
q is data-only ) );
end;

:: deftheorem defines data-only AMI_1:def 51 :
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 IT being PartFunc of FinPartSt S, FinPartSt S holds
( IT is data-only iff for p being FinPartState of S st p in dom IT holds
( p is data-only & ( for q being FinPartState of S st q = IT . p holds
q is data-only ) ) );

theorem :: AMI_1:109
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 realistic AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
not p is programmed
proof 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 s be State of S;
let p be PartState of S;
:: original: +*
redefine func s +* p -> State of S;
coherence
s +* p is State of S by CARD_3:69;
end;

theorem :: AMI_1:110
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 p being FinPartState of S st IC S in dom p holds
Start-At (IC p) c= p
proof end;

theorem :: AMI_1:111
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
for iloc being Instruction-Location of S holds IC (s +* (Start-At iloc)) = iloc
proof end;

theorem :: AMI_1:112
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 realistic AMI-Struct of IL,N
for s being State of S
for iloc, a being Instruction-Location of S holds s . a = (s +* (Start-At iloc)) . a
proof end;

theorem :: AMI_1:113
canceled;

theorem :: AMI_1:114
for IL being non empty set
for N being with_non-empty_elements set
for S being stored-program AMI-Struct of IL,N
for s being State of S holds IL c= dom s
proof end;

theorem :: AMI_1:115
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated AMI-Struct of IL,N
for s being State of S holds IC s in dom s
proof end;

theorem :: AMI_1:116
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program AMI-Struct of IL,N
for s being State of S
for l being Instruction-Location of S holds l in dom s
proof end;

theorem Th117: :: AMI_1:117
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of IL,N
for i being Instruction of S
for s being State of S holds (Exec i,s) | IL = s | IL
proof end;

registration
let IL be non empty set ;
let N be set ;
let S be AMI-Struct of IL,N;
cluster programmed Element of sproduct the Object-Kind of S;
existence
ex b1 being FinPartState of S st b1 is programmed
proof end;
end;

theorem Th118: :: AMI_1:118
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of IL,N
for p being programmed FinPartState of S holds rng p c= the Instructions of S
proof end;

definition
let IL be non empty set ;
let N be set ;
let S be AMI-Struct of IL,N;
let I, J be programmed PartState of S;
:: original: +*
redefine func I +* J -> programmed PartState of S;
coherence
I +* J is programmed PartState of S by Th78;
end;

theorem :: AMI_1:119
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of IL,N
for f being Function of the Instructions of S,the Instructions of S
for s being programmed FinPartState of S holds dom (f * s) = dom s
proof end;

definition
let IL be non empty set ;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of IL,N;
let s be programmed PartState of S;
let f be Function of the Instructions of S,the Instructions of S;
:: original: *
redefine func f * s -> programmed PartState of S;
coherence
s * f is programmed PartState of S
proof end;
end;

theorem :: AMI_1:120
for IL, N being set
for A being AMI-Struct of IL,N
for s being State of A
for I being programmed FinPartState of A holds s,s +* I equal_outside IL
proof end;

theorem :: AMI_1:121
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for s1, s2 being State of S st s1,s2 equal_outside IL holds
IC s1 = IC s2
proof end;

theorem :: AMI_1:122
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 s is halting holds
Result s = Computation s,(LifeSpan s)
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 definite AMI-Struct of IL,N;
let s be State of S;
let l be Instruction-Location of S;
let i be Instruction of S;
:: original: +*
redefine func s +* l,i -> State of S;
coherence
s +* l,i is State of S
proof end;
end;

theorem :: AMI_1:123
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for s being State of S
for n being Element of NAT holds s | IL = (Computation s,n) | IL
proof end;

theorem :: AMI_1:124
for i being Element of NAT
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for p being programmed FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
proof end;

theorem :: AMI_1:125
for IL being non empty set
for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for p being Element of FinPartSt S holds p is FinPartState of S
proof end;

theorem :: AMI_1:126
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of IL,N
for I being programmed FinPartState of S
for x being set st x in dom I holds
I . x is Instruction of S
proof end;

theorem :: AMI_1:127
for IL being non empty set
for N being non empty 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
for k being Element of NAT st CurInstr (Computation s,k) = halt S holds
Computation s,(LifeSpan s) = Computation s,k
proof end;

theorem :: AMI_1:128
for j being Element of NAT
for IL being non empty set
for N being non empty 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 LifeSpan s <= j & s is halting holds
Computation s,j = Computation s,(LifeSpan s)
proof end;

theorem :: AMI_1:129
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 realistic AMI-Struct of IL,N
for t, u being State of S
for il being Instruction-Location of S
for e being Element of ObjectKind (IC S)
for I being Element of ObjectKind il st e = il & u = t +* ((IC S),il --> e,I) holds
( u . il = I & IC u = il & IC (Following u) = (Exec (u . (IC u)),u) . (IC S) )
proof end;

theorem :: AMI_1:130
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 s = Following s holds
for n being Element of NAT holds Computation s,n = s
proof end;

theorem :: AMI_1:131
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 i being Instruction of S holds (Exec (s . (IC s)),s) . (IC S) = IC (Following s) ;

definition
let IL be non empty set ;
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of IL,N;
let I be FinPartState of S;
attr I is halt-free means :: AMI_1:def 52
not halt S in rng I;
end;

:: deftheorem defines halt-free AMI_1:def 52 :
for IL being non empty set
for N being with_non-empty_elements set
for S being halting AMI-Struct of IL,N
for I being FinPartState of S holds
( I is halt-free iff not halt S in rng I );

theorem :: AMI_1:132
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 st s = Following s holds
for n being Element of NAT holds Computation s,n = s
proof end;

theorem :: AMI_1:133
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 realistic AMI-Struct of IL,N
for t, u being State of S
for il being Instruction-Location of S
for e being Element of ObjectKind (IC S)
for I being Element of ObjectKind il st e = il & u = t +* ((IC S),il --> e,I) holds
( u . il = I & IC u = il & IC (Following u) = (Exec (u . (IC u)),u) . (IC S) )
proof end;

theorem TW1: :: AMI_1:134
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for l being Instruction-Location of S holds dom (Start-At l) misses IL
proof end;

theorem :: AMI_1:135
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for l being Instruction-Location of S holds ProgramPart (Start-At l) = {}
proof end;

registration
let IL, N be set ;
let S be non empty AMI-Struct of IL,N;
let p be FinPartState of S;
cluster DataPart p -> data-only ;
coherence
DataPart p is data-only
proof end;
end;

theorem :: AMI_1:136
for IL, N being set
for S being non empty AMI-Struct of IL,N
for p being data-only FinPartState of S holds ProgramPart p = {}
proof end;

theorem :: AMI_1:137
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of IL,N
for l, l1 being Instruction-Location of S holds not l in dom (Start-At l1)
proof end;

theorem :: AMI_1:138
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 l being Instruction-Location of S holds DataPart (Start-At l) = {}
proof end;

theorem Th139: :: AMI_1:139
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,N
for p being PartState of S holds
( p is data-only iff dom p c= Data-Locations S )
proof end;

theorem :: AMI_1:140
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 realistic AMI-Struct of IL,N
for s being State of S
for X being set st X c= IL holds
rng (s | X) c= the Instructions of S
proof end;

theorem :: AMI_1:141
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
for l1, l2 being Instruction-Location of S holds (s +* (Start-At l1)) +* (Start-At l2) = s +* (Start-At l2)
proof end;

theorem :: AMI_1:142
for IL being non empty set
for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,N
for p being PartState of S holds
( p is data-only iff DataPart p = p )
proof end;