:: 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;