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 Def4 defines Instruction-Location AMI_1:def 4 :
:: 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 AMI_1:def 12 :
canceled;
:: 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 :
:: deftheorem defines Following AMI_1:def 18 :
:: deftheorem Def19 defines Computation 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
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
canceled;
theorem Th48:
theorem
canceled;
theorem
canceled;
theorem Th51:
theorem Th52:
L79:
for N being with_non-empty_elements set
for S being AMI-Struct of N
for s being State of S holds dom s = the carrier of S
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
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
LmY:
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 k being Element of NAT holds ProgramPart s = ProgramPart (Computation s,k)
LmX:
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 k being Element of NAT holds (ProgramPart s) . (IC (Computation s,k)) = CurInstr (Computation s,k)
:: deftheorem Def22 defines Result AMI_1:def 22 :
theorem
theorem Th54:
theorem
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 :
:: deftheorem Def27 defines programmable AMI_1:def 27 :
theorem Th58:
theorem Th59:
theorem
canceled;
theorem
canceled;
theorem Th62:
begin
theorem
canceled;
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
:: deftheorem defines Result AMI_1:def 28 :
begin
:: deftheorem Def29 defines computes AMI_1:def 29 :
theorem Th68:
theorem Th69:
theorem Th70:
:: deftheorem Def30 defines computable AMI_1:def 30 :
theorem Th71:
theorem Th72:
theorem Th73:
:: deftheorem defines Program AMI_1:def 31 :
theorem
theorem
theorem
begin
:: deftheorem Def32 defines standard-ins AMI_1:def 32 :
:: deftheorem defines InsCodes AMI_1:def 33 :
theorem
begin
:: deftheorem Def34 defines IL-FinSequence AMI_1:def 34 :
:: deftheorem defines /. AMI_1:def 35 :
:: deftheorem defines IL-Function AMI_1:def 36 :
:: deftheorem defines IL-DecoratedTree AMI_1:def 37 :
:: deftheorem defines . AMI_1:def 38 :
begin
begin
:: deftheorem defines Start-At AMI_1:def 39 :
theorem Th78:
theorem
theorem Th80:
theorem Th81:
:: deftheorem AMI_1:def 40 :
canceled;
:: deftheorem defines starts_at AMI_1:def 41 :
:: deftheorem Def42 defines halts_at AMI_1:def 42 :
:: deftheorem Def43 defines IC AMI_1:def 43 :
:: deftheorem defines starts_at AMI_1:def 44 :
:: deftheorem defines halts_at AMI_1:def 45 :
theorem
canceled;
theorem Th83:
theorem
theorem Th85:
theorem
theorem Th87:
theorem Th88:
theorem
theorem
theorem
theorem
:: deftheorem Def46 defines LifeSpan AMI_1:def 46 :
theorem
theorem Th94:
theorem
theorem
canceled;
theorem
:: deftheorem defines pi AMI_1:def 47 :
:: deftheorem defines ProgramPart AMI_1:def 48 :
:: 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
theorem Th100:
theorem Th101:
theorem
theorem
theorem Th104:
theorem Th105:
theorem
theorem
theorem
:: deftheorem defines data-only AMI_1:def 52 :
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th118:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines halt-free AMI_1:def 53 :
theorem
theorem
theorem Th134:
theorem
theorem
theorem
theorem
theorem Th139:
theorem
theorem
theorem
theorem
theorem
theorem
theorem