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


begin

definition
let N be set ;
attr c2 is strict ;
struct AMI-Struct of N -> COM-Struct of N;
aggr AMI-Struct(# carrier, Instruction-Counter, Instructions, haltF, Object-Kind, Execution #) -> AMI-Struct of N;
sel Execution c2 -> Action of the Instructions of c2,(product the Object-Kind of c2);
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 = succ NAT & the Instruction-Counter of it = NAT & the Instructions of it = {[0 ,{} ,{} ]} & the haltF of it = [0 ,{} ,{} ] & the Object-Kind of it = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) & the Execution of it = [0 ,{} ,{} ] .--> (id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )))) );
existence
ex b1 being strict AMI-Struct of N st
( the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,{} ,{} ]} & the haltF of b1 = [0 ,{} ,{} ] & the Object-Kind of b1 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) & the Execution of b1 = [0 ,{} ,{} ] .--> (id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )))) )
proof end;
uniqueness
for b1, b2 being strict AMI-Struct of N st the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,{} ,{} ]} & the haltF of b1 = [0 ,{} ,{} ] & the Object-Kind of b1 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) & the Execution of b1 = [0 ,{} ,{} ] .--> (id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )))) & the carrier of b2 = succ NAT & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,{} ,{} ]} & the haltF of b2 = [0 ,{} ,{} ] & the Object-Kind of b2 = (NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT ) & the Execution of b2 = [0 ,{} ,{} ] .--> (id (product ((NAT --> {[0 ,{} ,{} ]}) +* (NAT .--> NAT )))) holds
b1 = b2 ;
end;

:: deftheorem AMI_1:def 1 :
canceled;

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

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

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

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

:: deftheorem AMI_1:def 3 :
canceled;

:: deftheorem AMI_1:def 4 :
canceled;

:: deftheorem AMI_1:def 5 :
canceled;

:: deftheorem AMI_1:def 6 :
canceled;

:: deftheorem defines Exec AMI_1:def 7 :
for N being with_non-empty_elements set
for S being AMI-Struct of 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 N be with_non-empty_elements set ;
let S be 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 :
for N being with_non-empty_elements set
for S being AMI-Struct of 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 N be with_non-empty_elements set ;
let S be AMI-Struct of N;
attr S is halting means :Def9: :: AMI_1:def 9
the haltF of S is halting ;
end;

:: deftheorem Def9 defines halting AMI_1:def 9 :
for N being with_non-empty_elements set
for S being AMI-Struct of N holds
( S is halting iff the haltF of S is halting );

definition
canceled;
end;

:: deftheorem AMI_1:def 10 :
canceled;

registration
let N be with_non-empty_elements set ;
cluster Trivial-AMI N -> strict halting ;
coherence
Trivial-AMI N is halting
proof end;
end;

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

registration
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
cluster halt S -> halting ;
coherence
halt S is halting by Def9;
end;

registration
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
cluster halting Element of the Instructions of S;
existence
ex b1 being Instruction of S st b1 is halting
proof end;
end;

definition
canceled;
canceled;
let N be with_non-empty_elements set ;
let IT be non empty 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 Element of NAT holds (Exec i,s) . l = s . l;
end;

:: deftheorem AMI_1:def 11 :
canceled;

:: deftheorem AMI_1:def 12 :
canceled;

:: deftheorem Def13 defines steady-programmed AMI_1:def 13 :
for N being with_non-empty_elements set
for IT being non empty AMI-Struct of N holds
( IT is steady-programmed iff for s being State of IT
for i being Instruction of IT
for l being Element of NAT holds (Exec i,s) . l = s . l );

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

theorem :: AMI_1:7
canceled;

theorem :: AMI_1:8
canceled;

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

registration
let E be set ;
cluster Trivial-AMI E -> IC-Ins-separated definite strict ;
coherence
( Trivial-AMI E is IC-Ins-separated & Trivial-AMI E is definite )
proof end;
end;

registration
let N be with_non-empty_elements set ;
cluster Trivial-AMI N -> strict steady-programmed ;
coherence
Trivial-AMI N is steady-programmed
proof end;
end;

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

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

theorem :: AMI_1:10
canceled;

theorem :: AMI_1:11
canceled;

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

begin

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

:: deftheorem AMI_1:def 14 :
canceled;

:: deftheorem AMI_1:def 15 :
canceled;

:: deftheorem AMI_1:def 16 :
canceled;

:: deftheorem AMI_1:def 17 :
canceled;

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

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
deffunc H1( set , State of S) -> Element of product the Object-Kind of S = down (Following p,$2);
let s be State of S;
let k be Nat;
func Comput p,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 p,(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 p,(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 p,(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 p,(f . i) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines Comput AMI_1:def 19 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S
for k being Nat
for b6 being State of S holds
( b6 = Comput p,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 p,(f . i) ) ) );

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let s be State of S;
pred p halts_on s means :Def20: :: AMI_1:def 20
 ex k being Nat st
( IC (Comput p,s,k) in dom p & CurInstr p,(Comput p,s,k) = halt S );
end;

:: deftheorem Def20 defines halts_on AMI_1:def 20 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S holds
( p halts_on s iff ex k being Nat st
( IC (Comput p,s,k) in dom p & CurInstr p,(Comput p,s,k) = halt S ) );

theorem Th13: :: AMI_1:13
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S holds Comput p,s,0 = s
proof end;

theorem Th14: :: AMI_1:14
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S
for k being Nat holds Comput p,s,(k + 1) = Following p,(Comput p,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 :: AMI_1:48
canceled;

theorem :: AMI_1:49
canceled;

theorem :: AMI_1:50
canceled;

theorem Th51: :: AMI_1:51
for i being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for s being State of S
for p being NAT -defined the Instructions of b3 -valued Function
for k being Element of NAT holds Comput p,s,(i + k) = Comput p,(Comput p,s,i),k
proof end;

theorem Th52: :: AMI_1:52
for i, j being Element of NAT st i <= j holds
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions of b4 -valued Function
for s being State of S st CurInstr p,(Comput p,s,i) = halt S holds
Comput p,s,j = Comput p,s,i
proof end;

definition
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let s be State of S;
assume A1: p halts_on s ;
func Result p,s -> State of S means :Def22: :: AMI_1:def 22
 ex k being Element of NAT st
( it = Comput p,s,k & CurInstr p,it = halt S );
uniqueness
for b1, b2 being State of S st ex k being Element of NAT st
( b1 = Comput p,s,k & CurInstr p,b1 = halt S ) & ex k being Element of NAT st
( b2 = Comput p,s,k & CurInstr p,b2 = halt S ) holds
b1 = b2
proof end;
correctness
existence
ex b1 being State of S ex k being Element of NAT st
( b1 = Comput p,s,k & CurInstr p,b1 = halt S );
proof end;
end;

:: deftheorem AMI_1:def 21 :
canceled;

:: deftheorem Def22 defines Result AMI_1:def 22 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S st p halts_on s holds
for b5 being State of S holds
( b5 = Result p,s iff ex k being Element of NAT st
( b5 = Comput p,s,k & CurInstr p,b5 = halt S ) );

L117: for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of N
for i being Instruction of S
for s being State of S holds ProgramPart (Exec i,s) = ProgramPart s
proof end;

LmA: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S
for n being Element of NAT holds ProgramPart s = ProgramPart (Comput P,s,n)
proof end;

theorem :: AMI_1:53
canceled;

theorem Th54: :: AMI_1:54
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S
for i, k being Element of NAT holds s . i = (Comput P,s,k) . i
proof end;

theorem :: AMI_1:55
for k being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b3 -valued ManySortedSet of NAT
for s being State of S holds Comput P,s,(k + 1) = Exec (P . (IC (Comput P,s,k))),(Comput P,s,k)
proof end;

theorem Th56: :: AMI_1:56
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S
for k being Element of NAT st P . (IC (Comput P,s,k)) = halt S holds
Result P,s = Comput P,s,k
proof end;

theorem Th57: :: AMI_1:57
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S st ex k being Element of NAT st P . (IC (Comput P,s,k)) = halt S holds
for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i)
proof end;

definition
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let IT be PartState 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 (Comput (ProgramPart s1),s1,i) | (dom IT) = (Comput (ProgramPart s2),s2,i) | (dom IT);
end;

:: deftheorem AMI_1:def 23 :
canceled;

:: deftheorem AMI_1:def 24 :
canceled;

:: deftheorem Def25 defines autonomic AMI_1:def 25 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for IT being PartState 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 (Comput (ProgramPart s1),s1,i) | (dom IT) = (Comput (ProgramPart s2),s2,i) | (dom IT) );

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

:: deftheorem Def26 defines halting AMI_1:def 26 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for IT being PartState of S holds
( IT is halting iff for s being State of S st IT c= s holds
ProgramPart s halts_on s );

registration
let E be set ;
cluster Trivial-AMI E -> realistic strict ;
coherence
Trivial-AMI E is realistic
proof end;
end;

registration
let E be set ;
cluster realistic strict AMI-Struct of E;
existence
ex b1 being AMI-Struct of E st
( b1 is realistic & b1 is strict )
proof end;
end;

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

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

begin

theorem :: AMI_1:58
canceled;

theorem :: AMI_1:59
canceled;

theorem :: AMI_1:60
canceled;

theorem :: AMI_1:61
canceled;

theorem :: AMI_1:62
canceled;

theorem :: AMI_1:63
canceled;

theorem :: AMI_1:64
canceled;

theorem Th65: :: AMI_1:65
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for l being Nat
for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is halting
proof end;

theorem Th66: :: AMI_1:66
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for l being Nat
for p being PartState of S
for s being State of S st p = (IC S),l --> l,(halt S) & p c= s holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = s
proof end;

theorem Th67: :: AMI_1:67
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for l being Nat
for p being PartState of S st p = (IC S),l --> l,(halt S) holds
p is autonomic
proof end;

registration
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N;
cluster Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V114() autonomic halting set ;
existence
ex b1 being FinPartState of S st
( b1 is autonomic & b1 is halting )
proof end;
end;

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

definition
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let d be FinPartState of S;
assume A1: ( d is pre-program of S & p = ProgramPart d ) ;
func Result p,d -> FinPartState of S means :: AMI_1:def 29
for s being State of S st d c= s holds
it = (Result (ProgramPart s),s) | (dom d);
existence
ex b1 being FinPartState of S st
for s being State of S st d c= s holds
b1 = (Result (ProgramPart s),s) | (dom d)
proof end;
correctness
uniqueness
for b1, b2 being FinPartState of S st ( for s being State of S st d c= s holds
b1 = (Result (ProgramPart s),s) | (dom d) ) & ( for s being State of S st d c= s holds
b2 = (Result (ProgramPart s),s) | (dom d) ) holds
b1 = b2;
proof end;
end;

:: deftheorem AMI_1:def 27 :
canceled;

:: deftheorem AMI_1:def 28 :
canceled;

:: deftheorem defines Result AMI_1:def 29 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for d being FinPartState of S st d is pre-program of S & p = ProgramPart d holds
for b5 being FinPartState of S holds
( b5 = Result p,d iff for s being State of S st d c= s holds
b5 = (Result (ProgramPart s),s) | (dom d) );

begin

definition
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let d be FinPartState of S;
let F be Function;
pred p,d computes F means :Def29: :: AMI_1:def 30
for x being set st x in dom F holds
ex s being FinPartState of S st
( x = s & (p +* d) +* s is pre-program of S & F . s c= Result p,(d +* s) );
end;

:: deftheorem Def29 defines computes AMI_1:def 30 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for d being FinPartState of S
for F being Function holds
( p,d computes F iff for x being set st x in dom F holds
ex s being FinPartState of S st
( x = s & (p +* d) +* s is pre-program of S & F . s c= Result p,(d +* s) ) );

theorem :: AMI_1:68
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for d being FinPartState of S holds p,d computes {}
proof end;

theorem :: AMI_1:69
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for d being FinPartState of S holds
( p +* d is pre-program of S iff p,d computes {} .--> (Result p,d) )
proof end;

theorem :: AMI_1:70
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for d being FinPartState of S holds
( p +* d is pre-program of S iff p,d computes {} .--> {} )
proof end;

begin

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

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

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

begin

theorem :: AMI_1:71
canceled;

theorem :: AMI_1:72
canceled;

theorem :: AMI_1:73
canceled;

theorem :: AMI_1:74
canceled;

theorem :: AMI_1:75
canceled;

theorem :: AMI_1:76
canceled;

theorem :: AMI_1:77
canceled;

theorem :: AMI_1:78
canceled;

theorem :: AMI_1:79
canceled;

theorem :: AMI_1:80
canceled;

theorem Th81: :: AMI_1:81
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being NAT -defined PartState of
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput P,s,k
proof end;

theorem :: AMI_1:82
canceled;

theorem Th83: :: AMI_1:83
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S holds
( p halts_on s iff ex i being Element of NAT st p halts_at IC (Comput p,s,i) )
proof end;

theorem :: AMI_1:84
canceled;

theorem Th85: :: AMI_1:85
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S
for k being Nat st p halts_on s holds
( Result p,s = Comput p,s,k iff p halts_at IC (Comput p,s,k) )
proof end;

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

theorem Th87: :: AMI_1:87
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being NAT -defined the Instructions of b2 -valued Function
for s being State of S
for k being Element of NAT st P halts_at IC (Comput P,s,k) holds
Result P,s = Comput P,s,k
proof end;

theorem Th88: :: AMI_1:88
for i, j being Element of NAT
for N being non empty with_non-empty_elements set st i <= j holds
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being NAT -defined the Instructions of b4 -valued Function
for s being State of S st P halts_at IC (Comput P,s,i) holds
P halts_at IC (Comput P,s,j)
proof end;

theorem :: AMI_1:89
for i, j being Element of NAT
for N being non empty with_non-empty_elements set st i <= j holds
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being NAT -defined the Instructions of b4 -valued Function
for s being State of S st P halts_at IC (Comput P,s,i) holds
Comput P,s,j = Comput P,s,i
proof end;

theorem :: AMI_1:90
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S st ex k being Element of NAT st P halts_at IC (Comput P,s,k) holds
for i being Element of NAT holds Result P,s = Result P,(Comput P,s,i)
proof end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let s be State of S;
assume A1: p halts_on s ;
func LifeSpan p,s -> Element of NAT means :Def46: :: AMI_1:def 46
( CurInstr p,(Comput p,s,it) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
it <= k ) );
existence
ex b1 being Element of NAT st
( CurInstr p,(Comput p,s,b1) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b1 <= k ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st CurInstr p,(Comput p,s,b1) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b1 <= k ) & CurInstr p,(Comput p,s,b2) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b2 <= k ) holds
b1 = b2
proof end;
end;

:: deftheorem AMI_1:def 31 :
canceled;

:: deftheorem AMI_1:def 32 :
canceled;

:: deftheorem AMI_1:def 33 :
canceled;

:: deftheorem AMI_1:def 34 :
canceled;

:: deftheorem AMI_1:def 35 :
canceled;

:: deftheorem AMI_1:def 36 :
canceled;

:: deftheorem AMI_1:def 37 :
canceled;

:: deftheorem AMI_1:def 38 :
canceled;

:: deftheorem AMI_1:def 39 :
canceled;

:: deftheorem AMI_1:def 40 :
canceled;

:: deftheorem AMI_1:def 41 :
canceled;

:: deftheorem AMI_1:def 42 :
canceled;

:: deftheorem AMI_1:def 43 :
canceled;

:: deftheorem AMI_1:def 44 :
canceled;

:: deftheorem AMI_1:def 45 :
canceled;

:: deftheorem Def46 defines LifeSpan AMI_1:def 46 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S st p halts_on s holds
for b5 being Element of NAT holds
( b5 = LifeSpan p,s iff ( CurInstr p,(Comput p,s,b5) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b5 <= k ) ) );

theorem :: AMI_1:91
canceled;

theorem :: AMI_1:92
canceled;

theorem :: AMI_1:93
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S
for m being Element of NAT holds
( p halts_on s iff p halts_on Comput p,s,m )
proof end;

theorem :: AMI_1:94
canceled;

theorem :: AMI_1:95
canceled;

theorem :: AMI_1:96
canceled;

theorem :: AMI_1:97
canceled;

theorem :: AMI_1:98
canceled;

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

theorem :: AMI_1:100
canceled;

theorem :: AMI_1:101
canceled;

theorem :: AMI_1:102
canceled;

theorem :: AMI_1:103
canceled;

theorem :: AMI_1:104
canceled;

theorem :: AMI_1:105
canceled;

theorem :: AMI_1:106
canceled;

theorem :: AMI_1:107
canceled;

theorem :: AMI_1:108
canceled;

theorem :: AMI_1:109
canceled;

theorem :: AMI_1:110
canceled;

theorem :: AMI_1:111
canceled;

theorem :: AMI_1:112
canceled;

theorem :: AMI_1:113
canceled;

theorem :: AMI_1:114
canceled;

theorem :: AMI_1:115
canceled;

theorem :: AMI_1:116
canceled;

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

theorem :: AMI_1:118
canceled;

theorem :: AMI_1:119
canceled;

theorem :: AMI_1:120
canceled;

theorem :: AMI_1:121
canceled;

theorem :: AMI_1:122
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b2 -valued Function
for s being State of S st p halts_on s holds
Result p,s = Comput p,s,(LifeSpan p,s)
proof end;

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

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

theorem :: AMI_1:125
canceled;

theorem :: AMI_1:126
canceled;

theorem :: AMI_1:127
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S
for k being Element of NAT st CurInstr P,(Comput P,s,k) = halt S holds
Comput P,s,(LifeSpan P,s) = Comput P,s,k
proof end;

theorem :: AMI_1:128
for j being Element of NAT
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b3 -valued Function
for s being State of S st LifeSpan p,s <= j & p halts_on s holds
Comput p,s,j = Comput p,s,(LifeSpan p,s)
proof end;

theorem :: AMI_1:129
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed AMI-Struct of N
for t, u being State of S
for e being Element of NAT
for I being Instruction of S st u = t +* ((IC S),e --> e,I) holds
( u . e = I & IC u = e & IC (Following (ProgramPart u),u) = (Exec (u . (IC u)),u) . (IC S) )
proof end;

theorem :: AMI_1:130
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S st s = Following P,s holds
for n being Element of NAT holds Comput P,s,n = s
proof end;

theorem :: AMI_1:131
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S
for i being Instruction of S holds (Exec (P . (IC s)),s) . (IC S) = IC (Following P,s)
proof end;

theorem :: AMI_1:132
canceled;

theorem :: AMI_1:133
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic steady-programmed AMI-Struct of N
for t, u being State of S
for il being Element of NAT
for e being Element of ObjectKind (IC S)
for I being Element of the Object-Kind of S . il st e = il & u = t +* ((IC S),il --> e,I) holds
( u . il = I & IC u = il & IC (Following (ProgramPart u),u) = (Exec (u . (IC u)),u) . (IC S) )
proof end;

theorem :: AMI_1:134
canceled;

theorem :: AMI_1:135
canceled;

theorem :: AMI_1:136
canceled;

theorem :: AMI_1:137
canceled;

theorem :: AMI_1:138
canceled;

theorem :: AMI_1:139
canceled;

theorem :: AMI_1:140
canceled;

theorem :: AMI_1:141
canceled;

theorem :: AMI_1:142
canceled;

theorem :: AMI_1:143
canceled;

theorem :: AMI_1:144
canceled;

theorem :: AMI_1:145
canceled;

theorem :: AMI_1:146
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite halting steady-programmed AMI-Struct of N
for P being the Instructions of b2 -valued ManySortedSet of NAT
for s being State of S holds
( P halts_on s iff ex k being Element of NAT st CurInstr P,(Comput P,s,k) = halt S )
proof end;