:: 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₂ -> Function of the Instructions of c₂,(Funcs (product the Object-Kind of c₂),(product the Object-Kind of c₂));

end;

definition

let N be set ;
canceled;
func Trivial-AMI N -> strict AMI-Struct of N means :Def2: :: AMI_1:def 2
( the carrier of it = 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 IT be non empty AMI-Struct of N;
canceled;
attr IT is steady-programmed means :Def13: :: AMI_1:def 13
for s being State of IT
for i being Instruction of IT
for l being Element of NAT holds (Exec i,s) . l = s . l;

end;

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

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 E be set ;
cluster strict AMI-Struct of E;
existence
ex b₁ being AMI-Struct of E st b₁ is strict

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;

registration

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;
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 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 with_non-empty_elements set ;
let S be AMI-Struct of N;
let f be Function of NAT ,(product the Object-Kind of S);
let k be Element of NAT ;
:: original: .
redefine func f . k -> Element of product the Object-Kind of S;
coherence
f . k is Element of product the Object-Kind of S by FUNCT_2:7;

end;

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 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 Element of NAT st
( IC (Comput (ProgramPart s),s,k) in dom p & p /. (IC (Comput (ProgramPart s),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 the Instructions of b₂ -valued Function
for s being State of S holds
( p halts_on s iff ex k being Element of NAT st
( IC (Comput (ProgramPart s),s,k) in dom p & p /. (IC (Comput (ProgramPart s),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

canceled;

theorem :: AMI_1:16

canceled;

theorem :: AMI_1:17

canceled;

theorem :: AMI_1:18

canceled;

theorem :: AMI_1:19

canceled;

theorem :: AMI_1:20

canceled;

theorem :: AMI_1:21

canceled;

theorem :: AMI_1:22

canceled;

theorem :: AMI_1:23

canceled;

theorem :: AMI_1:24

canceled;

theorem :: AMI_1:25

canceled;

theorem :: AMI_1:26

canceled;

theorem :: AMI_1:27

canceled;

theorem :: AMI_1:28

canceled;

theorem :: AMI_1:29

canceled;

theorem :: AMI_1:30

canceled;

theorem :: AMI_1:31

canceled;

theorem :: AMI_1:32

canceled;

theorem :: AMI_1:33

canceled;

theorem :: AMI_1:34

canceled;

theorem :: AMI_1:35

canceled;

theorem :: AMI_1:36

canceled;

theorem :: AMI_1:37

canceled;

theorem :: AMI_1:38

canceled;

theorem :: AMI_1:39

canceled;

theorem :: AMI_1:40

canceled;

theorem :: AMI_1:41

canceled;

theorem :: AMI_1:42

canceled;

theorem :: AMI_1:43

canceled;

theorem :: AMI_1:44

canceled;

theorem :: AMI_1:45

canceled;

theorem :: AMI_1:46

canceled;

theorem :: AMI_1:47

canceled;

theorem Th48: :: AMI_1:48

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

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 (Exec i,s) | NAT = s | NAT

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 s being State of S
for n being Element of NAT holds s | NAT = (Comput (ProgramPart s),s,n) | NAT

proof end;

LmY: 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 k being Element of NAT holds ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k)
by LmA;

LmX: 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 k being Element of NAT holds (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k)

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 s be State of S;
assume A1: ProgramPart s halts_on s ;
func Result s -> State of S means :Def22: :: AMI_1:def 22
ex k being Element of NAT st
( it = Comput (ProgramPart s),s,k & CurInstr (ProgramPart it),it = halt S );
uniqueness
for b₁, b₂ being State of S st ex k being Element of NAT st
( b₁ = Comput (ProgramPart s),s,k & CurInstr (ProgramPart b₁),b₁ = halt S ) & ex k being Element of NAT st
( b₂ = Comput (ProgramPart s),s,k & CurInstr (ProgramPart b₂),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 (ProgramPart s),s,k & CurInstr (ProgramPart b₁),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 s being State of S st ProgramPart s halts_on s holds
for b₄ being State of S holds
( b₄ = Result s iff ex k being Element of NAT st
( b₄ = Comput (ProgramPart s),s,k & CurInstr (ProgramPart b₄),b₄ = halt S ) );

theorem :: AMI_1:53

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 Element of NAT holds s . i = (Following (ProgramPart s),s) . i by Def13;

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;

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 s being State of S
for i, k being Element of NAT holds s . i = (Comput (ProgramPart s),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 steady-programmed definite AMI-Struct of N
for s being State of S holds Comput (ProgramPart s),s,(k + 1) = Exec (s . (IC (Comput (ProgramPart s),s,k))),(Comput (ProgramPart s),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 halting IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt S holds
Result s = Comput (ProgramPart s),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 s being State of S st ex k being Element of NAT st s . (IC (Comput (ProgramPart s),s,k)) = halt S holds
for i being Element of NAT holds Result s = Result (Comput (ProgramPart s),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;

definition

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

end;

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;

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 Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V118() 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 s be FinPartState of S;
canceled;
assume A1: s is pre-program of S ;
func Result s -> FinPartState of S means :: AMI_1:def 28
for s9 being State of S st s c= s9 holds
it = (Result s9) | (dom s);
existence
ex b₁ being FinPartState of S st
for s9 being State of S st s c= s9 holds
b₁ = (Result s9) | (dom s)

proof end;

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

proof end;

end;

:: deftheorem AMI_1:def 27 :

canceled;

:: deftheorem defines Result AMI_1:def 28 :

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 s being FinPartState of S st s is pre-program of S holds
for b₄ being FinPartState of S holds
( b₄ = Result s iff for s9 being State of S st s c= s9 holds
b₄ = (Result s9) | (dom s) );

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 FinPartState of S;
let F be Function;
pred p computes F means :Def29: :: AMI_1:def 29
for x being set st x in dom F holds
ex s being FinPartState of S st
( x = s & p +* s is pre-program of S & F . s c= Result (p +* s) );

end;

:: deftheorem Def29 defines computes AMI_1:def 29 :

for 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 FinPartState of S
for F being Function holds
( p computes F iff for x being set st x in dom F holds
ex s being FinPartState of S st
( x = s & p +* s is pre-program of S & F . s c= Result (p +* s) ) );

notation

let 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 FinPartState of S;
let F be Function;
antonym p does_not_compute F for p computes F;

end;

theorem Th68: :: 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 FinPartState of S holds p computes {}

proof end;

theorem Th69: :: 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 FinPartState of S holds
( p is pre-program of S iff p computes {} .--> (Result p) )

proof end;

theorem Th70: :: 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 FinPartState of S holds
( p is pre-program of S iff p computes {} .--> {} )

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 realistic AMI-Struct of N;
let IT be PartFunc of (FinPartSt S),(FinPartSt S);
attr IT is computable means :Def30: :: AMI_1:def 30
ex p being FinPartState of S st p computes IT;

end;

:: deftheorem Def30 defines computable AMI_1:def 30 :

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 IT being PartFunc of (FinPartSt S),(FinPartSt S) holds
( IT is computable iff ex p being FinPartState of S st p computes IT );

theorem Th71: :: AMI_1:71

for 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 F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} holds
F is computable

proof end;

theorem Th72: :: AMI_1:72

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 F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> {} holds
F is computable

proof end;

theorem Th73: :: AMI_1:73

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 pre-program of S
for F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> (Result p) holds
F is computable

proof end;

definition

let N be 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 F be PartFunc of (FinPartSt S),(FinPartSt S);
assume A1: F is computable ;
mode Program of F -> FinPartState of S means :: AMI_1:def 31
it computes F;
existence
ex b₁ being FinPartState of S st b₁ computes F by A1, Def30;

end;

:: deftheorem defines Program AMI_1:def 31 :

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 F being PartFunc of (FinPartSt S),(FinPartSt S) st F is computable holds
for b₄ being FinPartState of S holds
( b₄ is Program of F iff b₄ computes F );

theorem :: AMI_1:74

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 F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} holds
for p being FinPartState of S holds p is Program of F

proof end;

theorem :: AMI_1:75

for 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 F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> {} holds
for p being pre-program of S holds p is Program of F

proof end;

theorem :: AMI_1:76

for 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 pre-program of S
for F being PartFunc of (FinPartSt S),(FinPartSt S) st F = {} .--> (Result p) holds
p is Program of F

proof end;

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

definition

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

proof end;

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 defines Start-At AMI_1:def 39 :

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;

registration

let N be set ;
let S be AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V118() set ;
existence
ex b₁ being FinPartState of S st b₁ is NAT -defined

proof end;

end;

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 s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput (ProgramPart s),s,k

proof end;

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 s be State of S;
let l be Element of NAT ;
pred s starts_at l means :: AMI_1:def 41
IC s = l;

end;

:: deftheorem AMI_1:def 40 :

canceled;

:: deftheorem defines starts_at AMI_1:def 41 :

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
for l being Element of NAT holds
( s starts_at l iff IC s = l );

definition

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

end;

:: deftheorem Def42 defines halts_at AMI_1:def 42 :

for N being non empty with_non-empty_elements set
for S being non empty halting IC-Ins-separated AMI-Struct of N
for s being State of S
for l being set holds
( s halts_at l iff s . l = halt S );

definition

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 p be FinPartState of S;
let l be Element of NAT ;
pred p starts_at l means :: AMI_1:def 44
( IC S in dom p & IC p = l );

end;

:: deftheorem AMI_1:def 43 :

canceled;

:: deftheorem defines starts_at AMI_1:def 44 :

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 FinPartState of S
for l being Element of NAT holds
( p starts_at l iff ( IC S in dom p & IC p = l ) );

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

end;

:: deftheorem defines halts_at AMI_1:def 45 :

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

theorem :: AMI_1:82

canceled;

theorem Th83: :: AMI_1:83

for 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 s being State of S holds
( ProgramPart s halts_on s iff ex k being Element of NAT st s halts_at IC (Comput (ProgramPart s),s,k) )

proof end;

theorem :: AMI_1:84

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 s being State of S
for p being FinPartState of S
for l being Element of NAT st p c= s & p halts_at l holds
s halts_at l

proof end;

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 s being State of S
for k being Element of NAT st ProgramPart s halts_on s holds
( Result s = Comput (ProgramPart s),s,k iff s halts_at IC (Comput (ProgramPart s),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 s being State of S
for k being Element of NAT st s halts_at IC (Comput (ProgramPart s),s,k) holds
Result s = Comput (ProgramPart s),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 s being State of S st s halts_at IC (Comput (ProgramPart s),s,i) holds
s halts_at IC (Comput (ProgramPart s),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 s being State of S st s halts_at IC (Comput (ProgramPart s),s,i) holds
Comput (ProgramPart s),s,j = Comput (ProgramPart s),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 s being State of S st ex k being Element of NAT st s halts_at IC (Comput (ProgramPart s),s,k) holds
for i being Element of NAT holds Result s = Result (Comput (ProgramPart s),s,i)

proof end;

theorem :: AMI_1:91

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 s being State of S
for l, k being Element of NAT holds
( s halts_at l iff Comput (ProgramPart s),s,k halts_at l )

proof end;

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 p being FinPartState of S
for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l

proof end;

definition

let 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 s be State of S;
assume A1: ProgramPart s halts_on s ;
func LifeSpan s -> Element of NAT means :Def46: :: AMI_1:def 46
( CurInstr (ProgramPart (Comput (ProgramPart s),s,it)),(Comput (ProgramPart s),s,it) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S holds
it <= k ) );
existence
ex b₁ being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s),s,b₁)),(Comput (ProgramPart s),s,b₁) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S holds
b₁ <= k ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,b₁)),(Comput (ProgramPart s),s,b₁) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S holds
b₁ <= k ) & CurInstr (ProgramPart (Comput (ProgramPart s),s,b₂)),(Comput (ProgramPart s),s,b₂) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),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 s being State of S st ProgramPart s halts_on s holds
for b₄ being Element of NAT holds
( b₄ = LifeSpan s iff ( CurInstr (ProgramPart (Comput (ProgramPart s),s,b₄)),(Comput (ProgramPart s),s,b₄) = halt S & ( for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),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 s being State of S
for m being Element of NAT holds
( ProgramPart s halts_on s iff ProgramPart s halts_on Comput (ProgramPart s),s,m )

proof end;

theorem Th94: :: AMI_1:94

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 IC S in dom s

proof end;

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 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 FinPartState of ;
let loc be set ;
assume A1: loc in dom p ;
func pi p,loc -> Instruction of S equals :: AMI_1:def 47
p . loc;
coherence
p . loc is Instruction of S

proof end;

end;

:: deftheorem defines pi AMI_1:def 47 :

for 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 FinPartState of
for loc being set st loc in dom p holds
pi p,loc = p . loc;

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;

definition

let N be set ;
let S be non empty AMI-Struct of N;
let p be PartState of S;
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 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 Relation-like the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V118() 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

proof end;

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;

definition

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;
:: original: +*
redefine func s +* p -> State of S;
coherence
s +* p is State of S ;

end;

theorem :: AMI_1:110

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 st IC S in dom p holds
Start-At (IC p),S c= p

proof end;

theorem :: AMI_1:111

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
for iloc being Element of NAT holds IC (s +* (Start-At iloc,S)) = iloc

proof end;

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

proof end;

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 (Exec i,s) | NAT = s | NAT by L117;

registration

let N be set ;
let S be AMI-Struct of N;
cluster Relation-like NAT -defined the carrier of S -defined Function-like the Object-Kind of S -compatible finite countable V118() set ;
existence
ex b₁ being FinPartState of S st b₁ is NAT -defined

proof end;

end;

theorem Th118: :: AMI_1:118

for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of N
for p being NAT -defined FinPartState of holds rng p c= the Instructions of S

proof end;

definition

let N be set ;
let S be AMI-Struct of N;
let I, J be NAT -defined PartState of ;
:: original: +*
redefine func I +* J -> NAT -defined PartState of ;
coherence
I +* J is NAT -defined PartState of ;

end;

theorem :: AMI_1:119

for N being with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of N
for f being Function of the Instructions of S,the Instructions of S
for s being NAT -defined FinPartState of holds dom (f * s) = dom s

proof end;

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

proof end;

end;

theorem :: AMI_1:120

for N being with_non-empty_elements set
for A being AMI-Struct of N
for s being State of A
for I being NAT -defined FinPartState of holds s,s +* I equal_outside NAT

proof end;

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 s being State of S st ProgramPart s halts_on s holds
Result s = Comput (ProgramPart s),s,(LifeSpan 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 s | NAT = (Comput (ProgramPart s),s,n) | NAT 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 FinPartState of
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

for N being non empty with_non-empty_elements set
for S being non empty stored-program definite AMI-Struct of N
for I being NAT -defined FinPartState of
for x being set st x in dom I holds
I . x is Instruction of S

proof end;

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 s being State of S
for k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt S holds
Comput (ProgramPart s),s,(LifeSpan s) = Comput (ProgramPart s),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 s being State of S st LifeSpan s <= j & ProgramPart s halts_on s holds
Comput (ProgramPart s),s,j = Comput (ProgramPart s),s,(LifeSpan 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 s being State of S st s = Following (ProgramPart s),s holds
for n being Element of NAT holds Comput (ProgramPart s),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 s being State of S
for i being Instruction of S holds (Exec (s . (IC s)),s) . (IC S) = IC (Following (ProgramPart s),s)

proof end;

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 53
not halt S in rng I;

end;

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

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

theorem :: AMI_1:132

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 st s = Following (ProgramPart s),s holds
for n being Element of NAT holds Comput (ProgramPart s),s,n = s

proof end;

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

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
for l1, l2 being Element of NAT holds (s +* (Start-At l1,S)) +* (Start-At l2,S) = s +* (Start-At l2,S)

proof end;

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

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 k being Element of NAT holds ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by LmY;

theorem :: AMI_1:145

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 k being Element of NAT holds (ProgramPart s) /. (IC (Comput (ProgramPart s),s,k)) = CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) by LmX;

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 s being State of S holds
( ProgramPart s halts_on s iff ex k being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),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 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;