:: 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 c₂ is strict ;
struct AMI-Struct of N -> 1-sorted ;
aggr AMI-Struct(# carrier, Instruction-Counter, Instructions, Object-Kind, Execution #) -> AMI-Struct of N;
sel Instruction-Counter c₂ -> Element of the carrier of c₂;
sel Instructions c₂ -> non empty set ;
sel Object-Kind c₂ -> Function of the carrier of c₂,(N \/ {the Instructions of c₂,NAT });
sel Execution c₂ -> Action of the Instructions of c₂,(product the Object-Kind of c₂);

end;

definition

let N be set ;
canceled;
func Trivial-AMI N -> strict AMI-Struct of N means :Def2: :: AMI_1:def 2
( the carrier of it = succ NAT & the Instruction-Counter of it = NAT & the Instructions 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 b₁ being strict AMI-Struct of N st
( the carrier of b₁ = succ NAT & the Instruction-Counter of b₁ = NAT & the Instructions of b₁ = {[0 ,{} ]} & the Object-Kind of b₁ = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b₁ = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) )

proof end;

uniqueness
for b₁, b₂ being strict AMI-Struct of N st the carrier of b₁ = succ NAT & the Instruction-Counter of b₁ = NAT & the Instructions of b₁ = {[0 ,{} ]} & the Object-Kind of b₁ = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b₁ = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) & the carrier of b₂ = succ NAT & the Instruction-Counter of b₂ = NAT & the Instructions of b₂ = {[0 ,{} ]} & the Object-Kind of b₂ = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b₂ = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) holds
b₁ = b₂ ;

end;

:: deftheorem AMI_1:def 1 :

canceled;

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

for N being set
for b₂ being strict AMI-Struct of N holds
( b₂ = Trivial-AMI N iff ( the carrier of b₂ = succ NAT & the Instruction-Counter of b₂ = NAT & the Instructions of b₂ = {[0 ,{} ]} & the Object-Kind of b₂ = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b₂ = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) ) );

definition

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

end;

:: deftheorem Def3 defines stored-program AMI_1:def 3 :

for N being set
for S being AMI-Struct of N holds
( S is stored-program iff NAT c= the carrier of S );

registration

let N be set ;
cluster Trivial-AMI N -> non empty strict stored-program ;
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 b₁ being AMI-Struct of N st
( not b₁ is empty & b₁ is stored-program )

proof end;

end;

definition

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

end;

definition

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

end;

definition

canceled;
let N be set ;
let S be non empty AMI-Struct of 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 AMI_1:def 4 :

canceled;

:: deftheorem defines IC AMI_1:def 5 :

for N being set
for S being non empty AMI-Struct of N holds IC S = the Instruction-Counter of S;

definition

let N be set ;
let S be non empty AMI-Struct of N;
let o be Object of S;
func ObjectKind o -> Element of N \/ {the Instructions of S,NAT } 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,NAT };
;

end;

:: deftheorem defines ObjectKind AMI_1:def 6 :

for N being set
for S being non empty AMI-Struct of N
for o being Object of S holds ObjectKind o = the Object-Kind of S . o;

definition

let N be set ;
let S be AMI-Struct of N;
mode PartState of S is the carrier of S -defined the Object-Kind of S -compatible Function;

end;

definition

let N be set ;
let S be AMI-Struct of N;
mode FinPartState of S is finite PartState of S;

end;

definition

let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
mode State of S is total PartState of S;

end;

definition

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 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
ex I being Instruction of S st I 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 ex I being Instruction of S st I is halting );

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 b₁ being AMI-Struct of N st b₁ is halting

proof end;

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 b₁ being Instruction of S st b₁ is halting by Def9;

end;

definition

let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
func halt S -> Instruction of S equals :: AMI_1:def 10
the halting Instruction of S;
coherence
the halting Instruction of S is Instruction of S ;

end;

:: deftheorem defines halt AMI_1:def 10 :

for N being with_non-empty_elements set
for S being halting AMI-Struct of N holds halt S = the halting Instruction of S;

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 ;

end;

definition

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

end;

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

for N being set
for IT being non empty AMI-Struct of N holds
( IT is IC-Ins-separated iff ObjectKind (IC IT) = NAT );

definition

let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
let I be FinPartState of S;
attr I is halt-free means :: AMI_1:def 12
not halt S in rng I;

end;

:: deftheorem defines halt-free AMI_1:def 12 :

for N being with_non-empty_elements set
for S being halting AMI-Struct of N
for I being FinPartState of S holds
( I is halt-free iff not halt S in rng I );

definition

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

definition

let N be set ;
let IT be non empty stored-program AMI-Struct of N;
attr IT is definite means :Def14: :: AMI_1:def 14
for l being Element of NAT holds the Object-Kind of IT . l = the Instructions of IT;

end;

:: deftheorem Def14 defines definite AMI_1:def 14 :

for N being set
for IT being non empty stored-program AMI-Struct of N holds
( IT is definite iff for l being Element of NAT holds the Object-Kind of IT . l = the Instructions of IT );

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 -> strict IC-Ins-separated definite ;
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 strict stored-program IC-Ins-separated definite AMI-Struct of M;
existence
ex b₁ being non empty stored-program AMI-Struct of M st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ is strict )

proof end;

end;

registration

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

proof end;

end;

definition

let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let p be PartState of S;
func IC p -> Element of NAT equals :: AMI_1:def 15
p . (IC S);
coherence
p . (IC S) is Element of NAT

proof end;

end;

:: deftheorem defines IC AMI_1:def 15 :

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p being PartState of S holds IC p = p . (IC S);

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

let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let p be the Instructions of S -valued Function;
let s be State of S;
func CurInstr p,s -> Instruction of S equals :: AMI_1:def 16
p /. (IC s);
coherence
p /. (IC s) is Instruction of S ;

end;

:: deftheorem defines CurInstr AMI_1:def 16 :

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p being the Instructions of b₂ -valued Function
for s being State of S holds CurInstr p,s = p /. (IC s);

definition

let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
let s be PartState of S;
func ProgramPart s -> PartState of S equals :: AMI_1:def 17
s | NAT ;
coherence
s | NAT is PartState of S ;

end;

:: deftheorem defines ProgramPart AMI_1:def 17 :

for N being with_non-empty_elements set
for S being AMI-Struct of N
for s being PartState of S holds ProgramPart s = s | NAT ;

registration

let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
let s be PartState of S;
cluster ProgramPart s -> NAT -defined ;
coherence
ProgramPart s is NAT -defined ;

end;

BWL: 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 i being natural number holds (ProgramPart s) . i = s . i

proof end;

BWL2: 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 PartState of S
for i being natural number st i in dom s holds
(ProgramPart s) . i = s . i

proof end;

registration

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 s be PartState of S;
cluster ProgramPart s -> the Instructions of S -valued ;
coherence
ProgramPart s is the Instructions of S -valued

proof end;

end;

LmU: for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of N
for s being State of S holds dom (ProgramPart s) = NAT

proof end;

BWL1: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i

proof end;

definition

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 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 b₂ -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 H₁( 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 b₁ being State of S ex f being Function of NAT ,(product the Object-Kind of S) st
( b₁ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) )

proof end;

uniqueness
for b₁, b₂ being State of S st ex f being Function of NAT ,(product the Object-Kind of S) st
( b₁ = 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
( b₂ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) holds
b₁ = b₂

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 b₂ -valued Function
for s being State of S
for k being Nat
for b₆ being State of S holds
( b₆ = Comput p,s,k iff ex f being Function of NAT ,(product the Object-Kind of S) st
( b₆ = 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 halting IC-Ins-separated definite 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 halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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 ) );

definition

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

end;

:: deftheorem Def21 defines realistic AMI_1:def 21 :

for N being set
for IT being AMI-Struct of N holds
( IT is realistic iff not the Instruction-Counter of IT in NAT );

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 b₂ -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 b₂ -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

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 i being natural number holds (ProgramPart s) . i = s . i by BWL;

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 E being set
for S being non empty IC-Ins-separated AMI-Struct of E st S is realistic holds
for l being Element of NAT holds not IC S = l by Def21;

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 b₃ -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 halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b₄ -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

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite 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 b₁, b₂ being State of S st ex k being Element of NAT st
( b₁ = Comput p,s,k & CurInstr p,b₁ = halt S ) & ex k being Element of NAT st
( b₂ = Comput p,s,k & CurInstr p,b₂ = halt S ) holds
b₁ = b₂

proof end;

correctness
existence
ex b₁ being State of S ex k being Element of NAT st
( b₁ = Comput p,s,k & CurInstr p,b₁ = halt S );

proof end;

end;

:: 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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued Function
for s being State of S st p halts_on s holds
for b₅ being State of S holds
( b₅ = Result p,s iff ex k being Element of NAT st
( b₅ = Comput p,s,k & CurInstr p,b₅ = halt S ) );

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of N;
let s be State of S;
let l be Element of NAT ;
:: original: .
redefine func s . l -> Instruction of S;
coherence
s . l is Instruction of S

proof end;

end;

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 steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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;

registration

let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
let p be FinPartState of S;
cluster ProgramPart p -> finite ;
coherence
ProgramPart p is finite ;

end;

registration

let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
let p be PartState of S;
cluster ProgramPart p -> NAT -defined ;
coherence
ProgramPart p is NAT -defined ;

end;

LmL: for N being with_non-empty_elements set
for S being stored-program AMI-Struct of N
for s being State of S holds NAT c= dom s

proof end;

registration

let N be with_non-empty_elements set ;
let S be stored-program AMI-Struct of N;
let s be State of S;
cluster ProgramPart s -> total ;
coherence
ProgramPart s is total

proof end;

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 steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N;
let P be the Instructions of S -valued ManySortedSet of NAT ;
let k be Nat;
:: original: .
redefine func P . k -> Instruction of S;
coherence
P . k is Instruction of S

proof end;

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 steady-programmed definite AMI-Struct of N
for P being the Instructions of b₃ -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;

L94: for N being with_non-empty_elements set
for S being non empty AMI-Struct of N
for s being State of S holds IC S in dom s

proof end;

theorem Th56: :: AMI_1:56

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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;

registration

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

end;

begin

definition

let N be set ;
let S be AMI-Struct of N;
func FinPartSt S -> Subset of (sproduct the Object-Kind of S) equals :: AMI_1:def 23
{ p where p is Element of sproduct the Object-Kind of S : p is finite } ;
coherence
{ 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 N being set
for S being AMI-Struct of N holds FinPartSt S = { p where p is Element of sproduct the Object-Kind of S : p is finite } ;

definition

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

end;

:: deftheorem defines Data-Locations AMI_1:def 24 :

for N being set
for S being non empty AMI-Struct of N holds Data-Locations S = the carrier of S \ ({(IC S)} \/ NAT );

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 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 (Comput (ProgramPart s1),s1,i) | (dom IT) = (Comput (ProgramPart s2),s2,i) | (dom IT);

end;

:: 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 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 (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 halting IC-Ins-separated definite AMI-Struct of N;
let IT be FinPartState of S;
attr IT is halting means :Def26: :: AMI_1:def 26
for s being State of S st IT c= s holds
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 halting IC-Ins-separated definite AMI-Struct of N
for IT being FinPartState of S holds
( IT is halting iff for s being State of S st IT c= s holds
ProgramPart s halts_on s );

theorem Th58: :: AMI_1:58

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

proof end;

theorem Th59: :: AMI_1:59

for N being non empty with_non-empty_elements set
for S being non empty AMI-Struct of N
for A being set
for la being Object of S st the Object-Kind of S . la = A holds
for a being Element of A holds la .--> a is FinPartState of S

proof end;

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

registration

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

proof end;

end;

registration

let E be set ;
cluster strict realistic AMI-Struct of E;
existence
ex b₁ being AMI-Struct of E st
( b₁ is realistic & b₁ is strict )

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let N be set ;
let S be AMI-Struct of N;
let f, g be PartState of S;
cluster f +* g -> the carrier of S -defined the Object-Kind of S -compatible Function;
coherence
for b₁ being Function st b₁ = f +* g holds
( b₁ is the carrier of S -defined & b₁ is the Object-Kind of S -compatible ) ;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
func Start-At l,S -> FinPartState of S equals :: AMI_1:def 27
(IC S) .--> l;
correctness
coherence
(IC S) .--> l is FinPartState of S;

proof end;

end;

:: deftheorem defines Start-At AMI_1:def 27 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l being Nat holds Start-At l,S = (IC S) .--> l;

begin

theorem :: AMI_1:60

canceled;

theorem :: AMI_1:61

canceled;

theorem :: AMI_1:62

canceled;

theorem :: AMI_1:63

canceled;

theorem Th64: :: AMI_1:64

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for l being Nat
for I being Instruction of S
for p being FinPartState of S
for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I

proof end;

theorem Th65: :: AMI_1:65

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for l being Nat
for p being FinPartState 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 halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for l being Nat
for p being FinPartState 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 halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for l being Nat
for p being FinPartState of S st p = (IC S),l --> l,(halt S) holds
p is autonomic

proof end;

definition

let N be with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
let p be PartState of S;
attr p is l -started means :Def41: :: AMI_1:def 28
( IC S in dom p & IC p = l );

end;

:: deftheorem Def41 defines -started AMI_1:def 28 :

for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l being Nat
for p being PartState of S holds
( p is l -started iff ( IC S in dom p & IC p = l ) );

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N;
cluster autonomic halting set ;
existence
ex b₁ being FinPartState of S st
( b₁ is autonomic & b₁ is halting )

proof end;

end;

definition

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

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic 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 b₁ being FinPartState of S st
for s being State of S st d c= s holds
b₁ = (Result (ProgramPart s),s) | (dom d)

proof end;

correctness
uniqueness
for b₁, b₂ being FinPartState of S st ( for s being State of S st d c= s holds
b₁ = (Result (ProgramPart s),s) | (dom d) ) & ( for s being State of S st d c= s holds
b₂ = (Result (ProgramPart s),s) | (dom d) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem defines Result AMI_1:def 29 :

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued Function
for d being FinPartState of S st d is pre-program of S & p = ProgramPart d holds
for b₅ being FinPartState of S holds
( b₅ = Result p,d iff for s being State of S st d c= s holds
b₅ = (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 halting IC-Ins-separated steady-programmed definite realistic 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 halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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 halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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 halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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 halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued Function
for d being FinPartState of S holds
( p +* d is pre-program of S iff p,d computes {} .--> {} )

proof end;

begin

notation

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

end;

definition

let N be set ;
let S be AMI-Struct of N;
canceled;
attr S is standard-ins means :Def32: :: AMI_1:def 32
ex X being non empty set st the Instructions of S c= [:NAT ,(X * ):];

end;

:: deftheorem AMI_1:def 31 :

canceled;

:: deftheorem Def32 defines standard-ins AMI_1:def 32 :

for N being set
for S being AMI-Struct of N holds
( S is standard-ins iff ex X being non empty set st the Instructions of S c= [:NAT ,(X * ):] );

registration

let N be set ;
cluster Trivial-AMI N -> strict standard-ins ;
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 b₁ being AMI-Struct of N st
( b₁ is standard-ins & not b₁ is empty & b₁ is stored-program )

proof end;

end;

registration

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

proof end;

end;

registration

let N be set ;
let S be non empty standard-ins AMI-Struct of N;
let x be Instruction of S;
cluster InsCode x -> natural ;
coherence
InsCode x is natural

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 b₁ being non empty stored-program AMI-Struct of N st
( b₁ is IC-Ins-separated & b₁ is definite & b₁ is standard-ins )

proof end;

end;

registration

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

end;

definition

let N be set ;
let S be standard-ins AMI-Struct of 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 N being set
for S being standard-ins AMI-Struct of N holds InsCodes S = dom the Instructions of S;

definition

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

end;

definition

let N be set ;
let S be standard-ins AMI-Struct of 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;

begin

LMT: for N being with_non-empty_elements set
for S being AMI-Struct of N
for p being FinPartState of S holds p in FinPartSt S

proof end;

registration

let N be with_non-empty_elements set ;
let S be AMI-Struct of N;
cluster FinPartSt S -> non empty ;
coherence
not FinPartSt S is empty by LMT;

end;

registration

let N be set ;
let S be AMI-Struct of N;
cluster NAT -defined the Instructions of S -valued set ;
existence
ex b₁ being FinPartState of S st
( b₁ is NAT -defined & b₁ is the Instructions of S -valued )

proof end;

end;

registration

let N be set ;
let S be non empty stored-program definite AMI-Struct of N;
cluster NAT -defined the Instructions of S -valued -> the Object-Kind of S -compatible set ;
coherence
for b₁ being Function st b₁ is NAT -defined & b₁ is the Instructions of S -valued holds
b₁ is the Object-Kind of S -compatible

proof end;

end;

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 steady-programmed definite AMI-Struct of N
for p being NAT -defined FinPartState of
for P being the Instructions of b₂ -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;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
cluster Start-At l,S -> l -started ;
coherence
Start-At l,S is l -started

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
cluster l -started set ;
existence
ex b₁ being FinPartState of S st b₁ is l -started

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be AMI-Struct of N;
let s be State of S;
let p be PartState of S;
cluster s +* p -> total PartState of S;
coherence
for b₁ being PartState of S st b₁ = s +* p holds
b₁ is total ;
cluster p +* s -> total PartState of S;
coherence
for b₁ being PartState of S st b₁ = p +* s holds
b₁ is total ;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
let p be PartState of S;
let q be l -started PartState of S;
cluster p +* q -> l -started ;
coherence
p +* q is l -started

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
cluster l -started set ;
existence
ex b₁ being State of S st b₁ is l -started

proof end;

end;

definition

canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
let p be NAT -defined the Instructions of S -valued Function;
let l be set ;
pred p halts_at l means :Def42: :: AMI_1:def 42
( l in dom p & p . l = halt S );

end;

:: 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 Def42 defines halts_at AMI_1:def 42 :

for N being with_non-empty_elements set
for S being halting AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );

definition

canceled;
let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let l be Nat;
let s be State of S;
redefine attr s is l -started means :: AMI_1:def 44
IC s = l;
compatibility
( s is l -started iff IC s = l )

proof end;

end;

:: deftheorem AMI_1:def 43 :

canceled;

:: deftheorem defines -started AMI_1:def 44 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l being Nat
for s being State of S holds
( s is l -started iff IC s = l );

definition

let N be with_non-empty_elements set ;
let S be non empty halting AMI-Struct of N;
let s be the Instructions of S -valued ManySortedSet of NAT ;
let l be Nat;
redefine pred s halts_at l means :Def45: :: AMI_1:def 45
s . l = halt S;
compatibility
( s halts_at l iff s . l = halt S )

proof end;

end;

:: deftheorem Def45 defines halts_at AMI_1:def 45 :

for N being with_non-empty_elements set
for S being non empty halting AMI-Struct of N
for s being the Instructions of b₂ -valued ManySortedSet of NAT
for l being Nat holds
( s halts_at l iff s . l = halt S );

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 halting IC-Ins-separated definite AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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;

L105: for N being non empty with_non-empty_elements set
for S being non empty AMI-Struct of N
for p being NAT -defined FinPartState of holds ProgramPart p = p

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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -valued ManySortedSet of NAT
for s being State of S
for k being Element of 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 steady-programmed definite AMI-Struct of N
for s being State of S
for p being NAT -defined FinPartState 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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -valued ManySortedSet of NAT
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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₄ -valued ManySortedSet of NAT
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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₄ -valued ManySortedSet of NAT
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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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;

theorem :: AMI_1:91

canceled;

theorem :: AMI_1:92

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 l being Nat
for p being b₃ -started PartState of S
for s being PartState of S st p c= s holds
s is l -started

proof end;

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 l be Element of NAT ;
let I be Element of the Instructions of S;
:: original: .-->
redefine func l .--> I -> NAT -defined FinPartState of ;
coherence
l .--> I is NAT -defined FinPartState of

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite 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 b₁ being Element of NAT st
( CurInstr p,(Comput p,s,b₁) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b₁ <= k ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st CurInstr p,(Comput p,s,b₁) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b₁ <= k ) & CurInstr p,(Comput p,s,b₂) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b₂ <= k ) holds
b₁ = b₂

proof end;

end;

:: 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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued Function
for s being State of S st p halts_on s holds
for b₅ being Element of NAT holds
( b₅ = LifeSpan p,s iff ( CurInstr p,(Comput p,s,b₅) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b₅ <= k ) ) );

theorem :: AMI_1:93

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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 Th94: :: AMI_1:94

for N being with_non-empty_elements set
for S being non empty AMI-Struct of N
for s being State of S holds IC S in dom s by L94;

theorem :: AMI_1:95

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for s being State of S holds Start-At (IC s),S = s | {(IC S)}

proof end;

definition

let N be set ;
let S be non empty AMI-Struct of N;
let p be PartState of S;
canceled;
canceled;
canceled;
func DataPart p -> PartState of S equals :: AMI_1:def 50
p | (Data-Locations S);
coherence
p | (Data-Locations S) is PartState of S ;
projectivity
for b₁, b₂ being PartState of S st b₁ = b₂ | (Data-Locations S) holds
b₁ = b₁ | (Data-Locations S) by RELAT_1:101;

end;

:: deftheorem AMI_1:def 47 :

canceled;

:: deftheorem AMI_1:def 48 :

canceled;

:: deftheorem AMI_1:def 49 :

canceled;

:: deftheorem defines DataPart AMI_1:def 50 :

for N being set
for S being non empty AMI-Struct of N
for p being PartState of S holds DataPart p = p | (Data-Locations S);

registration

let N be set ;
let S be non empty AMI-Struct of N;
let p be FinPartState of S;
cluster DataPart p -> finite ;
coherence
DataPart p is finite ;

end;

definition

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

end;

:: deftheorem Def50 defines data-only AMI_1:def 51 :

for N being set
for S being non empty AMI-Struct of N
for IT being PartState of S holds
( IT is data-only iff dom IT misses {(IC S)} \/ NAT );

registration

let N be set ;
let S be non empty AMI-Struct of N;
cluster data-only set ;
existence
ex b₁ being FinPartState of S st b₁ is data-only

proof end;

end;

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 steady-programmed definite AMI-Struct of 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= Comput (ProgramPart s),s,i

proof end;

theorem Th100: :: AMI_1:100

for N being set
for S being non empty AMI-Struct of N
for p being FinPartState of S holds not IC S in dom (DataPart p)

proof end;

theorem Th101: :: AMI_1:101

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S holds not IC S in dom (ProgramPart p)

proof end;

theorem :: AMI_1:102

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

theorem :: AMI_1:103

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of 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 N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p, q being FinPartState of S holds dom (DataPart p) misses dom (ProgramPart q)

proof end;

theorem Th105: :: AMI_1:105

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p being NAT -defined FinPartState of holds ProgramPart p = p by L105;

theorem :: AMI_1:106

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for p being FinPartState of S
for l being Element of NAT st l in dom p holds
l in dom (ProgramPart p)

proof end;

theorem :: AMI_1:107

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of 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 N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S st IC S in dom p holds
p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty IC-Ins-separated AMI-Struct of N;
let IT be PartFunc of (FinPartSt S),(FinPartSt S);
attr IT is data-only means :: AMI_1:def 52
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 52 :

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of 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 N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S st IC S in dom p holds
not p is NAT -defined

proof end;

theorem :: AMI_1:110

canceled;

theorem :: AMI_1:111

canceled;

theorem :: AMI_1:112

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for s being State of S
for iloc, a being Element of NAT holds s . a = (s +* (Start-At iloc,S)) . a

proof end;

theorem :: AMI_1:113

canceled;

theorem :: AMI_1:114

for N being with_non-empty_elements set
for S being stored-program AMI-Struct of N
for s being State of S holds NAT c= dom s by LmL;

theorem :: AMI_1:115

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated AMI-Struct of N
for s being State of S holds IC s in dom s

proof end;

theorem :: AMI_1:116

for N being with_non-empty_elements set
for S being non empty stored-program AMI-Struct of N
for s being State of S
for l being Element of NAT holds l in dom s

proof end;

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;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program definite AMI-Struct of N;
let s be NAT -defined PartState of ;
let f be Function of the Instructions of S,the Instructions of S;
:: original: *
redefine func f * s -> NAT -defined PartState of ;
coherence
s * f is NAT -defined PartState of by RELAT_1:def 18;

end;

theorem :: AMI_1:118

canceled;

theorem :: AMI_1:119

canceled;

theorem :: AMI_1:120

canceled;

theorem :: AMI_1:121

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of N
for s1, s2 being State of S st s1,s2 equal_outside NAT holds
IC s1 = IC s2

proof end;

theorem :: AMI_1:122

for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -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;

definition

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 l be Element of NAT ;
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 N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite 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 steady-programmed definite AMI-Struct of N
for p being NAT -defined the Instructions of b₃ -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

for N being non empty with_non-empty_elements set
for S being AMI-Struct of N
for p being Element of FinPartSt S holds p is FinPartState of S

proof end;

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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for p being NAT -defined the Instructions of b₃ -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 steady-programmed definite realistic 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 halting IC-Ins-separated definite AMI-Struct of N
for P being the Instructions of b₂ -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 steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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 steady-programmed definite realistic 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 Th134: :: AMI_1:134

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of N
for l being Element of NAT holds dom (Start-At l,S) misses NAT

proof end;

theorem :: AMI_1:135

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of N
for l being Element of NAT holds ProgramPart (Start-At l,S) = {}

proof end;

registration

let N be set ;
let S be non empty AMI-Struct of 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 N being with_non-empty_elements set
for S being non empty AMI-Struct of N
for p being data-only FinPartState of S holds ProgramPart p = {}

proof end;

theorem :: AMI_1:137

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated realistic AMI-Struct of N
for l, l1 being Element of NAT holds not l in dom (Start-At l1,S)

proof end;

theorem :: AMI_1:138

for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of N
for l being Element of NAT holds DataPart (Start-At l,S) = {}

proof end;

theorem Th139: :: AMI_1:139

for N being non empty with_non-empty_elements set
for S being non empty AMI-Struct of 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 N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for s being State of S
for X being set st X c= NAT holds
rng (s | X) c= the Instructions of S

proof end;

theorem :: AMI_1:141

canceled;

theorem :: AMI_1:142

for N being non empty with_non-empty_elements set
for S being non empty AMI-Struct of N
for p being PartState of S holds
( p is data-only iff DataPart p = p )

proof end;

theorem :: AMI_1:143

for N being with_non-empty_elements set
for S being non empty stored-program steady-programmed AMI-Struct of N
for s being State of S holds dom (ProgramPart s) = NAT by LmU;

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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for P being the Instructions of b₂ -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;

theorem :: AMI_1:147

for N being with_non-empty_elements set
for S being AMI-Struct of N
for p being FinPartState of S holds p in FinPartSt S by LMT;

theorem :: AMI_1:148

for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of N
for f being NAT -defined the Instructions of b₂ -valued Function holds f is PartState of S

proof end;

theorem :: AMI_1:149

for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for n being Nat
for i being Instruction of S holds (IC S),n --> n,i is PartState of S

proof end;

theorem :: AMI_1:150

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i by BWL1;

theorem :: AMI_1:151

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s1, s2 being State of S holds ProgramPart (s1 +* (DataPart s2)) = ProgramPart s1

proof end;

theorem :: AMI_1:152

canceled;

theorem :: AMI_1:153

canceled;

theorem :: AMI_1:154

canceled;

theorem :: AMI_1:155

for N being set
for S being non empty AMI-Struct of N
for d being data-only PartState of S holds dom d misses NAT

proof end;