begin
definition
func SCMPDS -> strict AMI-Struct of
{INT } equals
AMI-Struct(#
SCM-Memory ,
(In NAT ,SCM-Memory ),
SCMPDS-Instr ,
(In [0 ,{} ,<*0 *>],SCMPDS-Instr ),
SCMPDS-OK ,
SCMPDS-Exec #);
correctness
coherence
AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),SCMPDS-Instr ,(In [0 ,{} ,<*0 *>],SCMPDS-Instr ),SCMPDS-OK ,SCMPDS-Exec #) is strict AMI-Struct of {INT };
;
end;
:: deftheorem defines SCMPDS SCMPDS_2:def 1 :
SCMPDS = AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),SCMPDS-Instr ,(In [0 ,{} ,<*0 *>],SCMPDS-Instr ),SCMPDS-OK ,SCMPDS-Exec #);
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
theorem
canceled;
theorem Th6:
begin
:: deftheorem Def2 defines Int_position SCMPDS_2:def 2 :
for b1 being Object of SCMPDS holds
( b1 is Int_position iff b1 in SCM-Data-Loc );
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem Th13:
begin
set S1 = { [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } ;
set S2 = { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;
set S3 = { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ;
set S4 = { [I2,{} ,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ;
set S5 = { [I3,{} ,<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ;
Lm1:
for I being Instruction of SCMPDS holds
( I in { [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } or I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or I in { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } or I in { [I2,{} ,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or I in { [I3,{} ,<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } )
theorem
canceled;
theorem
:: deftheorem SCMPDS_2:def 3 :
canceled;
:: deftheorem defines DataLoc SCMPDS_2:def 4 :
for m, n being Integer holds DataLoc m,n = [1,(abs (m + n))];
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
x being
set for
d4,
d5 being
Element of
SCM-Data-Loc for
k5,
k6 being
Integer st
x in {9,10,11,12,13} holds
[x,{} ,<*d4,d5,k5,k6*>] in SCMPDS-Instr
:: deftheorem defines goto SCMPDS_2:def 5 :
for k1 being Integer holds goto k1 = [0 ,{} ,<*k1*>];
:: deftheorem defines return SCMPDS_2:def 6 :
for a being Int_position holds return a = [1,{} ,<*a*>];
definition
let a be
Int_position ;
let k1 be
Integer;
func a := k1 -> Instruction of
SCMPDS equals
[2,{} ,<*a,k1*>];
correctness
coherence
[2,{} ,<*a,k1*>] is Instruction of SCMPDS ;
func saveIC a,
k1 -> Instruction of
SCMPDS equals
[3,{} ,<*a,k1*>];
correctness
coherence
[3,{} ,<*a,k1*>] is Instruction of SCMPDS ;
end;
:: deftheorem defines := SCMPDS_2:def 7 :
for a being Int_position
for k1 being Integer holds a := k1 = [2,{} ,<*a,k1*>];
:: deftheorem defines saveIC SCMPDS_2:def 8 :
for a being Int_position
for k1 being Integer holds saveIC a,k1 = [3,{} ,<*a,k1*>];
definition
let a be
Int_position ;
let k1,
k2 be
Integer;
func a,
k1 <>0_goto k2 -> Instruction of
SCMPDS equals
[4,{} ,<*a,k1,k2*>];
correctness
coherence
[4,{} ,<*a,k1,k2*>] is Instruction of SCMPDS ;
func a,
k1 <=0_goto k2 -> Instruction of
SCMPDS equals
[5,{} ,<*a,k1,k2*>];
correctness
coherence
[5,{} ,<*a,k1,k2*>] is Instruction of SCMPDS ;
func a,
k1 >=0_goto k2 -> Instruction of
SCMPDS equals
[6,{} ,<*a,k1,k2*>];
correctness
coherence
[6,{} ,<*a,k1,k2*>] is Instruction of SCMPDS ;
func a,
k1 := k2 -> Instruction of
SCMPDS equals
[7,{} ,<*a,k1,k2*>];
correctness
coherence
[7,{} ,<*a,k1,k2*>] is Instruction of SCMPDS ;
func AddTo a,
k1,
k2 -> Instruction of
SCMPDS equals
[8,{} ,<*a,k1,k2*>];
correctness
coherence
[8,{} ,<*a,k1,k2*>] is Instruction of SCMPDS ;
end;
:: deftheorem defines <>0_goto SCMPDS_2:def 9 :
for a being Int_position
for k1, k2 being Integer holds a,k1 <>0_goto k2 = [4,{} ,<*a,k1,k2*>];
:: deftheorem defines <=0_goto SCMPDS_2:def 10 :
for a being Int_position
for k1, k2 being Integer holds a,k1 <=0_goto k2 = [5,{} ,<*a,k1,k2*>];
:: deftheorem defines >=0_goto SCMPDS_2:def 11 :
for a being Int_position
for k1, k2 being Integer holds a,k1 >=0_goto k2 = [6,{} ,<*a,k1,k2*>];
:: deftheorem defines := SCMPDS_2:def 12 :
for a being Int_position
for k1, k2 being Integer holds a,k1 := k2 = [7,{} ,<*a,k1,k2*>];
:: deftheorem defines AddTo SCMPDS_2:def 13 :
for a being Int_position
for k1, k2 being Integer holds AddTo a,k1,k2 = [8,{} ,<*a,k1,k2*>];
definition
let a,
b be
Int_position ;
let k1,
k2 be
Integer;
func AddTo a,
k1,
b,
k2 -> Instruction of
SCMPDS equals
[9,{} ,<*a,b,k1,k2*>];
correctness
coherence
[9,{} ,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
func SubFrom a,
k1,
b,
k2 -> Instruction of
SCMPDS equals
[10,{} ,<*a,b,k1,k2*>];
correctness
coherence
[10,{} ,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
func MultBy a,
k1,
b,
k2 -> Instruction of
SCMPDS equals
[11,{} ,<*a,b,k1,k2*>];
correctness
coherence
[11,{} ,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
func Divide a,
k1,
b,
k2 -> Instruction of
SCMPDS equals
[12,{} ,<*a,b,k1,k2*>];
correctness
coherence
[12,{} ,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
func a,
k1 := b,
k2 -> Instruction of
SCMPDS equals
[13,{} ,<*a,b,k1,k2*>];
correctness
coherence
[13,{} ,<*a,b,k1,k2*>] is Instruction of SCMPDS ;
end;
:: deftheorem defines AddTo SCMPDS_2:def 14 :
for a, b being Int_position
for k1, k2 being Integer holds AddTo a,k1,b,k2 = [9,{} ,<*a,b,k1,k2*>];
:: deftheorem defines SubFrom SCMPDS_2:def 15 :
for a, b being Int_position
for k1, k2 being Integer holds SubFrom a,k1,b,k2 = [10,{} ,<*a,b,k1,k2*>];
:: deftheorem defines MultBy SCMPDS_2:def 16 :
for a, b being Int_position
for k1, k2 being Integer holds MultBy a,k1,b,k2 = [11,{} ,<*a,b,k1,k2*>];
:: deftheorem defines Divide SCMPDS_2:def 17 :
for a, b being Int_position
for k1, k2 being Integer holds Divide a,k1,b,k2 = [12,{} ,<*a,b,k1,k2*>];
:: deftheorem defines := SCMPDS_2:def 18 :
for a, b being Int_position
for k1, k2 being Integer holds a,k1 := b,k2 = [13,{} ,<*a,b,k1,k2*>];
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm2:
for I being Instruction of SCMPDS st I in { [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } holds
InsCode I = 0
Lm3:
for I being Instruction of SCMPDS st I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } holds
InsCode I = 1
Lm4:
for I being Instruction of SCMPDS holds
( not I in { [I1,{} ,<*d1,k1*>] where I1 is Element of Segm 14, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )
Lm5:
for I being Instruction of SCMPDS holds
( not I in { [I1,{} ,<*d1,k1,k2*>] where I1 is Element of Segm 14, d1 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {4,5,6,7,8} } or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )
Lm6:
for I being Instruction of SCMPDS holds
( not I in { [I1,{} ,<*d1,d2,k1,k2*>] where I1 is Element of Segm 14, d1, d2 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {9,10,11,12,13} } or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 )
theorem
theorem
theorem
theorem
Lm7:
for I being Instruction of SCMPDS holds
( ( not I in { [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } & not I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } & not I in { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } & not I in { [I3,{} ,<*d4,d5,k5,k6*>] where I3 is Element of Segm 14, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) or InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 )
theorem
theorem
theorem
theorem
theorem
Lm8:
for I being Instruction of SCMPDS holds
( ( not I in { [0 ,{} ,<*k1*>] where k1 is Element of INT : verum } & not I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } & not I in { [I1,{} ,<*d2,k2*>] where I1 is Element of Segm 14, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } & not I in { [I2,{} ,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ) or InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th50:
Lm9:
Data-Locations SCMPDS = SCM-Data-Loc
theorem
theorem
theorem
theorem
begin
theorem
canceled;
theorem
canceled;
theorem Th57:
theorem Th58:
theorem Th59:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
(
(Exec (a,k1 := b,k2),s) . (IC SCMPDS ) = succ (IC s) &
(Exec (a,k1 := b,k2),s) . (DataLoc (s . a),k1) = s . (DataLoc (s . b),k2) & ( for
c being
Int_position st
c <> DataLoc (s . a),
k1 holds
(Exec (a,k1 := b,k2),s) . c = s . c ) )
theorem Th60:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a being
Int_position holds
(
(Exec (AddTo a,k1,k2),s) . (IC SCMPDS ) = succ (IC s) &
(Exec (AddTo a,k1,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) + k2 & ( for
b being
Int_position st
b <> DataLoc (s . a),
k1 holds
(Exec (AddTo a,k1,k2),s) . b = s . b ) )
theorem Th61:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
(
(Exec (AddTo a,k1,b,k2),s) . (IC SCMPDS ) = succ (IC s) &
(Exec (AddTo a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) + (s . (DataLoc (s . b),k2)) & ( for
c being
Int_position st
c <> DataLoc (s . a),
k1 holds
(Exec (AddTo a,k1,b,k2),s) . c = s . c ) )
theorem Th62:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
(
(Exec (SubFrom a,k1,b,k2),s) . (IC SCMPDS ) = succ (IC s) &
(Exec (SubFrom a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) - (s . (DataLoc (s . b),k2)) & ( for
c being
Int_position st
c <> DataLoc (s . a),
k1 holds
(Exec (SubFrom a,k1,b,k2),s) . c = s . c ) )
theorem Th63:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
(
(Exec (MultBy a,k1,b,k2),s) . (IC SCMPDS ) = succ (IC s) &
(Exec (MultBy a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) * (s . (DataLoc (s . b),k2)) & ( for
c being
Int_position st
c <> DataLoc (s . a),
k1 holds
(Exec (MultBy a,k1,b,k2),s) . c = s . c ) )
theorem Th64:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
(
(Exec (Divide a,k1,b,k2),s) . (IC SCMPDS ) = succ (IC s) & (
DataLoc (s . a),
k1 <> DataLoc (s . b),
k2 implies
(Exec (Divide a,k1,b,k2),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) div (s . (DataLoc (s . b),k2)) ) &
(Exec (Divide a,k1,b,k2),s) . (DataLoc (s . b),k2) = (s . (DataLoc (s . a),k1)) mod (s . (DataLoc (s . b),k2)) & ( for
c being
Int_position st
c <> DataLoc (s . a),
k1 &
c <> DataLoc (s . b),
k2 holds
(Exec (Divide a,k1,b,k2),s) . c = s . c ) )
theorem
for
s being
State of
SCMPDS for
k1 being
Integer for
a being
Int_position holds
(
(Exec (Divide a,k1,a,k1),s) . (IC SCMPDS ) = succ (IC s) &
(Exec (Divide a,k1,a,k1),s) . (DataLoc (s . a),k1) = (s . (DataLoc (s . a),k1)) mod (s . (DataLoc (s . a),k1)) & ( for
c being
Int_position st
c <> DataLoc (s . a),
k1 holds
(Exec (Divide a,k1,a,k1),s) . c = s . c ) )
by Th64;
:: deftheorem SCMPDS_2:def 19 :
canceled;
:: deftheorem Def20 defines ICplusConst SCMPDS_2:def 20 :
for s being State of SCMPDS
for c being Integer
for b3 being Element of NAT holds
( b3 = ICplusConst s,c iff ex m being Element of NAT st
( m = IC s & b3 = abs (m + c) ) );
theorem Th66:
theorem Th67:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
( (
s . (DataLoc (s . a),k1) <> 0 implies
(Exec (a,k1 <>0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,
k2 ) & (
s . (DataLoc (s . a),k1) = 0 implies
(Exec (a,k1 <>0_goto k2),s) . (IC SCMPDS ) = succ (IC s) ) &
(Exec (a,k1 <>0_goto k2),s) . b = s . b )
theorem Th68:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
( (
s . (DataLoc (s . a),k1) <= 0 implies
(Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,
k2 ) & (
s . (DataLoc (s . a),k1) > 0 implies
(Exec (a,k1 <=0_goto k2),s) . (IC SCMPDS ) = succ (IC s) ) &
(Exec (a,k1 <=0_goto k2),s) . b = s . b )
theorem Th69:
for
s being
State of
SCMPDS for
k1,
k2 being
Integer for
a,
b being
Int_position holds
( (
s . (DataLoc (s . a),k1) >= 0 implies
(Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = ICplusConst s,
k2 ) & (
s . (DataLoc (s . a),k1) < 0 implies
(Exec (a,k1 >=0_goto k2),s) . (IC SCMPDS ) = succ (IC s) ) &
(Exec (a,k1 >=0_goto k2),s) . b = s . b )
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
for
I being
set holds
( not
I is
Instruction of
SCMPDS or ex
k1 being
Integer st
I = goto k1 or ex
a being
Int_position st
I = return a or ex
a being
Int_position ex
k1 being
Integer st
I = saveIC a,
k1 or ex
a being
Int_position ex
k1 being
Integer st
I = a := k1 or ex
a being
Int_position ex
k1,
k2 being
Integer st
I = a,
k1 := k2 or ex
a being
Int_position ex
k1,
k2 being
Integer st
I = a,
k1 <>0_goto k2 or ex
a being
Int_position ex
k1,
k2 being
Integer st
I = a,
k1 <=0_goto k2 or ex
a being
Int_position ex
k1,
k2 being
Integer st
I = a,
k1 >=0_goto k2 or ex
a,
b being
Int_position ex
k1,
k2 being
Integer st
I = AddTo a,
k1,
k2 or ex
a,
b being
Int_position ex
k1,
k2 being
Integer st
I = AddTo a,
k1,
b,
k2 or ex
a,
b being
Int_position ex
k1,
k2 being
Integer st
I = SubFrom a,
k1,
b,
k2 or ex
a,
b being
Int_position ex
k1,
k2 being
Integer st
I = MultBy a,
k1,
b,
k2 or ex
a,
b being
Int_position ex
k1,
k2 being
Integer st
I = Divide a,
k1,
b,
k2 or ex
a,
b being
Int_position ex
k1,
k2 being
Integer st
I = a,
k1 := b,
k2 )
Lm10:
for W being Instruction of SCMPDS st W is halting holds
W = goto 0
theorem Th92:
theorem
theorem
canceled;
theorem
canceled;
theorem Th96:
theorem Th97:
theorem
theorem
theorem