:: The SCMPDS Computer and the Basic Semantics of Its Instructions :: by JingChao Chen :: :: Received June 15, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users 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 ) proofend; 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 proofend; 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 proofend; 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} } ) proofend; theorem :: SCMPDS_2:6 for I being Instruction of SCMPDS holds InsCode I <= 14 proofend; registration let s be State of SCMPDS; let d be Int_position; clusters . d -> integer ; coherence s . d is integer proofend; 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 proofend; 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 proofend; theorem Th8: :: SCMPDS_2:8 for d1 being Element of SCM-Data-Loc holds [1,{},<*d1*>] in SCMPDS-Instr proofend; 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 proofend; 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 proofend; 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 proofend; 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; proofend; 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; proofend; func saveIC (a,k1) -> Instruction of SCMPDS equals :: SCMPDS_2:def 7 [3,{},<*a,k1*>]; correctness coherence [3,{},<*a,k1*>] is Instruction of SCMPDS; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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; proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; Lm7: for I being Instruction of SCMPDS st I in {[0,{},{}]} holds InsCode I = 0 proofend; theorem :: SCMPDS_2:26 for ins being Instruction of SCMPDS st InsCode ins = 14 holds ex k1 being Integer st ins = goto k1 proofend; theorem :: SCMPDS_2:27 for ins being Instruction of SCMPDS st InsCode ins = 1 holds ex a being Int_position st ins = return a proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; 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 ) proofend; 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) proofend; 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) proofend; 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) proofend; 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) proofend; 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) proofend; theorem :: SCMPDS_2:40 for s being State of SCMPDS for d being Int_position holds d in dom s proofend; theorem Th41: :: SCMPDS_2:41 for s being State of SCMPDS holds SCM-Data-Loc c= dom s proofend; Lm10: Data-Locations = SCM-Data-Loc proofend; theorem :: SCMPDS_2:42 for s being State of SCMPDS holds dom (DataPart s) = SCM-Data-Loc proofend; theorem :: SCMPDS_2:43 for dl being Int_position holds dl <> IC proofend; 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 proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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) ) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 proofend; 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 ) ) proofend; Lm11: for s being State of SCMPDS for I being Instruction of SCMPDS st InsCode I = 0 holds Exec (I,s) = s proofend; theorem Th63: :: SCMPDS_2:63 for I being Instruction of SCMPDS st I = [0,{},{}] holds I is halting proofend; 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 proofend; theorem :: SCMPDS_2:65 for k1 being Integer for a being Int_position holds not a := k1 is halting proofend; theorem :: SCMPDS_2:66 for k1, k2 being Integer for a being Int_position holds not (a,k1) := k2 is halting proofend; theorem :: SCMPDS_2:67 for k1, k2 being Integer for a, b being Int_position holds not (a,k1) := (b,k2) is halting proofend; theorem :: SCMPDS_2:68 for k1, k2 being Integer for a being Int_position holds not AddTo (a,k1,k2) is halting proofend; theorem :: SCMPDS_2:69 for k1, k2 being Integer for a, b being Int_position holds not AddTo (a,k1,b,k2) is halting proofend; theorem :: SCMPDS_2:70 for k1, k2 being Integer for a, b being Int_position holds not SubFrom (a,k1,b,k2) is halting proofend; theorem :: SCMPDS_2:71 for k1, k2 being Integer for a, b being Int_position holds not MultBy (a,k1,b,k2) is halting proofend; theorem :: SCMPDS_2:72 for k1, k2 being Integer for a, b being Int_position holds not Divide (a,k1,b,k2) is halting proofend; theorem :: SCMPDS_2:73 for k1 being Integer st k1 <> 0 holds not goto k1 is halting proofend; theorem :: SCMPDS_2:74 for k1, k2 being Integer for a being Int_position holds not (a,k1) <>0_goto k2 is halting proofend; theorem :: SCMPDS_2:75 for k1, k2 being Integer for a being Int_position holds not (a,k1) <=0_goto k2 is halting proofend; theorem :: SCMPDS_2:76 for k1, k2 being Integer for a being Int_position holds not (a,k1) >=0_goto k2 is halting proofend; theorem :: SCMPDS_2:77 for a being Int_position holds not return a is halting proofend; theorem :: SCMPDS_2:78 for k1 being Integer for a being Int_position holds not saveIC (a,k1) is halting proofend; 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) ) proofend; :: Poniewaz zostal dodany prawdziwy halt, :: tego lematu nie mozna udowodnic. ::Lm11: for W being Instruction of SCMPDS st W is halting holds W = goto 0 ::proof :: set I = goto 0; :: let W be Instruction of SCMPDS such that ::A1: W is halting; :: assume ::A2: I <> W; :: per cases by Th91; :: suppose :: ex k1 st W=goto k1; :: hence thesis by A1,A2,Th85; :: end; :: suppose :: ex a st W = return a; :: hence thesis by A1,Th89; :: end; :: suppose :: ex a,k1 st W = saveIC(a,k1); :: hence thesis by A1,Th90; :: end; :: suppose :: ex a,k1 st W = a:=k1; :: hence thesis by A1,Th77; :: end; :: suppose :: ex a,k1,k2 st W=(a,k1):=k2; :: hence thesis by A1,Th78; :: end; :: suppose :: ex a,k1,k2 st W = (a,k1)<>0_goto k2; :: hence thesis by A1,Th86; :: end; :: suppose :: ex a,k1,k2 st W = (a,k1)<=0_goto k2; :: hence thesis by A1,Th87; :: end; :: suppose :: ex a,k1,k2 st W = (a,k1)>=0_goto k2; :: hence thesis by A1,Th88; :: end; :: suppose :: ex a,b,k1,k2 st W = AddTo(a,k1,k2); :: hence thesis by A1,Th80; :: end; :: suppose :: ex a,b,k1,k2 st W = AddTo(a,k1,b,k2); :: hence thesis by A1,Th81; :: end; :: suppose :: ex a,b,k1,k2 st W = SubFrom(a,k1,b,k2); :: hence thesis by A1,Th82; :: end; :: suppose :: ex a,b,k1,k2 st W = MultBy(a,k1,b,k2); :: hence thesis by A1,Th83; :: end; :: suppose :: ex a,b,k1,k2 st W = Divide(a,k1,b,k2); :: hence thesis by A1,Th84; :: end; :: suppose :: ex a,b,k1,k2 st W = (a,k1):=(b,k2); :: hence thesis by A1,Th79; :: end; ::end; registration cluster SCMPDS -> strict halting ; coherence SCMPDS is halting proofend; end; ::Dopoki sa przeskoki, to jednoznacznosc instrukcji, ktora jest halting :: i tak sie nie uda udowodnic. ::theorem Th92: :: for I being Instruction of SCMPDS st I is halting holds I = halt :: SCMPDS ::proof :: let I be Instruction of SCMPDS; :: assume I is halting; :: then I = goto 0 by Lm11; :: hence thesis by Lm11; ::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 proofend; 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;