begin
definition
func SCM+FSA -> strict AMI-Struct of
{INT ,(INT * )} equals
AMI-Struct(#
SCM+FSA-Memory ,
(In NAT ,SCM+FSA-Memory ),
SCM+FSA-Instr ,
SCM+FSA-OK ,
SCM+FSA-Exec #);
coherence
AMI-Struct(# SCM+FSA-Memory ,(In NAT ,SCM+FSA-Memory ),SCM+FSA-Instr ,SCM+FSA-OK ,SCM+FSA-Exec #) is strict AMI-Struct of {INT ,(INT * )}
;
end;
:: deftheorem defines SCM+FSA SCMFSA_2:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
begin
:: deftheorem defines Int-Locations SCMFSA_2:def 2 :
:: deftheorem defines FinSeq-Locations SCMFSA_2:def 3 :
theorem
:: deftheorem Def4 defines Int-Location SCMFSA_2:def 4 :
:: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def 5 :
theorem
theorem
theorem
theorem
theorem
theorem Th14:
theorem
:: deftheorem defines intloc SCMFSA_2:def 6 :
:: deftheorem defines insloc SCMFSA_2:def 7 :
:: deftheorem defines fsloc SCMFSA_2:def 8 :
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th20:
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem Th35:
theorem
canceled;
theorem
theorem Th38:
definition
let a,
b be
Int-Location ;
canceled;canceled;func a := b -> Instruction of
SCM+FSA means :
Def11:
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = A := B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = A := B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = A := B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = A := B ) holds
b1 = b2;
;
func AddTo a,
b -> Instruction of
SCM+FSA means :
Def12:
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = AddTo A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = AddTo A,B ) holds
b1 = b2;
;
func SubFrom a,
b -> Instruction of
SCM+FSA means :
Def13:
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = SubFrom A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = SubFrom A,B ) holds
b1 = b2;
;
func MultBy a,
b -> Instruction of
SCM+FSA means :
Def14:
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = MultBy A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = MultBy A,B ) holds
b1 = b2;
;
func Divide a,
b -> Instruction of
SCM+FSA means :
Def15:
ex
A,
B being
Data-Location st
(
a = A &
b = B &
it = Divide A,
B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = Divide A,B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = Divide A,B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = Divide A,B ) holds
b1 = b2;
;
end;
:: deftheorem SCMFSA_2:def 9 :
canceled;
:: deftheorem SCMFSA_2:def 10 :
canceled;
:: deftheorem Def11 defines := SCMFSA_2:def 11 :
:: deftheorem Def12 defines AddTo SCMFSA_2:def 12 :
:: deftheorem Def13 defines SubFrom SCMFSA_2:def 13 :
:: deftheorem Def14 defines MultBy SCMFSA_2:def 14 :
:: deftheorem Def15 defines Divide SCMFSA_2:def 15 :
:: deftheorem Def16 defines goto SCMFSA_2:def 16 :
:: deftheorem Def17 defines =0_goto SCMFSA_2:def 17 :
:: deftheorem Def18 defines >0_goto SCMFSA_2:def 18 :
definition
let c,
i be
Int-Location ;
let a be
FinSeq-Location ;
func c := a,
i -> Instruction of
SCM+FSA equals
[9,<*c,a,i*>];
coherence
[9,<*c,a,i*>] is Instruction of SCM+FSA
func a,
i := c -> Instruction of
SCM+FSA equals
[10,<*c,a,i*>];
coherence
[10,<*c,a,i*>] is Instruction of SCM+FSA
end;
:: deftheorem defines := SCMFSA_2:def 19 :
:: deftheorem defines := SCMFSA_2:def 20 :
definition
let i be
Int-Location ;
let a be
FinSeq-Location ;
func i :=len a -> Instruction of
SCM+FSA equals
[11,<*i,a*>];
coherence
[11,<*i,a*>] is Instruction of SCM+FSA
func a :=<0,...,0> i -> Instruction of
SCM+FSA equals
[12,<*i,a*>];
coherence
[12,<*i,a*>] is Instruction of SCM+FSA
end;
:: deftheorem defines :=len SCMFSA_2:def 21 :
:: deftheorem defines :=<0,...,0> SCMFSA_2:def 22 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
begin
theorem
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem
theorem
theorem
theorem
theorem Th75:
theorem Th76:
theorem
canceled;
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem Th88:
begin
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
for
a,
b being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (Divide a,b),s) . (IC SCM+FSA ) = Next & (
a <> b implies
(Exec (Divide a,b),s) . a = (s . a) div (s . b) ) &
(Exec (Divide a,b),s) . b = (s . a) mod (s . b) & ( for
c being
Int-Location st
c <> a &
c <> b holds
(Exec (Divide a,b),s) . c = s . c ) & ( for
f being
FinSeq-Location holds
(Exec (Divide a,b),s) . f = s . f ) )
theorem
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
theorem Th99:
for
g being
FinSeq-Location for
a,
c being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (g,a := c),s) . (IC SCM+FSA ) = Next & ex
k being
Element of
NAT st
(
k = abs (s . a) &
(Exec (g,a := c),s) . g = (s . g) +* k,
(s . c) ) & ( for
b being
Int-Location holds
(Exec (g,a := c),s) . b = s . b ) & ( for
f being
FinSeq-Location st
f <> g holds
(Exec (g,a := c),s) . f = s . f ) )
theorem Th100:
theorem Th101:
for
g being
FinSeq-Location for
c being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next & ex
k being
Element of
NAT st
(
k = abs (s . c) &
(Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for
b being
Int-Location holds
(Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for
f being
FinSeq-Location st
f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )
begin
theorem
theorem Th103:
theorem Th104:
theorem Th105:
theorem Th106:
theorem Th107:
theorem Th108:
theorem Th109:
theorem Th110:
theorem Th111:
theorem Th112:
theorem Th113:
theorem Th114:
theorem Th115:
theorem Th116:
theorem
canceled;
theorem
theorem Th119:
theorem Th120:
for
I being
set holds
(
I is
Instruction of
SCM+FSA iff (
I = [0 ,{} ] or ex
a,
b being
Int-Location st
I = a := b or ex
a,
b being
Int-Location st
I = AddTo a,
b or ex
a,
b being
Int-Location st
I = SubFrom a,
b or ex
a,
b being
Int-Location st
I = MultBy a,
b or ex
a,
b being
Int-Location st
I = Divide a,
b or ex
la being
Instruction-Location of
SCM+FSA st
I = goto la or ex
lb being
Instruction-Location of
SCM+FSA ex
da being
Int-Location st
I = da =0_goto lb or ex
lb being
Instruction-Location of
SCM+FSA ex
da being
Int-Location st
I = da >0_goto lb or ex
b,
a being
Int-Location ex
fa being
FinSeq-Location st
I = a := fa,
b or ex
a,
b being
Int-Location ex
fa being
FinSeq-Location st
I = fa,
a := b or ex
a being
Int-Location ex
f being
FinSeq-Location st
I = a :=len f or ex
a being
Int-Location ex
f being
FinSeq-Location st
I = f :=<0,...,0> a ) )
Lm1:
for W being Instruction of SCM+FSA st W is halting holds
W = [0 ,{} ]
theorem Th121:
theorem Th122:
theorem Th123:
theorem
theorem
theorem
theorem