begin
definition
let N be
set ;
canceled;func Trivial-AMI N -> strict AMI-Struct of
N means :
Def2:
( 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 b1 being strict AMI-Struct of N st
( the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,{} ]} & the Object-Kind of b1 = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b1 = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) )
uniqueness
for b1, b2 being strict AMI-Struct of N st the carrier of b1 = succ NAT & the Instruction-Counter of b1 = NAT & the Instructions of b1 = {[0 ,{} ]} & the Object-Kind of b1 = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b1 = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) & the carrier of b2 = succ NAT & the Instruction-Counter of b2 = NAT & the Instructions of b2 = {[0 ,{} ]} & the Object-Kind of b2 = (NAT --> {[0 ,{} ]}) +* (NAT .--> NAT ) & the Execution of b2 = [0 ,{} ] .--> (id (product ((NAT --> {[0 ,{} ]}) +* (NAT .--> NAT )))) holds
b1 = b2
;
end;
:: deftheorem AMI_1:def 1 :
canceled;
:: deftheorem Def2 defines Trivial-AMI AMI_1:def 2 :
:: deftheorem Def3 defines stored-program AMI_1:def 3 :
:: deftheorem AMI_1:def 4 :
canceled;
:: deftheorem defines IC AMI_1:def 5 :
:: deftheorem defines ObjectKind AMI_1:def 6 :
:: deftheorem defines Exec AMI_1:def 7 :
:: deftheorem Def8 defines halting AMI_1:def 8 :
:: deftheorem Def9 defines halting AMI_1:def 9 :
:: deftheorem defines halt AMI_1:def 10 :
:: deftheorem Def11 defines IC-Ins-separated AMI_1:def 11 :
:: deftheorem defines halt-free AMI_1:def 12 :
:: deftheorem Def13 defines steady-programmed AMI_1:def 13 :
:: deftheorem Def14 defines definite AMI_1:def 14 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
:: deftheorem defines IC AMI_1:def 15 :
theorem
canceled;
theorem
canceled;
theorem
begin
:: deftheorem defines CurInstr AMI_1:def 16 :
:: deftheorem defines ProgramPart AMI_1:def 17 :
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
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
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
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
:: deftheorem defines Following AMI_1:def 18 :
definition
let N be non
empty with_non-empty_elements set ;
let S be non
empty stored-program IC-Ins-separated definite AMI-Struct of
N;
let p be
NAT -defined the
Instructions of
S -valued Function;
deffunc H1(
set ,
State of
S)
-> Element of
product the
Object-Kind of
S =
down (Following p,$2);
let s be
State of
S;
let k be
Nat;
func Comput p,
s,
k -> State of
S means :
Def19:
ex
f being
Function of
NAT ,
(product the Object-Kind of S) st
(
it = f . k &
f . 0 = s & ( for
i being
Nat holds
f . (i + 1) = Following p,
(f . i) ) );
existence
ex b1 being State of S ex f being Function of NAT ,(product the Object-Kind of S) st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) )
uniqueness
for b1, b2 being State of S st ex f being Function of NAT ,(product the Object-Kind of S) st
( b1 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) & ex f being Function of NAT ,(product the Object-Kind of S) st
( b2 = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following p,(f . i) ) ) holds
b1 = b2
end;
:: deftheorem Def19 defines Comput AMI_1:def 19 :
:: deftheorem Def20 defines halts_on AMI_1:def 20 :
:: deftheorem Def21 defines realistic AMI_1:def 21 :
theorem Th13:
theorem Th14:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th48:
theorem
canceled;
theorem
canceled;
theorem Th51:
theorem Th52:
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:
ex
k being
Element of
NAT st
(
it = Comput p,
s,
k &
CurInstr p,
it = halt S );
uniqueness
for b1, b2 being State of S st ex k being Element of NAT st
( b1 = Comput p,s,k & CurInstr p,b1 = halt S ) & ex k being Element of NAT st
( b2 = Comput p,s,k & CurInstr p,b2 = halt S ) holds
b1 = b2
correctness
existence
ex b1 being State of S ex k being Element of NAT st
( b1 = Comput p,s,k & CurInstr p,b1 = halt S );
end;
:: deftheorem Def22 defines Result AMI_1:def 22 :
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
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 b2 -valued ManySortedSet of NAT
for s being State of S
for n being Element of NAT holds ProgramPart s = ProgramPart (Comput P,s,n)
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
theorem
canceled;
theorem Th54:
theorem
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
theorem Th56:
theorem Th57:
begin
:: deftheorem defines FinPartSt AMI_1:def 23 :
:: deftheorem defines Data-Locations AMI_1:def 24 :
:: deftheorem Def25 defines autonomic AMI_1:def 25 :
:: deftheorem Def26 defines halting AMI_1:def 26 :
theorem Th58:
theorem Th59:
:: deftheorem defines Start-At AMI_1:def 27 :
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
:: deftheorem Def41 defines -started AMI_1:def 28 :
:: deftheorem defines Result AMI_1:def 29 :
begin
:: deftheorem Def29 defines computes AMI_1:def 30 :
theorem
theorem
theorem
begin
:: deftheorem AMI_1:def 31 :
canceled;
:: deftheorem Def32 defines standard-ins AMI_1:def 32 :
:: deftheorem defines InsCodes AMI_1:def 33 :
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
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th81:
:: 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 :
:: deftheorem AMI_1:def 43 :
canceled;
:: deftheorem defines -started AMI_1:def 44 :
:: deftheorem Def45 defines halts_at AMI_1:def 45 :
theorem
canceled;
theorem Th83:
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
theorem
canceled;
theorem Th85:
theorem
theorem Th87:
theorem Th88:
theorem
theorem
theorem
canceled;
theorem
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:
(
CurInstr p,
(Comput p,s,it) = halt S & ( for
k being
Element of
NAT st
CurInstr p,
(Comput p,s,k) = halt S holds
it <= k ) );
existence
ex b1 being Element of NAT st
( CurInstr p,(Comput p,s,b1) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b1 <= k ) )
uniqueness
for b1, b2 being Element of NAT st CurInstr p,(Comput p,s,b1) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b1 <= k ) & CurInstr p,(Comput p,s,b2) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
b2 <= k ) holds
b1 = b2
end;
:: deftheorem Def46 defines LifeSpan AMI_1:def 46 :
theorem
theorem Th94:
theorem
:: 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 :
:: deftheorem Def50 defines data-only AMI_1:def 51 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th100:
theorem Th101:
theorem
theorem
theorem Th104:
theorem Th105:
theorem
theorem
theorem
:: deftheorem defines data-only AMI_1:def 52 :
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem Th134:
theorem
theorem
theorem
theorem
theorem Th139:
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem