:: SCMPDS_2 semantic presentation
begin
definition
func SCMPDS -> strict AMI-Struct over 2 equals :: SCMPDS_2:def 1
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);
correctness
coherence
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #) is strict AMI-Struct over 2;
;
end;
:: deftheorem defines SCMPDS SCMPDS_2:def_1_:_
SCMPDS = AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCMPDS-Instr,SCM-OK,SCM-VAL,SCMPDS-Exec #);
registration
cluster SCMPDS -> non empty strict ;
coherence
not SCMPDS is empty by STRUCT_0:def_1;
end;
registration
cluster SCMPDS -> with_non-empty_values IC-Ins-separated strict ;
coherence
( SCMPDS is with_non-empty_values & SCMPDS is IC-Ins-separated )
proof
thus the_Values_of SCMPDS is non-empty ; :: according to MEMSTR_0:def_3 ::_thesis: SCMPDS is IC-Ins-separated
IC = NAT by AMI_2:22, FUNCT_7:def_1;
then Values (IC ) = NAT by AMI_2:6;
hence SCMPDS is IC-Ins-separated by MEMSTR_0:def_6; ::_thesis: verum
end;
end;
theorem :: SCMPDS_2:1
canceled;
theorem Th2: :: SCMPDS_2:2
IC = NAT by AMI_2:22, FUNCT_7:def_1;
begin
registration
cluster Int-like for Element of the carrier of SCMPDS;
existence
ex b1 being Object of SCMPDS st b1 is Int-like
proof
reconsider x = the Element of SCM-Data-Loc as Object of SCMPDS ;
take x ; ::_thesis: x is Int-like
thus x is Int-like by AMI_2:def_16; ::_thesis: verum
end;
end;
definition
mode Int_position is Int-like Object of SCMPDS;
canceled;
end;
:: deftheorem SCMPDS_2:def_2_:_
canceled;
theorem :: SCMPDS_2:3
canceled;
theorem :: SCMPDS_2:4
canceled;
theorem Th5: :: SCMPDS_2:5
for l being Int_position holds Values l = INT
proof
let l be Int_position; ::_thesis: Values l = INT
l in SCM-Data-Loc by AMI_2:def_16;
hence Values l = INT by AMI_2:8; ::_thesis: verum
end;
begin
set S1 = { [14,{},<*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 15, 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 15, 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 15, 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,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } )
proof
let I be Instruction of SCMPDS; ::_thesis: ( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } )
( I in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
then ( I in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
then ( I in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } or I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
then ( I in {[0,{},{}]} \/ { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by XBOOLE_0:def_3;
hence ( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: SCMPDS_2:6
for I being Instruction of SCMPDS holds InsCode I <= 14
proof
let I be Instruction of SCMPDS; ::_thesis: InsCode I <= 14
( 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 or InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 or InsCode I = 14 ) by SCMPDS_I:8;
hence InsCode I <= 14 ; ::_thesis: verum
end;
registration
let s be State of SCMPDS;
let d be Int_position;
clusters . d -> integer ;
coherence
s . d is integer
proof
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider S = s as SCM-State by CARD_3:107;
S . D = s . d ;
hence s . d is integer ; ::_thesis: verum
end;
end;
definition
let m, n be Integer;
func DataLoc (m,n) -> Int_position equals :: SCMPDS_2:def 3
[1,(abs (m + n))];
coherence
[1,(abs (m + n))] is Int_position
proof
[1,(abs (m + n))] in SCM-Data-Loc by AMI_2:24;
hence [1,(abs (m + n))] is Int_position by AMI_2:def_16; ::_thesis: verum
end;
end;
:: deftheorem defines DataLoc SCMPDS_2:def_3_:_
for m, n being Integer holds DataLoc (m,n) = [1,(abs (m + n))];
theorem Th7: :: SCMPDS_2:7
for k1 being Integer holds [14,{},<*k1*>] in SCMPDS-Instr
proof
let k1 be Integer; ::_thesis: [14,{},<*k1*>] in SCMPDS-Instr
k1 is Element of INT by INT_1:def_2;
then [14,{},<*k1*>] in { [14,{},<*k1*>] where k1 is Element of INT : verum } ;
then [14,{},<*k1*>] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def_3;
then [14,{},<*k1*>] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
then [14,{},<*k1*>] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } by XBOOLE_0:def_3;
then [14,{},<*k1*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by XBOOLE_0:def_3;
hence [14,{},<*k1*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th8: :: SCMPDS_2:8
for d1 being Element of SCM-Data-Loc holds [1,{},<*d1*>] in SCMPDS-Instr
proof
let d1 be Element of SCM-Data-Loc ; ::_thesis: [1,{},<*d1*>] in SCMPDS-Instr
[1,{},<*d1*>] in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ;
then [1,{},<*d1*>] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3;
then [1,{},<*d1*>] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } by XBOOLE_0:def_3;
then [1,{},<*d1*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by XBOOLE_0:def_3;
hence [1,{},<*d1*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th9: :: SCMPDS_2:9
for x being set
for d2 being Element of SCM-Data-Loc
for k2 being Integer st x in {2,3} holds
[x,{},<*d2,k2*>] in SCMPDS-Instr
proof
let x be set ; ::_thesis: for d2 being Element of SCM-Data-Loc
for k2 being Integer st x in {2,3} holds
[x,{},<*d2,k2*>] in SCMPDS-Instr
let d2 be Element of SCM-Data-Loc ; ::_thesis: for k2 being Integer st x in {2,3} holds
[x,{},<*d2,k2*>] in SCMPDS-Instr
let k2 be Integer; ::_thesis: ( x in {2,3} implies [x,{},<*d2,k2*>] in SCMPDS-Instr )
assume A1: x in {2,3} ; ::_thesis: [x,{},<*d2,k2*>] in SCMPDS-Instr
then ( x = 2 or x = 3 ) by TARSKI:def_2;
then reconsider x = x as Element of Segm 15 by NAT_1:44;
k2 is Element of INT by INT_1:def_2;
then [x,{},<*d2,k2*>] in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } by A1;
then [x,{},<*d2,k2*>] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } by XBOOLE_0:def_3;
then [x,{},<*d2,k2*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by XBOOLE_0:def_3;
hence [x,{},<*d2,k2*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th10: :: SCMPDS_2:10
for x being set
for d2 being Element of SCM-Data-Loc
for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,{},<*d2,k3,k4*>] in SCMPDS-Instr
proof
let x be set ; ::_thesis: for d2 being Element of SCM-Data-Loc
for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,{},<*d2,k3,k4*>] in SCMPDS-Instr
let d2 be Element of SCM-Data-Loc ; ::_thesis: for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,{},<*d2,k3,k4*>] in SCMPDS-Instr
let k3, k4 be Integer; ::_thesis: ( x in {4,5,6,7,8} implies [x,{},<*d2,k3,k4*>] in SCMPDS-Instr )
assume A1: x in {4,5,6,7,8} ; ::_thesis: [x,{},<*d2,k3,k4*>] in SCMPDS-Instr
then ( x = 4 or x = 5 or x = 6 or x = 7 or x = 8 ) by ENUMSET1:def_3;
then reconsider x = x as Element of Segm 15 by NAT_1:44;
( k3 is Element of INT & k4 is Element of INT ) by INT_1:def_2;
then [x,{},<*d2,k3,k4*>] in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by A1;
then [x,{},<*d2,k3,k4*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ) \/ { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } by XBOOLE_0:def_3;
hence [x,{},<*d2,k3,k4*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th11: :: SCMPDS_2:11
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
proof
let x be set ; ::_thesis: 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
let d4, d5 be Element of SCM-Data-Loc ; ::_thesis: for k5, k6 being Integer st x in {9,10,11,12,13} holds
[x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr
let k5, k6 be Integer; ::_thesis: ( x in {9,10,11,12,13} implies [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr )
assume A1: x in {9,10,11,12,13} ; ::_thesis: [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr
then ( x = 9 or x = 10 or x = 11 or x = 12 or x = 13 ) by ENUMSET1:def_3;
then reconsider x = x as Element of Segm 15 by NAT_1:44;
( k5 is Element of INT & k6 is Element of INT ) by INT_1:def_2;
then [x,{},<*d4,d5,k5,k6*>] in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } by A1;
hence [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let k1 be Integer;
func goto k1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 4
[14,{},<*k1*>];
correctness
coherence
[14,{},<*k1*>] is Instruction of SCMPDS;
by Th7;
end;
:: deftheorem defines goto SCMPDS_2:def_4_:_
for k1 being Integer holds goto k1 = [14,{},<*k1*>];
definition
let a be Int_position;
func return a -> Instruction of SCMPDS equals :: SCMPDS_2:def 5
[1,{},<*a*>];
correctness
coherence
[1,{},<*a*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
[1,{},<*v*>] in SCMPDS-Instr by Th8;
hence [1,{},<*a*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
end;
:: deftheorem defines return SCMPDS_2:def_5_:_
for a being Int_position holds return a = [1,{},<*a*>];
definition
let a be Int_position;
let k1 be Integer;
funca := k1 -> Instruction of SCMPDS equals :: SCMPDS_2:def 6
[2,{},<*a,k1*>];
correctness
coherence
[2,{},<*a,k1*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
2 in {2,3} by TARSKI:def_2;
then [2,{},<*v,k1*>] in SCMPDS-Instr by Th9;
hence [2,{},<*a,k1*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func saveIC (a,k1) -> Instruction of SCMPDS equals :: SCMPDS_2:def 7
[3,{},<*a,k1*>];
correctness
coherence
[3,{},<*a,k1*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
3 in {2,3} by TARSKI:def_2;
then [3,{},<*v,k1*>] in SCMPDS-Instr by Th9;
hence [3,{},<*a,k1*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
end;
:: deftheorem defines := SCMPDS_2:def_6_:_
for a being Int_position
for k1 being Integer holds a := k1 = [2,{},<*a,k1*>];
:: deftheorem defines saveIC SCMPDS_2:def_7_:_
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 :: SCMPDS_2:def 8
[4,{},<*a,k1,k2*>];
correctness
coherence
[4,{},<*a,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
4 in {4,5,6,7,8} by ENUMSET1:def_3;
then [4,{},<*v,k1,k2*>] in SCMPDS-Instr by Th10;
hence [4,{},<*a,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func(a,k1) <=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 9
[5,{},<*a,k1,k2*>];
correctness
coherence
[5,{},<*a,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
5 in {4,5,6,7,8} by ENUMSET1:def_3;
then [5,{},<*v,k1,k2*>] in SCMPDS-Instr by Th10;
hence [5,{},<*a,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func(a,k1) >=0_goto k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 10
[6,{},<*a,k1,k2*>];
correctness
coherence
[6,{},<*a,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
6 in {4,5,6,7,8} by ENUMSET1:def_3;
then [6,{},<*v,k1,k2*>] in SCMPDS-Instr by Th10;
hence [6,{},<*a,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func(a,k1) := k2 -> Instruction of SCMPDS equals :: SCMPDS_2:def 11
[7,{},<*a,k1,k2*>];
correctness
coherence
[7,{},<*a,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
7 in {4,5,6,7,8} by ENUMSET1:def_3;
then [7,{},<*v,k1,k2*>] in SCMPDS-Instr by Th10;
hence [7,{},<*a,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func AddTo (a,k1,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 12
[8,{},<*a,k1,k2*>];
correctness
coherence
[8,{},<*a,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v = a as Element of SCM-Data-Loc by AMI_2:def_16;
8 in {4,5,6,7,8} by ENUMSET1:def_3;
then [8,{},<*v,k1,k2*>] in SCMPDS-Instr by Th10;
hence [8,{},<*a,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
end;
:: deftheorem defines <>0_goto SCMPDS_2:def_8_:_
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_9_:_
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_10_:_
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_11_:_
for a being Int_position
for k1, k2 being Integer holds (a,k1) := k2 = [7,{},<*a,k1,k2*>];
:: deftheorem defines AddTo SCMPDS_2:def_12_:_
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 :: SCMPDS_2:def 13
[9,{},<*a,b,k1,k2*>];
correctness
coherence
[9,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def_16;
9 in {9,10,11,12,13} by ENUMSET1:def_3;
then [9,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th11;
hence [9,{},<*a,b,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func SubFrom (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 14
[10,{},<*a,b,k1,k2*>];
correctness
coherence
[10,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def_16;
10 in {9,10,11,12,13} by ENUMSET1:def_3;
then [10,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th11;
hence [10,{},<*a,b,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func MultBy (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 15
[11,{},<*a,b,k1,k2*>];
correctness
coherence
[11,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def_16;
11 in {9,10,11,12,13} by ENUMSET1:def_3;
then [11,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th11;
hence [11,{},<*a,b,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func Divide (a,k1,b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 16
[12,{},<*a,b,k1,k2*>];
correctness
coherence
[12,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def_16;
12 in {9,10,11,12,13} by ENUMSET1:def_3;
then [12,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th11;
hence [12,{},<*a,b,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
func(a,k1) := (b,k2) -> Instruction of SCMPDS equals :: SCMPDS_2:def 17
[13,{},<*a,b,k1,k2*>];
correctness
coherence
[13,{},<*a,b,k1,k2*>] is Instruction of SCMPDS;
proof
reconsider v1 = a, v2 = b as Element of SCM-Data-Loc by AMI_2:def_16;
13 in {9,10,11,12,13} by ENUMSET1:def_3;
then [13,{},<*v1,v2,k1,k2*>] in SCMPDS-Instr by Th11;
hence [13,{},<*a,b,k1,k2*>] is Instruction of SCMPDS ; ::_thesis: verum
end;
end;
:: deftheorem defines AddTo SCMPDS_2:def_13_:_
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_14_:_
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_15_:_
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_16_:_
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_17_:_
for a, b being Int_position
for k1, k2 being Integer holds (a,k1) := (b,k2) = [13,{},<*a,b,k1,k2*>];
theorem :: SCMPDS_2:12
for k1 being Integer holds InsCode (goto k1) = 14 by RECDEF_2:def_1;
theorem :: SCMPDS_2:13
for a being Int_position holds InsCode (return a) = 1 by RECDEF_2:def_1;
theorem :: SCMPDS_2:14
for k1 being Integer
for a being Int_position holds InsCode (a := k1) = 2 by RECDEF_2:def_1;
theorem :: SCMPDS_2:15
for k1 being Integer
for a being Int_position holds InsCode (saveIC (a,k1)) = 3 by RECDEF_2:def_1;
theorem :: SCMPDS_2:16
for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) <>0_goto k2) = 4 by RECDEF_2:def_1;
theorem :: SCMPDS_2:17
for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) <=0_goto k2) = 5 by RECDEF_2:def_1;
theorem :: SCMPDS_2:18
for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) >=0_goto k2) = 6 by RECDEF_2:def_1;
theorem :: SCMPDS_2:19
for k1, k2 being Integer
for a being Int_position holds InsCode ((a,k1) := k2) = 7 by RECDEF_2:def_1;
theorem :: SCMPDS_2:20
for k1, k2 being Integer
for a being Int_position holds InsCode (AddTo (a,k1,k2)) = 8 by RECDEF_2:def_1;
theorem :: SCMPDS_2:21
for k1, k2 being Integer
for a, b being Int_position holds InsCode (AddTo (a,k1,b,k2)) = 9 by RECDEF_2:def_1;
theorem :: SCMPDS_2:22
for k1, k2 being Integer
for a, b being Int_position holds InsCode (SubFrom (a,k1,b,k2)) = 10 by RECDEF_2:def_1;
theorem :: SCMPDS_2:23
for k1, k2 being Integer
for a, b being Int_position holds InsCode (MultBy (a,k1,b,k2)) = 11 by RECDEF_2:def_1;
theorem :: SCMPDS_2:24
for k1, k2 being Integer
for a, b being Int_position holds InsCode (Divide (a,k1,b,k2)) = 12 by RECDEF_2:def_1;
theorem :: SCMPDS_2:25
for k1, k2 being Integer
for a, b being Int_position holds InsCode ((a,k1) := (b,k2)) = 13 by RECDEF_2:def_1;
Lm2: for I being Instruction of SCMPDS st I in { [14,{},<*k1*>] where k1 is Element of INT : verum } holds
InsCode I = 14
proof
let I be Instruction of SCMPDS; ::_thesis: ( I in { [14,{},<*k1*>] where k1 is Element of INT : verum } implies InsCode I = 14 )
assume I in { [14,{},<*k1*>] where k1 is Element of INT : verum } ; ::_thesis: InsCode I = 14
then ex k1 being Element of INT st I = [14,{},<*k1*>] ;
hence InsCode I = 14 by RECDEF_2:def_1; ::_thesis: verum
end;
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
proof
let I be Instruction of SCMPDS; ::_thesis: ( I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } implies InsCode I = 1 )
assume I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; ::_thesis: InsCode I = 1
then ex d1 being Element of SCM-Data-Loc st I = [1,{},<*d1*>] ;
hence InsCode I = 1 by RECDEF_2:def_1; ::_thesis: verum
end;
Lm4: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )
proof
let I be Instruction of SCMPDS; ::_thesis: ( not I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } or InsCode I = 2 or InsCode I = 3 )
assume I in { [I1,{},<*d1,k1*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1 is Element of INT : I1 in {2,3} } ; ::_thesis: ( InsCode I = 2 or InsCode I = 3 )
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1 being Element of INT such that
A1: I = [I1,{},<*d1,k1*>] and
A2: I1 in {2,3} ;
( I1 = 2 or I1 = 3 ) by A2, TARSKI:def_2;
hence ( InsCode I = 2 or InsCode I = 3 ) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
Lm5: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, 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 )
proof
let I be Instruction of SCMPDS; ::_thesis: ( not I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, 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 )
assume I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {4,5,6,7,8} } ; ::_thesis: ( InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A1: I = [I1,{},<*d1,k1,k2*>] and
A2: I1 in {4,5,6,7,8} ;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A2, ENUMSET1:def_3;
hence ( InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 ) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
Lm6: for I being Instruction of SCMPDS holds
( not I in { [I1,{},<*d1,d2,k1,k2*>] where I1 is Element of Segm 15, 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 )
proof
let I be Instruction of SCMPDS; ::_thesis: ( not I in { [I1,{},<*d1,d2,k1,k2*>] where I1 is Element of Segm 15, 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 )
assume I in { [I1,{},<*d1,d2,k1,k2*>] where I1 is Element of Segm 15, d1, d2 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {9,10,11,12,13} } ; ::_thesis: ( InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 )
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A1: I = [I1,{},<*d1,d2,k1,k2*>] and
A2: I1 in {9,10,11,12,13} ;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A2, ENUMSET1:def_3;
hence ( InsCode I = 9 or InsCode I = 10 or InsCode I = 11 or InsCode I = 12 or InsCode I = 13 ) by A1, RECDEF_2:def_1; ::_thesis: verum
end;
Lm7: for I being Instruction of SCMPDS st I in {[0,{},{}]} holds
InsCode I = 0
proof
let I be Instruction of SCMPDS; ::_thesis: ( I in {[0,{},{}]} implies InsCode I = 0 )
assume I in {[0,{},{}]} ; ::_thesis: InsCode I = 0
then I = [0,{},{}] by TARSKI:def_1;
hence InsCode I = 0 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMPDS_2:26
for ins being Instruction of SCMPDS st InsCode ins = 14 holds
ex k1 being Integer st ins = goto k1
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 14 implies ex k1 being Integer st I = goto k1 )
assume A1: InsCode I = 14 ; ::_thesis: ex k1 being Integer st I = goto k1
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider k1 being Element of INT such that
A2: I = [14,{},<*k1*>] by A1, Lm3, Lm4, Lm5, Lm6, Lm7;
take k1 ; ::_thesis: I = goto k1
thus I = goto k1 by A2; ::_thesis: verum
end;
theorem :: SCMPDS_2:27
for ins being Instruction of SCMPDS st InsCode ins = 1 holds
ex a being Int_position st ins = return a
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 1 implies ex a being Int_position st I = return a )
assume A1: InsCode I = 1 ; ::_thesis: ex a being Int_position st I = return a
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider d1 being Element of SCM-Data-Loc such that
A2: I = [1,{},<*d1*>] by A1, Lm2, Lm4, Lm5, Lm6, Lm7;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: I = return a
thus I = return a by A2; ::_thesis: verum
end;
theorem :: SCMPDS_2:28
for ins being Instruction of SCMPDS st InsCode ins = 2 holds
ex a being Int_position ex k1 being Integer st ins = a := k1
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 2 implies ex a being Int_position ex k1 being Integer st I = a := k1 )
assume A1: InsCode I = 2 ; ::_thesis: ex a being Int_position ex k1 being Integer st I = a := k1
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1 being Element of INT such that
A2: I = [I1,{},<*d1,k1*>] and
A3: I1 in {2,3} by A1, Lm2, Lm3, Lm5, Lm6, Lm7;
( I1 = 2 or I1 = 3 ) by A3, TARSKI:def_2;
then consider d1 being Element of SCM-Data-Loc , k1 being Integer such that
A4: I = [2,{},<*d1,k1*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1 being Integer st I = a := k1
take k1 ; ::_thesis: I = a := k1
thus I = a := k1 by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:29
for ins being Instruction of SCMPDS st InsCode ins = 3 holds
ex a being Int_position ex k1 being Integer st ins = saveIC (a,k1)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 3 implies ex a being Int_position ex k1 being Integer st I = saveIC (a,k1) )
assume A1: InsCode I = 3 ; ::_thesis: ex a being Int_position ex k1 being Integer st I = saveIC (a,k1)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1 being Element of INT such that
A2: I = [I1,{},<*d1,k1*>] and
A3: I1 in {2,3} by A1, Lm2, Lm3, Lm5, Lm6, Lm7;
( I1 = 2 or I1 = 3 ) by A3, TARSKI:def_2;
then consider d1 being Element of SCM-Data-Loc , k1 being Integer such that
A4: I = [3,{},<*d1,k1*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1 being Integer st I = saveIC (a,k1)
take k1 ; ::_thesis: I = saveIC (a,k1)
thus I = saveIC (a,k1) by A4; ::_thesis: verum
end;
Lm8: for I being Instruction of SCMPDS holds
( ( not I in {[0,{},{}]} & not I in { [14,{},<*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 15, 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 15, 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 = 14 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 )
by Lm2, Lm3, Lm4, Lm6, Lm7;
theorem :: SCMPDS_2:30
for ins being Instruction of SCMPDS st InsCode ins = 4 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) <>0_goto k2
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 4 implies ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <>0_goto k2 )
assume A1: InsCode I = 4 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <>0_goto k2
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,k1,k2*>] and
A3: I1 in {4,5,6,7,8} by A1, Lm8;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A3, ENUMSET1:def_3;
then consider d1 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [4,{},<*d1,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1, k2 being Integer st I = (a,k1) <>0_goto k2
take k1 ; ::_thesis: ex k2 being Integer st I = (a,k1) <>0_goto k2
take k2 ; ::_thesis: I = (a,k1) <>0_goto k2
thus I = (a,k1) <>0_goto k2 by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:31
for ins being Instruction of SCMPDS st InsCode ins = 5 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) <=0_goto k2
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 5 implies ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <=0_goto k2 )
assume A1: InsCode I = 5 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st I = (a,k1) <=0_goto k2
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,k1,k2*>] and
A3: I1 in {4,5,6,7,8} by A1, Lm8;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A3, ENUMSET1:def_3;
then consider d1 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [5,{},<*d1,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1, k2 being Integer st I = (a,k1) <=0_goto k2
take k1 ; ::_thesis: ex k2 being Integer st I = (a,k1) <=0_goto k2
take k2 ; ::_thesis: I = (a,k1) <=0_goto k2
thus I = (a,k1) <=0_goto k2 by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:32
for ins being Instruction of SCMPDS st InsCode ins = 6 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) >=0_goto k2
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 6 implies ex a being Int_position ex k1, k2 being Integer st I = (a,k1) >=0_goto k2 )
assume A1: InsCode I = 6 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st I = (a,k1) >=0_goto k2
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,k1,k2*>] and
A3: I1 in {4,5,6,7,8} by A1, Lm8;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A3, ENUMSET1:def_3;
then consider d1 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [6,{},<*d1,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1, k2 being Integer st I = (a,k1) >=0_goto k2
take k1 ; ::_thesis: ex k2 being Integer st I = (a,k1) >=0_goto k2
take k2 ; ::_thesis: I = (a,k1) >=0_goto k2
thus I = (a,k1) >=0_goto k2 by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:33
for ins being Instruction of SCMPDS st InsCode ins = 7 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) := k2
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 7 implies ex a being Int_position ex k1, k2 being Integer st I = (a,k1) := k2 )
assume A1: InsCode I = 7 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st I = (a,k1) := k2
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,k1,k2*>] and
A3: I1 in {4,5,6,7,8} by A1, Lm8;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A3, ENUMSET1:def_3;
then consider d1 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [7,{},<*d1,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1, k2 being Integer st I = (a,k1) := k2
take k1 ; ::_thesis: ex k2 being Integer st I = (a,k1) := k2
take k2 ; ::_thesis: I = (a,k1) := k2
thus I = (a,k1) := k2 by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:34
for ins being Instruction of SCMPDS st InsCode ins = 8 holds
ex a being Int_position ex k1, k2 being Integer st ins = AddTo (a,k1,k2)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 8 implies ex a being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,k2) )
assume A1: InsCode I = 8 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,k2)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,k1,k2*>] and
A3: I1 in {4,5,6,7,8} by A1, Lm8;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A3, ENUMSET1:def_3;
then consider d1 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [8,{},<*d1,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex k1, k2 being Integer st I = AddTo (a,k1,k2)
take k1 ; ::_thesis: ex k2 being Integer st I = AddTo (a,k1,k2)
take k2 ; ::_thesis: I = AddTo (a,k1,k2)
thus I = AddTo (a,k1,k2) by A4; ::_thesis: verum
end;
Lm9: for I being Instruction of SCMPDS holds
( ( not I in {[0,{},{}]} & not I in { [14,{},<*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 15, 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 15, 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 = 14 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 )
proof
let I be Instruction of SCMPDS; ::_thesis: ( ( not I in {[0,{},{}]} & not I in { [14,{},<*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 15, 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 15, 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 = 14 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 )
assume A1: ( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ) ; ::_thesis: ( InsCode I = 0 or InsCode I = 14 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 )
percases ( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ) by A1;
suppose I in {[0,{},{}]} ; ::_thesis: ( InsCode I = 0 or InsCode I = 14 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 )
hence ( InsCode I = 0 or InsCode I = 14 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 ) by Lm7; ::_thesis: verum
end;
suppose I in { [14,{},<*k1*>] where k1 is Element of INT : verum } ; ::_thesis: ( InsCode I = 0 or InsCode I = 14 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 )
hence ( InsCode I = 0 or InsCode I = 14 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 ) by Lm2; ::_thesis: verum
end;
suppose I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; ::_thesis: ( InsCode I = 0 or InsCode I = 14 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 )
hence ( InsCode I = 0 or InsCode I = 14 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 ) by Lm3; ::_thesis: verum
end;
suppose I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ; ::_thesis: ( InsCode I = 0 or InsCode I = 14 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 )
hence ( InsCode I = 0 or InsCode I = 14 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 ) by Lm4; ::_thesis: verum
end;
suppose I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ; ::_thesis: ( InsCode I = 0 or InsCode I = 14 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 )
hence ( InsCode I = 0 or InsCode I = 14 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 ) by Lm5; ::_thesis: verum
end;
end;
end;
theorem :: SCMPDS_2:35
for ins being Instruction of SCMPDS st InsCode ins = 9 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = AddTo (a,k1,b,k2)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 9 implies ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2) )
assume A1: InsCode I = 9 ; ::_thesis: ex a, b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,d2,k1,k2*>] and
A3: I1 in {9,10,11,12,13} by A1, Lm9;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A3, ENUMSET1:def_3;
then consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [9,{},<*d1,d2,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1, b = d2 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex b being Int_position ex k1, k2 being Integer st I = AddTo (a,k1,b,k2)
take b ; ::_thesis: ex k1, k2 being Integer st I = AddTo (a,k1,b,k2)
take k1 ; ::_thesis: ex k2 being Integer st I = AddTo (a,k1,b,k2)
take k2 ; ::_thesis: I = AddTo (a,k1,b,k2)
thus I = AddTo (a,k1,b,k2) by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:36
for ins being Instruction of SCMPDS st InsCode ins = 10 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = SubFrom (a,k1,b,k2)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 10 implies ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom (a,k1,b,k2) )
assume A1: InsCode I = 10 ; ::_thesis: ex a, b being Int_position ex k1, k2 being Integer st I = SubFrom (a,k1,b,k2)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,d2,k1,k2*>] and
A3: I1 in {9,10,11,12,13} by A1, Lm9;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A3, ENUMSET1:def_3;
then consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [10,{},<*d1,d2,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1, b = d2 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex b being Int_position ex k1, k2 being Integer st I = SubFrom (a,k1,b,k2)
take b ; ::_thesis: ex k1, k2 being Integer st I = SubFrom (a,k1,b,k2)
take k1 ; ::_thesis: ex k2 being Integer st I = SubFrom (a,k1,b,k2)
take k2 ; ::_thesis: I = SubFrom (a,k1,b,k2)
thus I = SubFrom (a,k1,b,k2) by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:37
for ins being Instruction of SCMPDS st InsCode ins = 11 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = MultBy (a,k1,b,k2)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 11 implies ex a, b being Int_position ex k1, k2 being Integer st I = MultBy (a,k1,b,k2) )
assume A1: InsCode I = 11 ; ::_thesis: ex a, b being Int_position ex k1, k2 being Integer st I = MultBy (a,k1,b,k2)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,d2,k1,k2*>] and
A3: I1 in {9,10,11,12,13} by A1, Lm9;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A3, ENUMSET1:def_3;
then consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [11,{},<*d1,d2,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1, b = d2 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex b being Int_position ex k1, k2 being Integer st I = MultBy (a,k1,b,k2)
take b ; ::_thesis: ex k1, k2 being Integer st I = MultBy (a,k1,b,k2)
take k1 ; ::_thesis: ex k2 being Integer st I = MultBy (a,k1,b,k2)
take k2 ; ::_thesis: I = MultBy (a,k1,b,k2)
thus I = MultBy (a,k1,b,k2) by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:38
for ins being Instruction of SCMPDS st InsCode ins = 12 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = Divide (a,k1,b,k2)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 12 implies ex a, b being Int_position ex k1, k2 being Integer st I = Divide (a,k1,b,k2) )
assume A1: InsCode I = 12 ; ::_thesis: ex a, b being Int_position ex k1, k2 being Integer st I = Divide (a,k1,b,k2)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,d2,k1,k2*>] and
A3: I1 in {9,10,11,12,13} by A1, Lm9;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A3, ENUMSET1:def_3;
then consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [12,{},<*d1,d2,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1, b = d2 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex b being Int_position ex k1, k2 being Integer st I = Divide (a,k1,b,k2)
take b ; ::_thesis: ex k1, k2 being Integer st I = Divide (a,k1,b,k2)
take k1 ; ::_thesis: ex k2 being Integer st I = Divide (a,k1,b,k2)
take k2 ; ::_thesis: I = Divide (a,k1,b,k2)
thus I = Divide (a,k1,b,k2) by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:39
for ins being Instruction of SCMPDS st InsCode ins = 13 holds
ex a, b being Int_position ex k1, k2 being Integer st ins = (a,k1) := (b,k2)
proof
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 13 implies ex a, b being Int_position ex k1, k2 being Integer st I = (a,k1) := (b,k2) )
assume A1: InsCode I = 13 ; ::_thesis: ex a, b being Int_position ex k1, k2 being Integer st I = (a,k1) := (b,k2)
( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
then consider I1 being Element of Segm 15, d1, d2 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A2: I = [I1,{},<*d1,d2,k1,k2*>] and
A3: I1 in {9,10,11,12,13} by A1, Lm9;
( I1 = 9 or I1 = 10 or I1 = 11 or I1 = 12 or I1 = 13 ) by A3, ENUMSET1:def_3;
then consider d1, d2 being Element of SCM-Data-Loc , k1, k2 being Integer such that
A4: I = [13,{},<*d1,d2,k1,k2*>] by A1, A2, RECDEF_2:def_1;
reconsider a = d1, b = d2 as Int_position by AMI_2:def_16;
take a ; ::_thesis: ex b being Int_position ex k1, k2 being Integer st I = (a,k1) := (b,k2)
take b ; ::_thesis: ex k1, k2 being Integer st I = (a,k1) := (b,k2)
take k1 ; ::_thesis: ex k2 being Integer st I = (a,k1) := (b,k2)
take k2 ; ::_thesis: I = (a,k1) := (b,k2)
thus I = (a,k1) := (b,k2) by A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:40
for s being State of SCMPDS
for d being Int_position holds d in dom s
proof
let s be State of SCMPDS; ::_thesis: for d being Int_position holds d in dom s
let d be Int_position; ::_thesis: d in dom s
dom s = the carrier of SCMPDS by PARTFUN1:def_2;
hence d in dom s ; ::_thesis: verum
end;
theorem Th41: :: SCMPDS_2:41
for s being State of SCMPDS holds SCM-Data-Loc c= dom s
proof
let s be State of SCMPDS; ::_thesis: SCM-Data-Loc c= dom s
dom s = the carrier of SCMPDS by PARTFUN1:def_2;
hence SCM-Data-Loc c= dom s ; ::_thesis: verum
end;
Lm10: Data-Locations = SCM-Data-Loc
proof
SCM-Data-Loc misses {NAT} by AMI_2:20, ZFMISC_1:50;
then A1: SCM-Data-Loc misses {NAT} ;
thus Data-Locations = ({NAT} \/ SCM-Data-Loc) \ {NAT} by AMI_2:22, FUNCT_7:def_1
.= (SCM-Data-Loc \/ {NAT}) \ {NAT}
.= SCM-Data-Loc \ {NAT} by XBOOLE_1:40
.= SCM-Data-Loc by A1, XBOOLE_1:83 ; ::_thesis: verum
end;
theorem :: SCMPDS_2:42
for s being State of SCMPDS holds dom (DataPart s) = SCM-Data-Loc
proof
let s be State of SCMPDS; ::_thesis: dom (DataPart s) = SCM-Data-Loc
SCM-Data-Loc c= dom s by Th41;
hence dom (DataPart s) = SCM-Data-Loc by Lm10, RELAT_1:62; ::_thesis: verum
end;
theorem :: SCMPDS_2:43
for dl being Int_position holds dl <> IC
proof
let dl be Int_position; ::_thesis: dl <> IC
Values dl = INT by Th5;
hence dl <> IC by MEMSTR_0:def_6, NUMBERS:27; ::_thesis: verum
end;
theorem :: SCMPDS_2:44
for s1, s2 being State of SCMPDS st IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) holds
s1 = s2
proof
let s1, s2 be State of SCMPDS; ::_thesis: ( IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1 . a = s2 . a ; ::_thesis: s1 = s2
A3: dom s1 = the carrier of SCMPDS by PARTFUN1:def_2;
A4: dom s2 = the carrier of SCMPDS by PARTFUN1:def_2;
A5: now__::_thesis:_for_x_being_set_st_x_in_SCM-Memory_holds_
s1_._x_=_s2_._x
let x be set ; ::_thesis: ( x in SCM-Memory implies s1 . b1 = s2 . b1 )
assume x in SCM-Memory ; ::_thesis: s1 . b1 = s2 . b1
then A6: x in {(IC )} \/ SCM-Data-Loc by Th2;
percases ( x in {(IC )} or x in SCM-Data-Loc ) by A6, XBOOLE_0:def_3;
suppose x in {(IC )} ; ::_thesis: s1 . b1 = s2 . b1
then x = IC by TARSKI:def_1;
hence s1 . x = s2 . x by A1; ::_thesis: verum
end;
suppose x in SCM-Data-Loc ; ::_thesis: s1 . b1 = s2 . b1
then x is Int_position by AMI_2:def_16;
hence s1 . x = s2 . x by A2; ::_thesis: verum
end;
end;
end;
SCM-Memory = dom s1 by A3;
hence s1 = s2 by A4, A5, FUNCT_1:2; ::_thesis: verum
end;
begin
theorem Th45: :: SCMPDS_2:45
for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((a := k1),s)) . (IC ) = succ (IC s) & (Exec ((a := k1),s)) . a = k1 & ( for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b ) )
proof
let s be State of SCMPDS; ::_thesis: for k1 being Integer
for a being Int_position holds
( (Exec ((a := k1),s)) . (IC ) = succ (IC s) & (Exec ((a := k1),s)) . a = k1 & ( for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b ) )
let k1 be Integer; ::_thesis: for a being Int_position holds
( (Exec ((a := k1),s)) . (IC ) = succ (IC s) & (Exec ((a := k1),s)) . a = k1 & ( for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b ) )
let a be Int_position; ::_thesis: ( (Exec ((a := k1),s)) . (IC ) = succ (IC s) & (Exec ((a := k1),s)) . a = k1 & ( for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = a := k1 as Element of SCMPDS-Instr ;
set S1 = SCM-Chg (S,(I P21address),(I P22const));
reconsider i = 2 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*mk,k1*>] ;
then A2: I P21address = mk by SCMPDS_I:5;
A3: I P22const = k1 by A1, SCMPDS_I:5;
A4: InsCode I = 2 by RECDEF_2:def_1;
A5: Exec ((a := k1),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(I P21address),(I P22const))),(succ (IC S))) by A4, SCMPDS_1:def_22 ;
hence (Exec ((a := k1),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (Exec ((a := k1),s)) . a = k1 & ( for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b ) )
thus (Exec ((a := k1),s)) . a = (SCM-Chg (S,(I P21address),(I P22const))) . mk by A5, AMI_2:12
.= k1 by A2, A3, AMI_2:15 ; ::_thesis: for b being Int_position st b <> a holds
(Exec ((a := k1),s)) . b = s . b
let b be Int_position; ::_thesis: ( b <> a implies (Exec ((a := k1),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: b <> a ; ::_thesis: (Exec ((a := k1),s)) . b = s . b
thus (Exec ((a := k1),s)) . b = (SCM-Chg (S,(I P21address),(I P22const))) . mn by A5, AMI_2:12
.= s . b by A2, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th46: :: SCMPDS_2:46
for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) & (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a being Int_position holds
( (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) & (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b ) )
let k1, k2 be Integer; ::_thesis: for a being Int_position holds
( (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) & (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b ) )
let a be Int_position; ::_thesis: ( (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) & (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = (a,k1) := k2 as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P31address),(I P32const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),(I P33const));
reconsider i = 7 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*mk,k1,k2*>] ;
then A2: I P33const = k2 by SCMPDS_I:6;
A3: InsCode I = 7 by RECDEF_2:def_1;
A4: Exec (((a,k1) := k2),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),(I P33const))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = k2 & ( for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b ) )
A5: ( I P31address = mk & I P32const = k1 ) by A1, SCMPDS_I:6;
hence (Exec (((a,k1) := k2),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),(I P33const))) . (Address_Add (S,(I P31address),(I P32const))) by A4, AMI_2:12
.= k2 by A2, AMI_2:15 ;
::_thesis: for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := k2),s)) . b = s . b
let b be Int_position; ::_thesis: ( b <> DataLoc ((s . a),k1) implies (Exec (((a,k1) := k2),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: b <> DataLoc ((s . a),k1) ; ::_thesis: (Exec (((a,k1) := k2),s)) . b = s . b
thus (Exec (((a,k1) := k2),s)) . b = (SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),(I P33const))) . mn by A4, AMI_2:12
.= s . b by A5, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th47: :: SCMPDS_2:47
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 ) = 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 ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a, b being Int_position holds
( (Exec (((a,k1) := (b,k2)),s)) . (IC ) = 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 ) )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( (Exec (((a,k1) := (b,k2)),s)) . (IC ) = 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 ) )
let a, b be Int_position; ::_thesis: ( (Exec (((a,k1) := (b,k2)),s)) . (IC ) = 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 ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider da = a, db = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = (a,k1) := (b,k2) as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P41address),(I P43const));
set A4 = Address_Add (S,(I P42address),(I P44const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),(S . (Address_Add (S,(I P42address),(I P44const)))));
reconsider i = 13 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*da,db,k1,k2*>] ;
then A2: ( I P42address = db & I P44const = k2 ) by SCMPDS_I:7;
A3: InsCode I = 13 by RECDEF_2:def_1;
A4: Exec (((a,k1) := (b,k2)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),(S . (Address_Add (S,(I P42address),(I P44const)))))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec (((a,k1) := (b,k2)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (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 ) )
A5: ( I P41address = da & I P43const = k1 ) by A1, SCMPDS_I:7;
hence (Exec (((a,k1) := (b,k2)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),(S . (Address_Add (S,(I P42address),(I P44const)))))) . (Address_Add (S,(I P41address),(I P43const))) by A4, AMI_2:12
.= s . (DataLoc ((s . b),k2)) by A2, AMI_2:15 ;
::_thesis: for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec (((a,k1) := (b,k2)),s)) . c = s . c
let c be Int_position; ::_thesis: ( c <> DataLoc ((s . a),k1) implies (Exec (((a,k1) := (b,k2)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: c <> DataLoc ((s . a),k1) ; ::_thesis: (Exec (((a,k1) := (b,k2)),s)) . c = s . c
thus (Exec (((a,k1) := (b,k2)),s)) . c = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),(S . (Address_Add (S,(I P42address),(I P44const)))))) . mn by A4, AMI_2:12
.= s . c by A5, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th48: :: SCMPDS_2:48
for s being State of SCMPDS
for k1, k2 being Integer
for a being Int_position holds
( (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = 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 ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a being Int_position holds
( (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = 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 ) )
let k1, k2 be Integer; ::_thesis: for a being Int_position holds
( (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = 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 ) )
let a be Int_position; ::_thesis: ( (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = 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 ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider mk = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = AddTo (a,k1,k2) as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P31address),(I P32const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),((S . (Address_Add (S,(I P31address),(I P32const)))) + (I P33const)));
reconsider i = 8 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*mk,k1,k2*>] ;
then A2: I P33const = k2 by SCMPDS_I:6;
A3: InsCode I = 8 by RECDEF_2:def_1;
A4: Exec ((AddTo (a,k1,k2)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),((S . (Address_Add (S,(I P31address),(I P32const)))) + (I P33const)))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (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 ) )
A5: ( I P31address = mk & I P32const = k1 ) by A1, SCMPDS_I:6;
hence (Exec ((AddTo (a,k1,k2)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),((S . (Address_Add (S,(I P31address),(I P32const)))) + (I P33const)))) . (Address_Add (S,(I P31address),(I P32const))) by A4, AMI_2:12
.= (s . (DataLoc ((s . a),k1))) + k2 by A5, A2, AMI_2:15 ;
::_thesis: for b being Int_position st b <> DataLoc ((s . a),k1) holds
(Exec ((AddTo (a,k1,k2)),s)) . b = s . b
let c be Int_position; ::_thesis: ( c <> DataLoc ((s . a),k1) implies (Exec ((AddTo (a,k1,k2)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: c <> DataLoc ((s . a),k1) ; ::_thesis: (Exec ((AddTo (a,k1,k2)),s)) . c = s . c
thus (Exec ((AddTo (a,k1,k2)),s)) . c = (SCM-Chg (S,(Address_Add (S,(I P31address),(I P32const))),((S . (Address_Add (S,(I P31address),(I P32const)))) + (I P33const)))) . mn by A4, AMI_2:12
.= s . c by A5, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th49: :: SCMPDS_2:49
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 ) = 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 ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( (Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let a, b be Int_position; ::_thesis: ( (Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = 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 ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider da = a, db = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = AddTo (a,k1,b,k2) as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P41address),(I P43const));
set A4 = Address_Add (S,(I P42address),(I P44const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) + (S . (Address_Add (S,(I P42address),(I P44const))))));
reconsider i = 9 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*da,db,k1,k2*>] ;
then A2: ( I P42address = db & I P44const = k2 ) by SCMPDS_I:7;
A3: InsCode I = 9 by RECDEF_2:def_1;
A4: Exec ((AddTo (a,k1,b,k2)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) + (S . (Address_Add (S,(I P42address),(I P44const))))))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (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 ) )
A5: ( I P41address = da & I P43const = k1 ) by A1, SCMPDS_I:7;
hence (Exec ((AddTo (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) + (S . (Address_Add (S,(I P42address),(I P44const))))))) . (Address_Add (S,(I P41address),(I P43const))) by A4, AMI_2:12
.= (s . (DataLoc ((s . a),k1))) + (s . (DataLoc ((s . b),k2))) by A5, A2, AMI_2:15 ;
::_thesis: for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((AddTo (a,k1,b,k2)),s)) . c = s . c
let c be Int_position; ::_thesis: ( c <> DataLoc ((s . a),k1) implies (Exec ((AddTo (a,k1,b,k2)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: c <> DataLoc ((s . a),k1) ; ::_thesis: (Exec ((AddTo (a,k1,b,k2)),s)) . c = s . c
thus (Exec ((AddTo (a,k1,b,k2)),s)) . c = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) + (S . (Address_Add (S,(I P42address),(I P44const))))))) . mn by A4, AMI_2:12
.= s . c by A5, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th50: :: SCMPDS_2:50
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 ) = 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 ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( (Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let a, b be Int_position; ::_thesis: ( (Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = 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 ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider da = a, db = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = SubFrom (a,k1,b,k2) as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P41address),(I P43const));
set A4 = Address_Add (S,(I P42address),(I P44const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) - (S . (Address_Add (S,(I P42address),(I P44const))))));
reconsider i = 10 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*da,db,k1,k2*>] ;
then A2: ( I P42address = db & I P44const = k2 ) by SCMPDS_I:7;
A3: InsCode I = 10 by RECDEF_2:def_1;
A4: Exec ((SubFrom (a,k1,b,k2)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) - (S . (Address_Add (S,(I P42address),(I P44const))))))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (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 ) )
A5: ( I P41address = da & I P43const = k1 ) by A1, SCMPDS_I:7;
hence (Exec ((SubFrom (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) - (S . (Address_Add (S,(I P42address),(I P44const))))))) . (Address_Add (S,(I P41address),(I P43const))) by A4, AMI_2:12
.= (s . (DataLoc ((s . a),k1))) - (s . (DataLoc ((s . b),k2))) by A5, A2, AMI_2:15 ;
::_thesis: for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((SubFrom (a,k1,b,k2)),s)) . c = s . c
let c be Int_position; ::_thesis: ( c <> DataLoc ((s . a),k1) implies (Exec ((SubFrom (a,k1,b,k2)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: c <> DataLoc ((s . a),k1) ; ::_thesis: (Exec ((SubFrom (a,k1,b,k2)),s)) . c = s . c
thus (Exec ((SubFrom (a,k1,b,k2)),s)) . c = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) - (S . (Address_Add (S,(I P42address),(I P44const))))))) . mn by A4, AMI_2:12
.= s . c by A5, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th51: :: SCMPDS_2:51
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 ) = 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 ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( (Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let a, b be Int_position; ::_thesis: ( (Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = 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 ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider da = a, db = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = MultBy (a,k1,b,k2) as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P41address),(I P43const));
set A4 = Address_Add (S,(I P42address),(I P44const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) * (S . (Address_Add (S,(I P42address),(I P44const))))));
reconsider i = 11 as Element of Segm 15 by NAT_1:44;
A1: I = [i,{},<*da,db,k1,k2*>] ;
then A2: ( I P42address = db & I P44const = k2 ) by SCMPDS_I:7;
A3: InsCode I = 11 by RECDEF_2:def_1;
A4: Exec ((MultBy (a,k1,b,k2)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) * (S . (Address_Add (S,(I P42address),(I P44const))))))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (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 ) )
A5: ( I P41address = da & I P43const = k1 ) by A1, SCMPDS_I:7;
hence (Exec ((MultBy (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) * (S . (Address_Add (S,(I P42address),(I P44const))))))) . (Address_Add (S,(I P41address),(I P43const))) by A4, AMI_2:12
.= (s . (DataLoc ((s . a),k1))) * (s . (DataLoc ((s . b),k2))) by A5, A2, AMI_2:15 ;
::_thesis: for c being Int_position st c <> DataLoc ((s . a),k1) holds
(Exec ((MultBy (a,k1,b,k2)),s)) . c = s . c
let c be Int_position; ::_thesis: ( c <> DataLoc ((s . a),k1) implies (Exec ((MultBy (a,k1,b,k2)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: c <> DataLoc ((s . a),k1) ; ::_thesis: (Exec ((MultBy (a,k1,b,k2)),s)) . c = s . c
thus (Exec ((MultBy (a,k1,b,k2)),s)) . c = (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) * (S . (Address_Add (S,(I P42address),(I P44const))))))) . mn by A4, AMI_2:12
.= s . c by A5, A6, AMI_2:16 ; ::_thesis: verum
end;
theorem Th52: :: SCMPDS_2:52
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 ) = 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 ) )
proof
let s be State of SCMPDS; ::_thesis: for k1, k2 being Integer
for a, b being Int_position holds
( (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = 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 ) )
let a, b be Int_position; ::_thesis: ( (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = 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 ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider da = a, db = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = Divide (a,k1,b,k2) as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P41address),(I P43const));
set A4 = Address_Add (S,(I P42address),(I P44const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))));
set S2 = SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))),(Address_Add (S,(I P42address),(I P44const))),((S . (Address_Add (S,(I P41address),(I P43const)))) mod (S . (Address_Add (S,(I P42address),(I P44const))))));
reconsider i = 12 as Element of Segm 15 by NAT_1:44;
set Da = DataLoc ((s . a),k1);
set Db = DataLoc ((s . b),k2);
A1: I = [i,{},<*da,db,k1,k2*>] ;
then A2: ( I P41address = da & I P43const = k1 ) by SCMPDS_I:7;
A3: InsCode I = 12 by RECDEF_2:def_1;
A4: Exec ((Divide (a,k1,b,k2)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))),(Address_Add (S,(I P42address),(I P44const))),((S . (Address_Add (S,(I P41address),(I P43const)))) mod (S . (Address_Add (S,(I P42address),(I P44const))))))),(succ (IC S))) by A3, SCMPDS_1:def_22 ;
hence (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( ( 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 ) )
A5: ( I P42address = db & I P44const = k2 ) by A1, SCMPDS_I:7;
hereby ::_thesis: ( (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 ) )
reconsider mn = DataLoc ((s . a),k1) as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: DataLoc ((s . a),k1) <> DataLoc ((s . b),k2) ; ::_thesis: (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2)))
thus (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))),(Address_Add (S,(I P42address),(I P44const))),((S . (Address_Add (S,(I P41address),(I P43const)))) mod (S . (Address_Add (S,(I P42address),(I P44const))))))) . mn by A4, AMI_2:12
.= (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))) . (Address_Add (S,(I P41address),(I P43const))) by A2, A5, A6, AMI_2:16
.= (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) by A2, A5, AMI_2:15 ; ::_thesis: verum
end;
thus (Exec ((Divide (a,k1,b,k2)),s)) . (DataLoc ((s . b),k2)) = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))),(Address_Add (S,(I P42address),(I P44const))),((S . (Address_Add (S,(I P41address),(I P43const)))) mod (S . (Address_Add (S,(I P42address),(I P44const))))))) . (Address_Add (S,(I P42address),(I P44const))) by A4, A5, AMI_2:12
.= (s . (DataLoc ((s . a),k1))) mod (s . (DataLoc ((s . b),k2))) by A2, A5, AMI_2:15 ; ::_thesis: 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
let c be Int_position; ::_thesis: ( c <> DataLoc ((s . a),k1) & c <> DataLoc ((s . b),k2) implies (Exec ((Divide (a,k1,b,k2)),s)) . c = s . c )
reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def_16;
assume that
A7: c <> DataLoc ((s . a),k1) and
A8: c <> DataLoc ((s . b),k2) ; ::_thesis: (Exec ((Divide (a,k1,b,k2)),s)) . c = s . c
thus (Exec ((Divide (a,k1,b,k2)),s)) . c = (SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))),(Address_Add (S,(I P42address),(I P44const))),((S . (Address_Add (S,(I P41address),(I P43const)))) mod (S . (Address_Add (S,(I P42address),(I P44const))))))) . mn by A4, AMI_2:12
.= (SCM-Chg (S,(Address_Add (S,(I P41address),(I P43const))),((S . (Address_Add (S,(I P41address),(I P43const)))) div (S . (Address_Add (S,(I P42address),(I P44const))))))) . mn by A5, A8, AMI_2:16
.= s . c by A2, A7, AMI_2:16 ; ::_thesis: verum
end;
theorem :: SCMPDS_2:53
for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((Divide (a,k1,a,k1)),s)) . (IC ) = 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 Th52;
definition
let s be State of SCMPDS;
let c be Integer;
func ICplusConst (s,c) -> Element of NAT means :Def18: :: SCMPDS_2:def 18
ex m being Element of NAT st
( m = IC s & it = abs (m + c) );
existence
ex b1, m being Element of NAT st
( m = IC s & b1 = abs (m + c) )
proof
reconsider m1 = IC s as Element of NAT ;
consider k being Element of NAT such that
A1: m1 = k ;
reconsider m = abs (k + c) as Nat ;
reconsider l = m as Element of NAT ;
take l ; ::_thesis: ex m being Element of NAT st
( m = IC s & l = abs (m + c) )
thus ex m being Element of NAT st
( m = IC s & l = abs (m + c) ) by A1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of NAT st ex m being Element of NAT st
( m = IC s & b1 = abs (m + c) ) & ex m being Element of NAT st
( m = IC s & b2 = abs (m + c) ) holds
b1 = b2;
;
end;
:: deftheorem Def18 defines ICplusConst SCMPDS_2:def_18_:_
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 Th54: :: SCMPDS_2:54
for s being State of SCMPDS
for k1 being Integer holds
( (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) & ( for a being Int_position holds (Exec ((goto k1),s)) . a = s . a ) )
proof
let s be State of SCMPDS; ::_thesis: for k1 being Integer holds
( (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) & ( for a being Int_position holds (Exec ((goto k1),s)) . a = s . a ) )
let k1 be Integer; ::_thesis: ( (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) & ( for a being Int_position holds (Exec ((goto k1),s)) . a = s . a ) )
reconsider i = 14 as Element of Segm 15 by NAT_1:44;
reconsider I = goto k1 as Element of SCMPDS-Instr ;
reconsider S = s as SCM-State by CARD_3:107;
I = [i,{},<*k1*>] ;
then A1: I const_INT = k1 by SCMPDS_I:4;
A2: InsCode I = 14 by RECDEF_2:def_1;
A3: Exec ((goto k1),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg (S,(jump_address (S,(I const_INT)))) by A2, SCMPDS_1:def_22 ;
ex n being Element of NAT st
( n = IC s & ICplusConst (s,k1) = abs (n + k1) ) by Def18;
hence (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) by A3, A1, Th2, AMI_2:11; ::_thesis: for a being Int_position holds (Exec ((goto k1),s)) . a = s . a
let a be Int_position; ::_thesis: (Exec ((goto k1),s)) . a = s . a
reconsider mn = a as Element of SCM-Data-Loc by AMI_2:def_16;
thus (Exec ((goto k1),s)) . a = S . mn by A3, AMI_2:12
.= s . a ; ::_thesis: verum
end;
theorem Th55: :: SCMPDS_2:55
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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )
proof
let s be State of SCMPDS; ::_thesis: 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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) <> 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )
let a, b be Int_position; ::_thesis: ( ( s . (DataLoc ((s . a),k1)) <> 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider S = s as SCM-State by CARD_3:107;
A1: ex n being Element of NAT st
( n = IC s & ICplusConst (s,k2) = abs (n + k2) ) by Def18;
reconsider da = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = (a,k1) <>0_goto k2 as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P31address),(I P32const));
set JP = jump_address (S,(I P33const));
set IF = IFEQ ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const))));
set Da = DataLoc ((s . a),k1);
reconsider i = 4 as Element of Segm 15 by NAT_1:44;
A2: I = [i,{},<*da,k1,k2*>] ;
then A3: ( I P31address = da & I P32const = k1 ) by SCMPDS_I:6;
A4: InsCode I = 4 by RECDEF_2:def_1;
A5: Exec (((a,k1) <>0_goto k2),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg (S,(IFEQ ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))))) by A4, SCMPDS_1:def_22 ;
A6: I P33const = k2 by A2, SCMPDS_I:6;
thus ( s . (DataLoc ((s . a),k1)) <> 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) ::_thesis: ( ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <>0_goto k2),s)) . b = s . b )
proof
assume A7: s . (DataLoc ((s . a),k1)) <> 0 ; ::_thesis: (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = ICplusConst (s,k2)
thus (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = IFEQ ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= ICplusConst (s,k2) by A3, A6, A1, A7, Th2, FUNCOP_1:def_8 ; ::_thesis: verum
end;
thus ( s . (DataLoc ((s . a),k1)) = 0 implies (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) ) ::_thesis: (Exec (((a,k1) <>0_goto k2),s)) . b = s . b
proof
assume A8: s . (DataLoc ((s . a),k1)) = 0 ; ::_thesis: (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s)
thus (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = IFEQ ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= succ (IC S) by A3, A8, FUNCOP_1:def_8
.= succ (IC s) by AMI_2:22, FUNCT_7:def_1 ; ::_thesis: verum
end;
thus (Exec (((a,k1) <>0_goto k2),s)) . b = S . mn by A5, AMI_2:12
.= s . b ; ::_thesis: verum
end;
theorem Th56: :: SCMPDS_2:56
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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )
proof
let s be State of SCMPDS; ::_thesis: 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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) <= 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )
let a, b be Int_position; ::_thesis: ( ( s . (DataLoc ((s . a),k1)) <= 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider S = s as SCM-State by CARD_3:107;
A1: ex n being Element of NAT st
( n = IC s & ICplusConst (s,k2) = abs (n + k2) ) by Def18;
reconsider da = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = (a,k1) <=0_goto k2 as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P31address),(I P32const));
set JP = jump_address (S,(I P33const));
set IF = IFGT ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const))));
set Da = DataLoc ((s . a),k1);
reconsider i = 5 as Element of Segm 15 by NAT_1:44;
A2: I = [i,{},<*da,k1,k2*>] ;
then A3: ( I P31address = da & I P32const = k1 ) by SCMPDS_I:6;
A4: InsCode I = 5 by RECDEF_2:def_1;
A5: Exec (((a,k1) <=0_goto k2),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg (S,(IFGT ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))))) by A4, SCMPDS_1:def_22 ;
A6: I P33const = k2 by A2, SCMPDS_I:6;
thus ( s . (DataLoc ((s . a),k1)) <= 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) ::_thesis: ( ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) <=0_goto k2),s)) . b = s . b )
proof
assume A7: s . (DataLoc ((s . a),k1)) <= 0 ; ::_thesis: (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = ICplusConst (s,k2)
thus (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = IFGT ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= ICplusConst (s,k2) by A3, A6, A1, A7, Th2, XXREAL_0:def_11 ; ::_thesis: verum
end;
thus ( s . (DataLoc ((s . a),k1)) > 0 implies (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) ) ::_thesis: (Exec (((a,k1) <=0_goto k2),s)) . b = s . b
proof
assume A8: s . (DataLoc ((s . a),k1)) > 0 ; ::_thesis: (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s)
thus (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = IFGT ((S . (Address_Add (S,(I P31address),(I P32const)))),0,(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= succ (IC S) by A3, A8, XXREAL_0:def_11
.= succ (IC s) by AMI_2:22, FUNCT_7:def_1 ; ::_thesis: verum
end;
thus (Exec (((a,k1) <=0_goto k2),s)) . b = S . mn by A5, AMI_2:12
.= s . b ; ::_thesis: verum
end;
theorem Th57: :: SCMPDS_2:57
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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
proof
let s be State of SCMPDS; ::_thesis: 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 ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds
( ( s . (DataLoc ((s . a),k1)) >= 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
let a, b be Int_position; ::_thesis: ( ( s . (DataLoc ((s . a),k1)) >= 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) & ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider S = s as SCM-State by CARD_3:107;
A1: ex n being Element of NAT st
( n = IC s & ICplusConst (s,k2) = abs (n + k2) ) by Def18;
reconsider da = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = (a,k1) >=0_goto k2 as Element of SCMPDS-Instr ;
set A2 = Address_Add (S,(I P31address),(I P32const));
set JP = jump_address (S,(I P33const));
set IF = IFGT (0,(S . (Address_Add (S,(I P31address),(I P32const)))),(succ (IC S)),(jump_address (S,(I P33const))));
set Da = DataLoc ((s . a),k1);
reconsider i = 6 as Element of Segm 15 by NAT_1:44;
A2: I = [i,{},<*da,k1,k2*>] ;
then A3: ( I P31address = da & I P32const = k1 ) by SCMPDS_I:6;
A4: InsCode I = 6 by RECDEF_2:def_1;
A5: Exec (((a,k1) >=0_goto k2),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg (S,(IFGT (0,(S . (Address_Add (S,(I P31address),(I P32const)))),(succ (IC S)),(jump_address (S,(I P33const)))))) by A4, SCMPDS_1:def_22 ;
A6: I P33const = k2 by A2, SCMPDS_I:6;
thus ( s . (DataLoc ((s . a),k1)) >= 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = ICplusConst (s,k2) ) ::_thesis: ( ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) & (Exec (((a,k1) >=0_goto k2),s)) . b = s . b )
proof
assume A7: s . (DataLoc ((s . a),k1)) >= 0 ; ::_thesis: (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = ICplusConst (s,k2)
thus (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = IFGT (0,(S . (Address_Add (S,(I P31address),(I P32const)))),(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= ICplusConst (s,k2) by A3, A6, A1, A7, Th2, XXREAL_0:def_11 ; ::_thesis: verum
end;
thus ( s . (DataLoc ((s . a),k1)) < 0 implies (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) ) ::_thesis: (Exec (((a,k1) >=0_goto k2),s)) . b = s . b
proof
assume A8: s . (DataLoc ((s . a),k1)) < 0 ; ::_thesis: (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s)
thus (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = IFGT (0,(S . (Address_Add (S,(I P31address),(I P32const)))),(succ (IC S)),(jump_address (S,(I P33const)))) by A5, Th2, AMI_2:11
.= succ (IC S) by A3, A8, XXREAL_0:def_11
.= succ (IC s) by AMI_2:22, FUNCT_7:def_1 ; ::_thesis: verum
end;
thus (Exec (((a,k1) >=0_goto k2),s)) . b = S . mn by A5, AMI_2:12
.= s . b ; ::_thesis: verum
end;
theorem Th58: :: SCMPDS_2:58
for s being State of SCMPDS
for a being Int_position holds
( (Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 & (Exec ((return a),s)) . a = s . (DataLoc ((s . a),RetSP)) & ( for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b ) )
proof
let s be State of SCMPDS; ::_thesis: for a being Int_position holds
( (Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 & (Exec ((return a),s)) . a = s . (DataLoc ((s . a),RetSP)) & ( for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b ) )
let a be Int_position; ::_thesis: ( (Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 & (Exec ((return a),s)) . a = s . (DataLoc ((s . a),RetSP)) & ( for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider da = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = return a as Element of SCMPDS-Instr ;
set A1 = Address_Add (S,(I address_1),RetSP);
set S1 = SCM-Chg (S,(I address_1),(S . (Address_Add (S,(I address_1),RetSP))));
set A2 = Address_Add (S,(I address_1),RetIC);
set lc = PopInstrLoc (S,(Address_Add (S,(I address_1),RetIC)));
reconsider i = 1 as Element of Segm 15 by NAT_1:44;
I = [i,{},<*da*>] ;
then A1: I address_1 = da by SCMPDS_I:3;
A2: InsCode I = 1 by RECDEF_2:def_1;
A3: Exec ((return a),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(I address_1),(S . (Address_Add (S,(I address_1),RetSP))))),(PopInstrLoc (S,(Address_Add (S,(I address_1),RetIC))))) by A2, SCMPDS_1:def_22 ;
hence (Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 by A1, Th2, AMI_2:11; ::_thesis: ( (Exec ((return a),s)) . a = s . (DataLoc ((s . a),RetSP)) & ( for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b ) )
thus (Exec ((return a),s)) . a = (SCM-Chg (S,(I address_1),(S . (Address_Add (S,(I address_1),RetSP))))) . da by A3, AMI_2:12
.= s . (DataLoc ((s . a),RetSP)) by A1, AMI_2:15 ; ::_thesis: for b being Int_position st a <> b holds
(Exec ((return a),s)) . b = s . b
let b be Int_position; ::_thesis: ( a <> b implies (Exec ((return a),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
assume A4: b <> a ; ::_thesis: (Exec ((return a),s)) . b = s . b
thus (Exec ((return a),s)) . b = (SCM-Chg (S,(I address_1),(S . (Address_Add (S,(I address_1),RetSP))))) . mn by A3, AMI_2:12
.= s . b by A1, A4, AMI_2:16 ; ::_thesis: verum
end;
theorem Th59: :: SCMPDS_2:59
for s being State of SCMPDS
for k1 being Integer
for a being Int_position holds
( (Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) & (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )
proof
let s be State of SCMPDS; ::_thesis: for k1 being Integer
for a being Int_position holds
( (Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) & (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )
let k1 be Integer; ::_thesis: for a being Int_position holds
( (Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) & (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )
let a be Int_position; ::_thesis: ( (Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) & (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )
reconsider S = s as SCM-State by CARD_3:107;
reconsider m = IC S as Element of NAT ;
reconsider da = a as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = saveIC (a,k1) as Element of SCMPDS-Instr ;
set A1 = Address_Add (S,(I P21address),(I P22const));
set S1 = SCM-Chg (S,(Address_Add (S,(I P21address),(I P22const))),m);
reconsider i = 3 as Element of Segm 15 by NAT_1:44;
set DL = DataLoc ((s . a),k1);
I = [i,{},<*da,k1*>] ;
then A1: ( I P21address = da & I P22const = k1 ) by SCMPDS_I:5;
A2: InsCode I = 3 by RECDEF_2:def_1;
A3: Exec ((saveIC (a,k1)),s) = SCM-Exec-Res (I,S) by SCMPDS_1:def_23
.= SCM-Chg ((SCM-Chg (S,(Address_Add (S,(I P21address),(I P22const))),m)),(succ (IC S))) by A2, SCMPDS_1:def_22 ;
hence (Exec ((saveIC (a,k1)),s)) . (IC ) = succ (IC s) by Th2, AMI_2:11; ::_thesis: ( (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = IC s & ( for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b ) )
thus (Exec ((saveIC (a,k1)),s)) . (DataLoc ((s . a),k1)) = (SCM-Chg (S,(Address_Add (S,(I P21address),(I P22const))),m)) . (Address_Add (S,(I P21address),(I P22const))) by A3, A1, AMI_2:12
.= IC s by Th2, AMI_2:15 ; ::_thesis: for b being Int_position st DataLoc ((s . a),k1) <> b holds
(Exec ((saveIC (a,k1)),s)) . b = s . b
let b be Int_position; ::_thesis: ( DataLoc ((s . a),k1) <> b implies (Exec ((saveIC (a,k1)),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
assume A4: DataLoc ((s . a),k1) <> b ; ::_thesis: (Exec ((saveIC (a,k1)),s)) . b = s . b
thus (Exec ((saveIC (a,k1)),s)) . b = (SCM-Chg (S,(Address_Add (S,(I P21address),(I P22const))),m)) . mn by A3, AMI_2:12
.= s . b by A1, A4, AMI_2:16 ; ::_thesis: verum
end;
theorem :: SCMPDS_2:60
canceled;
theorem Th61: :: SCMPDS_2:61
for k being Integer ex s being State of SCMPDS st
for d being Int_position holds s . d = k
proof
set f = the_Values_of SCMPDS;
set S = the SCM-State;
let k be Integer; ::_thesis: ex s being State of SCMPDS st
for d being Int_position holds s . d = k
A1: dom the SCM-State = the carrier of SCMPDS by PARTFUN1:def_2;
A2: dom (the_Values_of SCMPDS) = SCM-Memory by PARTFUN1:def_2;
k in INT by INT_1:def_2;
then reconsider g = SCM-Data-Loc --> k as Function of SCM-Data-Loc,INT by FUNCOP_1:45;
set t = the SCM-State +* g;
A3: for x being set st x in dom (the_Values_of SCMPDS) holds
( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCMPDS) implies ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x )
assume A4: x in dom (the_Values_of SCMPDS) ; ::_thesis: ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x
percases ( x in dom g or not x in dom g ) ;
supposeA5: x in dom g ; ::_thesis: ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x
then A6: x in SCM-Data-Loc by FUNCT_2:def_1;
then A7: (the_Values_of SCMPDS) . x = INT by AMI_2:8;
( the SCM-State +* g) . x = g . x by A5, FUNCT_4:13
.= k by A6, FUNCOP_1:7 ;
hence ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x by A7, INT_1:def_2; ::_thesis: verum
end;
suppose not x in dom g ; ::_thesis: ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x
then ( the SCM-State +* g) . x = the SCM-State . x by FUNCT_4:11;
hence ( the SCM-State +* g) . x in (the_Values_of SCMPDS) . x by A4, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom ( the SCM-State +* g) = (dom the SCM-State) \/ (dom g) by FUNCT_4:def_1
.= SCM-Memory \/ (dom g) by A1
.= SCM-Memory \/ SCM-Data-Loc by FUNCT_2:def_1
.= SCM-Memory by XBOOLE_1:12 ;
then reconsider s = the SCM-State +* g as State of SCMPDS by A2, A3, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
take s ; ::_thesis: for d being Int_position holds s . d = k
let d be Int_position; ::_thesis: s . d = k
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def_16;
D in SCM-Data-Loc ;
then D in dom g by FUNCT_2:def_1;
hence s . d = g . D by FUNCT_4:13
.= k by FUNCOP_1:7 ;
::_thesis: verum
end;
theorem Th62: :: SCMPDS_2:62
for k being Integer
for loc being Element of NAT ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
proof
set f = the_Values_of SCMPDS;
let k be Integer; ::_thesis: for loc being Element of NAT ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
let loc be Element of NAT ; ::_thesis: ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
A1: {NAT} c= SCM-Memory by AMI_2:22, ZFMISC_1:31;
A2: dom (the_Values_of SCMPDS) = SCM-Memory by PARTFUN1:def_2;
consider s1 being State of SCMPDS such that
A3: for d being Int_position holds s1 . d = k by Th61;
reconsider S = s1 as SCM-State by CARD_3:107;
set t = S +* (NAT .--> loc);
A4: dom S = the carrier of SCMPDS by PARTFUN1:def_2;
A5: dom (NAT .--> loc) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> loc) by TARSKI:def_1;
then A6: (S +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:13
.= loc by FUNCOP_1:72 ;
then A7: (S +* (NAT .--> loc)) . NAT in NAT ;
A8: for x being set st x in dom (the_Values_of SCMPDS) holds
(S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCMPDS) implies (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x )
assume A9: x in dom (the_Values_of SCMPDS) ; ::_thesis: (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x
percases ( x = NAT or x <> NAT ) ;
suppose x = NAT ; ::_thesis: (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x
hence (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x by A7, AMI_2:6; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x
then not x in dom (NAT .--> loc) by A5, TARSKI:def_1;
then (S +* (NAT .--> loc)) . x = S . x by FUNCT_4:11;
hence (S +* (NAT .--> loc)) . x in (the_Values_of SCMPDS) . x by A9, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom (S +* (NAT .--> loc)) = (dom S) \/ (dom (NAT .--> loc)) by FUNCT_4:def_1
.= SCM-Memory \/ (dom (NAT .--> loc)) by A4
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= SCM-Memory by A1, XBOOLE_1:12 ;
then reconsider s = S +* (NAT .--> loc) as State of SCMPDS by A2, A8, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
take s ; ::_thesis: ( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
thus s . NAT = loc by A6; ::_thesis: for d being Int_position holds s . d = k
hereby ::_thesis: verum
let d be Int_position; ::_thesis: s . d = k
d in SCM-Data-Loc by AMI_2:def_16;
then A10: ex j being Element of NAT st d = [1,j] by AMI_2:23;
not d in dom (NAT .--> loc) by A5, A10, TARSKI:def_1;
hence s . d = s1 . d by FUNCT_4:11
.= k by A3 ;
::_thesis: verum
end;
end;
Lm11: for s being State of SCMPDS
for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s
proof
let s be State of SCMPDS; ::_thesis: for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s
let I be Instruction of SCMPDS; ::_thesis: ( InsCode I = 0 implies Exec (I,s) = s )
assume InsCode I = 0 ; ::_thesis: Exec (I,s) = s
then A1: ( InsCode I <> 1 & InsCode I <> 2 & InsCode I <> 3 & InsCode I <> 4 & InsCode I <> 5 & InsCode I <> 6 & InsCode I <> 7 & InsCode I <> 8 & InsCode I <> 9 & InsCode I <> 10 & InsCode I <> 11 & InsCode I <> 12 & InsCode I <> 13 & InsCode I <> 14 ) ;
reconsider ss = s as SCM-State by CARD_3:107;
reconsider ii = I as Element of SCMPDS-Instr ;
thus Exec (I,s) = ( the Execution of SCMPDS . I) . s
.= (SCMPDS-Exec . I) . s
.= SCM-Exec-Res (ii,ss) by SCMPDS_1:def_23
.= s by A1, SCMPDS_1:def_22 ; ::_thesis: verum
end;
theorem Th63: :: SCMPDS_2:63
for I being Instruction of SCMPDS st I = [0,{},{}] holds
I is halting
proof
let I be Instruction of SCMPDS; ::_thesis: ( I = [0,{},{}] implies I is halting )
assume I = [0,{},{}] ; ::_thesis: I is halting
then A1: InsCode I = 0 by RECDEF_2:def_1;
let s be State of SCMPDS; :: according to EXTPRO_1:def_3 ::_thesis: Exec (I,s) = s
thus Exec (I,s) = s by A1, Lm11; ::_thesis: verum
end;
theorem Th64: :: SCMPDS_2:64
for I being Instruction of SCMPDS st ex s being State of SCMPDS st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting
proof
let I be Instruction of SCMPDS; ::_thesis: ( ex s being State of SCMPDS st (Exec (I,s)) . (IC ) = succ (IC s) implies not I is halting )
given s being State of SCMPDS such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; ::_thesis: not I is halting
assume I is halting ; ::_thesis: contradiction
then (Exec (I,s)) . (IC ) = s . NAT by Th2, EXTPRO_1:def_3;
hence contradiction by A1, Th2; ::_thesis: verum
IC s = s . NAT by AMI_2:22, FUNCT_7:def_1;
then reconsider w = s . NAT as Element of NAT ;
end;
theorem :: SCMPDS_2:65
for k1 being Integer
for a being Int_position holds not a := k1 is halting
proof
let k1 be Integer; ::_thesis: for a being Int_position holds not a := k1 is halting
let a be Int_position; ::_thesis: not a := k1 is halting
set s = the State of SCMPDS;
(Exec ((a := k1), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th45;
hence not a := k1 is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:66
for k1, k2 being Integer
for a being Int_position holds not (a,k1) := k2 is halting
proof
let k1, k2 be Integer; ::_thesis: for a being Int_position holds not (a,k1) := k2 is halting
let a be Int_position; ::_thesis: not (a,k1) := k2 is halting
set s = the State of SCMPDS;
(Exec (((a,k1) := k2), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th46;
hence not (a,k1) := k2 is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:67
for k1, k2 being Integer
for a, b being Int_position holds not (a,k1) := (b,k2) is halting
proof
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds not (a,k1) := (b,k2) is halting
let a, b be Int_position; ::_thesis: not (a,k1) := (b,k2) is halting
set s = the State of SCMPDS;
(Exec (((a,k1) := (b,k2)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th47;
hence not (a,k1) := (b,k2) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:68
for k1, k2 being Integer
for a being Int_position holds not AddTo (a,k1,k2) is halting
proof
let k1, k2 be Integer; ::_thesis: for a being Int_position holds not AddTo (a,k1,k2) is halting
let a be Int_position; ::_thesis: not AddTo (a,k1,k2) is halting
set s = the State of SCMPDS;
(Exec ((AddTo (a,k1,k2)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th48;
hence not AddTo (a,k1,k2) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:69
for k1, k2 being Integer
for a, b being Int_position holds not AddTo (a,k1,b,k2) is halting
proof
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds not AddTo (a,k1,b,k2) is halting
let a, b be Int_position; ::_thesis: not AddTo (a,k1,b,k2) is halting
set s = the State of SCMPDS;
(Exec ((AddTo (a,k1,b,k2)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th49;
hence not AddTo (a,k1,b,k2) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:70
for k1, k2 being Integer
for a, b being Int_position holds not SubFrom (a,k1,b,k2) is halting
proof
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds not SubFrom (a,k1,b,k2) is halting
let a, b be Int_position; ::_thesis: not SubFrom (a,k1,b,k2) is halting
set s = the State of SCMPDS;
(Exec ((SubFrom (a,k1,b,k2)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th50;
hence not SubFrom (a,k1,b,k2) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:71
for k1, k2 being Integer
for a, b being Int_position holds not MultBy (a,k1,b,k2) is halting
proof
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds not MultBy (a,k1,b,k2) is halting
let a, b be Int_position; ::_thesis: not MultBy (a,k1,b,k2) is halting
set s = the State of SCMPDS;
(Exec ((MultBy (a,k1,b,k2)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th51;
hence not MultBy (a,k1,b,k2) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:72
for k1, k2 being Integer
for a, b being Int_position holds not Divide (a,k1,b,k2) is halting
proof
let k1, k2 be Integer; ::_thesis: for a, b being Int_position holds not Divide (a,k1,b,k2) is halting
let a, b be Int_position; ::_thesis: not Divide (a,k1,b,k2) is halting
set s = the State of SCMPDS;
(Exec ((Divide (a,k1,b,k2)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th52;
hence not Divide (a,k1,b,k2) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:73
for k1 being Integer st k1 <> 0 holds
not goto k1 is halting
proof
let k1 be Integer; ::_thesis: ( k1 <> 0 implies not goto k1 is halting )
assume A1: k1 <> 0 ; ::_thesis: not goto k1 is halting
set n = abs k1;
reconsider loc = (abs k1) + 1 as Element of NAT ;
consider s being State of SCMPDS such that
A2: s . NAT = loc and
for d being Int_position holds s . d = 0 by Th62;
- (abs k1) <= k1 by ABSVALUE:4;
then 0 - (abs k1) <= k1 ;
then A3: ((abs k1) + k1) * 1 >= 0 by XREAL_1:20;
ex m being Element of NAT st
( m = IC s & ICplusConst (s,k1) = abs (m + k1) ) by Def18;
then A4: (Exec ((goto k1),s)) . (IC ) = abs (((abs k1) + k1) + 1) by A2, Th2, Th54
.= (abs ((abs k1) + k1)) + (abs 1) by A3, ABSVALUE:11
.= (abs ((abs k1) + k1)) + 1 by ABSVALUE:def_1
.= ((abs k1) + k1) + 1 by A3, ABSVALUE:def_1
.= ((abs k1) + 1) + k1 ;
assume goto k1 is halting ; ::_thesis: contradiction
then (Exec ((goto k1),s)) . (IC ) = (abs k1) + 1 by A2, Th2, EXTPRO_1:def_3;
hence contradiction by A1, A4; ::_thesis: verum
end;
theorem :: SCMPDS_2:74
for k1, k2 being Integer
for a being Int_position holds not (a,k1) <>0_goto k2 is halting
proof
let k1, k2 be Integer; ::_thesis: for a being Int_position holds not (a,k1) <>0_goto k2 is halting
let a be Int_position; ::_thesis: not (a,k1) <>0_goto k2 is halting
consider s being State of SCMPDS such that
A1: for d being Int_position holds s . d = 0 by Th61;
s . (DataLoc ((s . a),k1)) = 0 by A1;
then (Exec (((a,k1) <>0_goto k2),s)) . (IC ) = succ (IC s) by Th55;
hence not (a,k1) <>0_goto k2 is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:75
for k1, k2 being Integer
for a being Int_position holds not (a,k1) <=0_goto k2 is halting
proof
let k1, k2 be Integer; ::_thesis: for a being Int_position holds not (a,k1) <=0_goto k2 is halting
let a be Int_position; ::_thesis: not (a,k1) <=0_goto k2 is halting
consider s being State of SCMPDS such that
A1: for d being Int_position holds s . d = 1 by Th61;
s . (DataLoc ((s . a),k1)) = 1 by A1;
then (Exec (((a,k1) <=0_goto k2),s)) . (IC ) = succ (IC s) by Th56;
hence not (a,k1) <=0_goto k2 is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:76
for k1, k2 being Integer
for a being Int_position holds not (a,k1) >=0_goto k2 is halting
proof
let k1, k2 be Integer; ::_thesis: for a being Int_position holds not (a,k1) >=0_goto k2 is halting
let a be Int_position; ::_thesis: not (a,k1) >=0_goto k2 is halting
consider s being State of SCMPDS such that
A1: for d being Int_position holds s . d = - 1 by Th61;
s . (DataLoc ((s . a),k1)) = - 1 by A1;
then (Exec (((a,k1) >=0_goto k2),s)) . (IC ) = succ (IC s) by Th57;
hence not (a,k1) >=0_goto k2 is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:77
for a being Int_position holds not return a is halting
proof
let a be Int_position; ::_thesis: not return a is halting
reconsider loc = 1 as Element of NAT ;
A1: In (NAT,SCM-Memory) = NAT by AMI_2:22, FUNCT_7:def_1;
consider s being State of SCMPDS such that
A2: s . NAT = loc and
A3: for d being Int_position holds s . d = 0 by Th62;
(Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 by Th58
.= (abs 0) + 2 by A3
.= 0 + 2 by ABSVALUE:def_1
.= succ (IC s) by A2, A1 ;
hence not return a is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:78
for k1 being Integer
for a being Int_position holds not saveIC (a,k1) is halting
proof
let k1 be Integer; ::_thesis: for a being Int_position holds not saveIC (a,k1) is halting
let a be Int_position; ::_thesis: not saveIC (a,k1) is halting
set s = the State of SCMPDS;
(Exec ((saveIC (a,k1)), the State of SCMPDS)) . (IC ) = succ (IC the State of SCMPDS) by Th59;
hence not saveIC (a,k1) is halting by Th64; ::_thesis: verum
end;
theorem :: SCMPDS_2:79
for I being set holds
( not I is Instruction of SCMPDS or I = [0,{},{}] 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) )
proof
let I be set ; ::_thesis: ( not I is Instruction of SCMPDS or I = [0,{},{}] 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) )
assume I is Instruction of SCMPDS ; ::_thesis: ( I = [0,{},{}] 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) )
then reconsider I = I as Instruction of SCMPDS ;
percases ( I in {[0,{},{}]} or I in { [14,{},<*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 15, 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 15, 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 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ) by Lm1;
suppose I in {[0,{},{}]} ; ::_thesis: ( I = [0,{},{}] 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) )
then I = [0,{},{}] by TARSKI:def_1;
hence ( I = [0,{},{}] 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) ) ; ::_thesis: verum
end;
suppose I in { [14,{},<*k1*>] where k1 is Element of INT : verum } ; ::_thesis: ( I = [0,{},{}] 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) )
then consider k1 being Element of INT such that
A1: I = [14,{},<*k1*>] ;
I = goto k1 by A1;
hence ( I = [0,{},{}] 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) ) ; ::_thesis: verum
end;
suppose I in { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; ::_thesis: ( I = [0,{},{}] 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) )
then consider d1 being Element of SCM-Data-Loc such that
A2: I = [1,{},<*d1*>] ;
reconsider a = d1 as Int_position by AMI_2:def_16;
I = return a by A2;
hence ( I = [0,{},{}] 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) ) ; ::_thesis: verum
end;
suppose I in { [I1,{},<*d2,k2*>] where I1 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I1 in {2,3} } ; ::_thesis: ( I = [0,{},{}] 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) )
then consider I2 being Element of Segm 15, d2 being Element of SCM-Data-Loc , k2 being Element of INT such that
A3: ( I = [I2,{},<*d2,k2*>] & I2 in {2,3} ) ;
reconsider a = d2 as Int_position by AMI_2:def_16;
( I = saveIC (a,k2) or I = a := k2 ) by A3, TARSKI:def_2;
hence ( I = [0,{},{}] 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) ) ; ::_thesis: verum
end;
suppose I in { [I2,{},<*d3,k3,k4*>] where I2 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } ; ::_thesis: ( I = [0,{},{}] 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) )
then consider I3 being Element of Segm 15, d3 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A4: ( I = [I3,{},<*d3,k1,k2*>] & I3 in {4,5,6,7,8} ) ;
reconsider a = d3 as Int_position by AMI_2:def_16;
( I = (a,k1) <>0_goto k2 or I = (a,k1) <=0_goto k2 or I = (a,k1) >=0_goto k2 or I = (a,k1) := k2 or I = AddTo (a,k1,k2) ) by A4, ENUMSET1:def_3;
hence ( I = [0,{},{}] 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) ) ; ::_thesis: verum
end;
suppose I in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } ; ::_thesis: ( I = [0,{},{}] 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) )
then consider I3 being Element of Segm 15, d4, d5 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A5: ( I = [I3,{},<*d4,d5,k1,k2*>] & I3 in {9,10,11,12,13} ) ;
reconsider a = d4, b = d5 as Int_position by AMI_2:def_16;
( I = AddTo (a,k1,b,k2) or I = SubFrom (a,k1,b,k2) or I = MultBy (a,k1,b,k2) or I = Divide (a,k1,b,k2) or I = (a,k1) := (b,k2) ) by A5, ENUMSET1:def_3;
hence ( I = [0,{},{}] 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) ) ; ::_thesis: verum
end;
end;
end;
registration
cluster SCMPDS -> strict halting ;
coherence
SCMPDS is halting
proof
thus halt SCMPDS is halting by Th63; :: according to EXTPRO_1:def_4 ::_thesis: verum
end;
end;
theorem :: SCMPDS_2:80
halt SCMPDS = [0,{},{}] ;
theorem :: SCMPDS_2:81
canceled;
theorem :: SCMPDS_2:82
for i being Element of NAT holds IC <> dl. i
proof
let i be Element of NAT ; ::_thesis: IC <> dl. i
assume IC = dl. i ; ::_thesis: contradiction
then NAT = [1,i] by Th2, AMI_3:def_11;
hence contradiction ; ::_thesis: verum
end;
theorem :: SCMPDS_2:83
canceled;
theorem :: SCMPDS_2:84
Data-Locations = SCM-Data-Loc by Lm10;
theorem :: SCMPDS_2:85
canceled;
theorem :: SCMPDS_2:86
for s being State of SCMPDS
for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s by Lm11;