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 ,
(In [0 ,{} ,{} ],SCM+FSA-Instr ),
SCM+FSA-OK ,
SCM+FSA-Exec #);
coherence
AMI-Struct(# SCM+FSA-Memory ,(In NAT ,SCM+FSA-Memory ),SCM+FSA-Instr ,(In [0 ,{} ,{} ],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 :
SCM+FSA = AMI-Struct(# SCM+FSA-Memory ,(In NAT ,SCM+FSA-Memory ),SCM+FSA-Instr ,(In [0 ,{} ,{} ],SCM+FSA-Instr ),SCM+FSA-OK ,SCM+FSA-Exec #);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
begin
:: deftheorem defines Int-Locations SCMFSA_2:def 2 :
Int-Locations = SCM+FSA-Data-Loc ;
:: deftheorem defines FinSeq-Locations SCMFSA_2:def 3 :
FinSeq-Locations = SCM+FSA-Data*-Loc ;
theorem
:: deftheorem Def4 defines Int-Location SCMFSA_2:def 4 :
for b1 being Object of SCM+FSA holds
( b1 is Int-Location iff b1 in SCM+FSA-Data-Loc );
:: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def 5 :
for b1 being Object of SCM+FSA holds
( b1 is FinSeq-Location iff b1 in SCM+FSA-Data*-Loc );
theorem
theorem
theorem
theorem
theorem
theorem Th14:
theorem
:: deftheorem defines intloc SCMFSA_2:def 6 :
for k being natural number holds intloc k = dl. k;
:: deftheorem SCMFSA_2:def 7 :
canceled;
:: deftheorem defines fsloc SCMFSA_2:def 8 :
for k being natural number holds fsloc k = - (k + 1);
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 :
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = a := b iff ex A, B being Data-Location st
( a = A & b = B & b3 = A := B ) );
:: deftheorem Def12 defines AddTo SCMFSA_2:def 12 :
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = AddTo a,b iff ex A, B being Data-Location st
( a = A & b = B & b3 = AddTo A,B ) );
:: deftheorem Def13 defines SubFrom SCMFSA_2:def 13 :
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = SubFrom a,b iff ex A, B being Data-Location st
( a = A & b = B & b3 = SubFrom A,B ) );
:: deftheorem Def14 defines MultBy SCMFSA_2:def 14 :
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = MultBy a,b iff ex A, B being Data-Location st
( a = A & b = B & b3 = MultBy A,B ) );
:: deftheorem Def15 defines Divide SCMFSA_2:def 15 :
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = Divide a,b iff ex A, B being Data-Location st
( a = A & b = B & b3 = Divide A,B ) );
:: deftheorem Def16 defines goto SCMFSA_2:def 16 :
for la being Element of NAT holds goto la = SCM-goto la;
:: deftheorem Def17 defines =0_goto SCMFSA_2:def 17 :
for la being Element of NAT
for a being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = a =0_goto la iff ex A being Data-Location st
( a = A & b3 = A =0_goto la ) );
:: deftheorem Def18 defines >0_goto SCMFSA_2:def 18 :
for la being Element of NAT
for a being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = a >0_goto la iff ex A being Data-Location st
( a = A & b3 = A >0_goto la ) );
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 :
for c, i being Int-Location
for a being FinSeq-Location holds c := a,i = [9,{} ,<*c,a,i*>];
:: deftheorem defines := SCMFSA_2:def 20 :
for c, i being Int-Location
for a being FinSeq-Location holds a,i := c = [10,{} ,<*c,a,i*>];
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 :
for i being Int-Location
for a being FinSeq-Location holds i :=len a = [11,{} ,<*i,a*>];
:: deftheorem defines :=<0,...,0> SCMFSA_2:def 22 :
for i being Int-Location
for a being FinSeq-Location holds a :=<0,...,0> i = [12,{} ,<*i,a*>];
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 Th73:
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 ) = succ (IC s) & (
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 ) = succ (IC s) & 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 ) = succ (IC s) & 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
Element of
NAT st
I = goto la or ex
lb being
Element of
NAT ex
da being
Int-Location st
I = da =0_goto lb or ex
lb being
Element of
NAT 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