begin
definition
func SCM -> strict AMI-Struct of
{INT } equals
AMI-Struct(#
SCM-Memory ,
(In NAT ,SCM-Memory ),
SCM-Instr ,
(In [0 ,{} ,{} ],SCM-Instr ),
SCM-OK ,
SCM-Exec #);
coherence
AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),SCM-Instr ,(In [0 ,{} ,{} ],SCM-Instr ),SCM-OK ,SCM-Exec #) is strict AMI-Struct of {INT }
;
end;
:: deftheorem defines SCM AMI_3:def 1 :
SCM = AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),SCM-Instr ,(In [0 ,{} ,{} ],SCM-Instr ),SCM-OK ,SCM-Exec #);
theorem
canceled;
theorem
canceled;
:: deftheorem Def2 defines Data-Location AMI_3:def 2 :
for b1 being Object of SCM holds
( b1 is Data-Location iff b1 in SCM-Data-Loc );
definition
let a,
b be
Data-Location ;
func a := b -> Instruction of
SCM equals
[1,{} ,<*a,b*>];
correctness
coherence
[1,{} ,<*a,b*>] is Instruction of SCM ;
func AddTo a,
b -> Instruction of
SCM equals
[2,{} ,<*a,b*>];
correctness
coherence
[2,{} ,<*a,b*>] is Instruction of SCM ;
func SubFrom a,
b -> Instruction of
SCM equals
[3,{} ,<*a,b*>];
correctness
coherence
[3,{} ,<*a,b*>] is Instruction of SCM ;
func MultBy a,
b -> Instruction of
SCM equals
[4,{} ,<*a,b*>];
correctness
coherence
[4,{} ,<*a,b*>] is Instruction of SCM ;
func Divide a,
b -> Instruction of
SCM equals
[5,{} ,<*a,b*>];
correctness
coherence
[5,{} ,<*a,b*>] is Instruction of SCM ;
end;
:: deftheorem defines := AMI_3:def 3 :
for a, b being Data-Location holds a := b = [1,{} ,<*a,b*>];
:: deftheorem defines AddTo AMI_3:def 4 :
for a, b being Data-Location holds AddTo a,b = [2,{} ,<*a,b*>];
:: deftheorem defines SubFrom AMI_3:def 5 :
for a, b being Data-Location holds SubFrom a,b = [3,{} ,<*a,b*>];
:: deftheorem defines MultBy AMI_3:def 6 :
for a, b being Data-Location holds MultBy a,b = [4,{} ,<*a,b*>];
:: deftheorem defines Divide AMI_3:def 7 :
for a, b being Data-Location holds Divide a,b = [5,{} ,<*a,b*>];
definition
let loc be
Nat;
func SCM-goto loc -> Instruction of
SCM equals
[6,<*loc*>,{} ];
correctness
coherence
[6,<*loc*>,{} ] is Instruction of SCM ;
let a be
Data-Location ;
func a =0_goto loc -> Instruction of
SCM equals
[7,<*loc*>,<*a*>];
correctness
coherence
[7,<*loc*>,<*a*>] is Instruction of SCM ;
func a >0_goto loc -> Instruction of
SCM equals
[8,<*loc*>,<*a*>];
correctness
coherence
[8,<*loc*>,<*a*>] is Instruction of SCM ;
end;
:: deftheorem defines SCM-goto AMI_3:def 8 :
for loc being Nat holds SCM-goto loc = [6,<*loc*>,{} ];
:: deftheorem defines =0_goto AMI_3:def 9 :
for loc being Nat
for a being Data-Location holds a =0_goto loc = [7,<*loc*>,<*a*>];
:: deftheorem defines >0_goto AMI_3:def 10 :
for loc being Nat
for a being Data-Location holds a >0_goto loc = [8,<*loc*>,<*a*>];
theorem
canceled;
theorem Th4:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
Lm1:
for I being Instruction of SCM st ex s being State of SCM st (Exec I,s) . (IC SCM ) = succ (IC s) holds
not I is halting
Lm2:
for I being Instruction of SCM st I = [0 ,{} ,{} ] holds
I is halting
Lm3:
for a, b being Data-Location holds not a := b is halting
Lm4:
for a, b being Data-Location holds not AddTo a,b is halting
Lm5:
for a, b being Data-Location holds not SubFrom a,b is halting
Lm6:
for a, b being Data-Location holds not MultBy a,b is halting
Lm7:
for a, b being Data-Location holds not Divide a,b is halting
Lm8:
for loc being Nat holds not SCM-goto loc is halting
Lm9:
for a being Data-Location
for loc being Nat holds not a =0_goto loc is halting
Lm10:
for a being Data-Location
for loc being Nat holds not a >0_goto loc is halting
Lm11:
for I being set holds
( I is Instruction of SCM iff ( I = [0 ,{} ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex loc being Nat st I = SCM-goto loc or ex a being Data-Location ex loc being Nat st I = a =0_goto loc or ex a being Data-Location ex loc being Nat st I = a >0_goto loc ) )
Lm12:
for W being Instruction of SCM st W is halting holds
W = [0 ,{} ,{} ]
Lm13:
halt SCM = [0 ,{} ,{} ]
by Lm12;
begin
Lm14:
for s being State of SCM
for i being Instruction of SCM
for l being Element of NAT holds (Exec i,s) . l = s . l
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
canceled;
theorem
canceled;
theorem Th51:
:: deftheorem AMI_3:def 11 :
canceled;
:: deftheorem AMI_3:def 12 :
canceled;
:: deftheorem AMI_3:def 13 :
canceled;
:: deftheorem AMI_3:def 14 :
canceled;
:: deftheorem AMI_3:def 15 :
canceled;
:: deftheorem AMI_3:def 16 :
canceled;
:: deftheorem AMI_3:def 17 :
canceled;
:: deftheorem AMI_3:def 18 :
canceled;
:: deftheorem defines dl. AMI_3:def 19 :
for k being natural number holds dl. k = [1,k];
:: deftheorem AMI_3:def 20 :
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem Th55:
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
for
I being
set holds
(
I is
Instruction of
SCM iff (
I = [0 ,{} ,{} ] or ex
a,
b being
Data-Location st
I = a := b or ex
a,
b being
Data-Location st
I = AddTo a,
b or ex
a,
b being
Data-Location st
I = SubFrom a,
b or ex
a,
b being
Data-Location st
I = MultBy a,
b or ex
a,
b being
Data-Location st
I = Divide a,
b or ex
loc being
Nat st
I = SCM-goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a =0_goto loc or ex
a being
Data-Location ex
loc being
Nat st
I = a >0_goto loc ) )
by Lm11;
theorem
theorem
theorem