begin
definition
func SCM -> strict AMI-Struct of
{INT } equals
AMI-Struct(#
SCM-Memory ,
(In NAT ,SCM-Memory ),
SCM-Instr ,
SCM-OK ,
SCM-Exec #);
coherence
AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),SCM-Instr ,SCM-OK ,SCM-Exec #) is strict AMI-Struct of {INT }
;
end;
:: deftheorem defines SCM AMI_3:def 1 :
theorem
canceled;
theorem Th2:
:: deftheorem Def2 defines Data-Location AMI_3:def 2 :
definition
let a,
b be
Data-Location ;
func a := b -> Instruction of
equals
[1,<*a,b*>];
correctness
coherence
[1,<*a,b*>] is Instruction of ;
func AddTo a,
b -> Instruction of
equals
[2,<*a,b*>];
correctness
coherence
[2,<*a,b*>] is Instruction of ;
func SubFrom a,
b -> Instruction of
equals
[3,<*a,b*>];
correctness
coherence
[3,<*a,b*>] is Instruction of ;
func MultBy a,
b -> Instruction of
equals
[4,<*a,b*>];
correctness
coherence
[4,<*a,b*>] is Instruction of ;
func Divide a,
b -> Instruction of
equals
[5,<*a,b*>];
correctness
coherence
[5,<*a,b*>] is Instruction of ;
end;
:: deftheorem defines := AMI_3:def 3 :
:: deftheorem defines AddTo AMI_3:def 4 :
:: deftheorem defines SubFrom AMI_3:def 5 :
:: deftheorem defines MultBy AMI_3:def 6 :
:: deftheorem defines Divide AMI_3:def 7 :
definition
let loc be
Nat;
func goto loc -> Instruction of
equals
[6,<*loc*>];
correctness
coherence
[6,<*loc*>] is Instruction of ;
let a be
Data-Location ;
func a =0_goto loc -> Instruction of
equals
[7,<*loc,a*>];
correctness
coherence
[7,<*loc,a*>] is Instruction of ;
func a >0_goto loc -> Instruction of
equals
[8,<*loc,a*>];
correctness
coherence
[8,<*loc,a*>] is Instruction of ;
end;
:: deftheorem defines goto AMI_3:def 8 :
:: deftheorem defines =0_goto AMI_3:def 9 :
:: deftheorem defines >0_goto AMI_3:def 10 :
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 st ex s being State of st (Exec I,s) . (IC SCM ) = Next holds
not I is halting
Lm2:
for I being Instruction of 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 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 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 = 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 st W is halting holds
W = [0 ,{} ]
Lm13:
halt SCM = [0 ,{} ]
by Lm12;
begin
Lm14:
for s being State of
for i being Instruction of
for l being Instruction-Location of SCM 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 :
:: deftheorem defines il. AMI_3:def 20 :
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 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 = 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