:: The { \bf SCM_FSA } computer :: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki :: :: Received February 7, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin definition func SCM+FSA -> strict AMI-Struct over 3 equals :: SCMFSA_2:def 1 AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #); coherence AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3 ; end; :: deftheorem defines SCM+FSA SCMFSA_2:def_1_:_ SCM+FSA = AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #); registration cluster SCM+FSA -> non empty with_non-empty_values strict ; coherence ( not SCM+FSA is empty & SCM+FSA is with_non-empty_values ) proofend; end; registration cluster SCM+FSA -> strict with_non_trivial_Instructions ; coherence SCM+FSA is with_non_trivial_Instructions proofend; end; theorem Th1: :: SCMFSA_2:1 IC = NAT by FUNCT_7:def_1, SCMFSA_1:5; begin notation synonym Int-Locations for SCM+FSA-Data-Loc ; end; definition :: original:Int-Locations redefine func Int-Locations -> Subset of SCM+FSA; coherence Int-Locations is Subset of SCM+FSA proofend; canceled; func FinSeq-Locations -> Subset of SCM+FSA equals :: SCMFSA_2:def 3 SCM+FSA-Data*-Loc ; coherence SCM+FSA-Data*-Loc is Subset of SCM+FSA ; end; :: deftheorem SCMFSA_2:def_2_:_ canceled; :: deftheorem defines FinSeq-Locations SCMFSA_2:def_3_:_ FinSeq-Locations = SCM+FSA-Data*-Loc ; registration cluster Int-like for Element of the carrier of SCM+FSA; existence ex b1 being Object of SCM+FSA st b1 is Int-like proofend; end; definition mode Int-Location is Int-like Object of SCM+FSA; canceled; mode FinSeq-Location -> Object of SCM+FSA means :Def5: :: SCMFSA_2:def 5 it in SCM+FSA-Data*-Loc ; existence ex b1 being Object of SCM+FSA st b1 in SCM+FSA-Data*-Loc proofend; end; :: deftheorem SCMFSA_2:def_4_:_ canceled; :: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def_5_:_ for b1 being Object of SCM+FSA holds ( b1 is FinSeq-Location iff b1 in SCM+FSA-Data*-Loc ); theorem :: SCMFSA_2:2 canceled; theorem :: SCMFSA_2:3 canceled; theorem :: SCMFSA_2:4 canceled; theorem :: SCMFSA_2:5 canceled; theorem :: SCMFSA_2:6 canceled; definition let k be Nat; func intloc k -> Int-Location equals :: SCMFSA_2:def 6 dl. k; coherence dl. k is Int-Location proofend; func fsloc k -> FinSeq-Location equals :: SCMFSA_2:def 7 - (k + 1); coherence - (k + 1) is FinSeq-Location proofend; end; :: deftheorem defines intloc SCMFSA_2:def_6_:_ for k being Nat holds intloc k = dl. k; :: deftheorem defines fsloc SCMFSA_2:def_7_:_ for k being Nat holds fsloc k = - (k + 1); theorem :: SCMFSA_2:7 for k1, k2 being Nat st k1 <> k2 holds fsloc k1 <> fsloc k2 ; theorem :: SCMFSA_2:8 for dl being Int-Location ex i being Element of NAT st dl = intloc i proofend; theorem Th9: :: SCMFSA_2:9 for fl being FinSeq-Location ex i being Element of NAT st fl = fsloc i proofend; registration cluster FinSeq-Locations -> infinite ; coherence not FinSeq-Locations is finite proofend; end; theorem Th10: :: SCMFSA_2:10 for I being Int-Location holds I is Data-Location proofend; theorem Th11: :: SCMFSA_2:11 for l being Int-Location holds Values l = INT proofend; theorem Th12: :: SCMFSA_2:12 for l being FinSeq-Location holds Values l = INT * proofend; begin theorem :: SCMFSA_2:13 canceled; theorem :: SCMFSA_2:14 canceled; theorem Th15: :: SCMFSA_2:15 for I being Instruction of SCM+FSA st InsCode I <= 8 holds I is Instruction of SCM proofend; theorem Th16: :: SCMFSA_2:16 for I being Instruction of SCM+FSA holds InsCode I <= 12 proofend; theorem Th17: :: SCMFSA_2:17 for I being Instruction of SCM holds I is Instruction of SCM+FSA proofend; definition let a, b be Int-Location; funca := b -> Instruction of SCM+FSA means :Def8: :: SCMFSA_2:def 8 ex A, B being Data-Location st ( a = A & b = B & it = A := B ); existence ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st ( a = A & b = B & b1 = A := B ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st ( a = A & b = B & b1 = A := B ) & ex A, B being Data-Location st ( a = A & b = B & b2 = A := B ) holds b1 = b2; ; func AddTo (a,b) -> Instruction of SCM+FSA means :Def9: :: SCMFSA_2:def 9 ex A, B being Data-Location st ( a = A & b = B & it = AddTo (A,B) ); existence ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st ( a = A & b = B & b1 = AddTo (A,B) ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st ( a = A & b = B & b1 = AddTo (A,B) ) & ex A, B being Data-Location st ( a = A & b = B & b2 = AddTo (A,B) ) holds b1 = b2; ; func SubFrom (a,b) -> Instruction of SCM+FSA means :Def10: :: SCMFSA_2:def 10 ex A, B being Data-Location st ( a = A & b = B & it = SubFrom (A,B) ); existence ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st ( a = A & b = B & b1 = SubFrom (A,B) ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st ( a = A & b = B & b1 = SubFrom (A,B) ) & ex A, B being Data-Location st ( a = A & b = B & b2 = SubFrom (A,B) ) holds b1 = b2; ; func MultBy (a,b) -> Instruction of SCM+FSA means :Def11: :: SCMFSA_2:def 11 ex A, B being Data-Location st ( a = A & b = B & it = MultBy (A,B) ); existence ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st ( a = A & b = B & b1 = MultBy (A,B) ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st ( a = A & b = B & b1 = MultBy (A,B) ) & ex A, B being Data-Location st ( a = A & b = B & b2 = MultBy (A,B) ) holds b1 = b2; ; func Divide (a,b) -> Instruction of SCM+FSA means :Def12: :: SCMFSA_2:def 12 ex A, B being Data-Location st ( a = A & b = B & it = Divide (A,B) ); existence ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st ( a = A & b = B & b1 = Divide (A,B) ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st ( a = A & b = B & b1 = Divide (A,B) ) & ex A, B being Data-Location st ( a = A & b = B & b2 = Divide (A,B) ) holds b1 = b2; ; end; :: deftheorem Def8 defines := SCMFSA_2:def_8_:_ for a, b being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = a := b iff ex A, B being Data-Location st ( a = A & b = B & b3 = A := B ) ); :: deftheorem Def9 defines AddTo SCMFSA_2:def_9_:_ for a, b being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = AddTo (a,b) iff ex A, B being Data-Location st ( a = A & b = B & b3 = AddTo (A,B) ) ); :: deftheorem Def10 defines SubFrom SCMFSA_2:def_10_:_ for a, b being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = SubFrom (a,b) iff ex A, B being Data-Location st ( a = A & b = B & b3 = SubFrom (A,B) ) ); :: deftheorem Def11 defines MultBy SCMFSA_2:def_11_:_ for a, b being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = MultBy (a,b) iff ex A, B being Data-Location st ( a = A & b = B & b3 = MultBy (A,B) ) ); :: deftheorem Def12 defines Divide SCMFSA_2:def_12_:_ for a, b being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = Divide (a,b) iff ex A, B being Data-Location st ( a = A & b = B & b3 = Divide (A,B) ) ); definition let la be Element of NAT ; func goto la -> Instruction of SCM+FSA equals :: SCMFSA_2:def 13 SCM-goto la; coherence SCM-goto la is Instruction of SCM+FSA by Th17; let a be Int-Location; funca =0_goto la -> Instruction of SCM+FSA means :Def14: :: SCMFSA_2:def 14 ex A being Data-Location st ( a = A & it = A =0_goto la ); existence ex b1 being Instruction of SCM+FSA ex A being Data-Location st ( a = A & b1 = A =0_goto la ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A being Data-Location st ( a = A & b1 = A =0_goto la ) & ex A being Data-Location st ( a = A & b2 = A =0_goto la ) holds b1 = b2; ; funca >0_goto la -> Instruction of SCM+FSA means :Def15: :: SCMFSA_2:def 15 ex A being Data-Location st ( a = A & it = A >0_goto la ); existence ex b1 being Instruction of SCM+FSA ex A being Data-Location st ( a = A & b1 = A >0_goto la ) proofend; correctness uniqueness for b1, b2 being Instruction of SCM+FSA st ex A being Data-Location st ( a = A & b1 = A >0_goto la ) & ex A being Data-Location st ( a = A & b2 = A >0_goto la ) holds b1 = b2; ; end; :: deftheorem defines goto SCMFSA_2:def_13_:_ for la being Element of NAT holds goto la = SCM-goto la; :: deftheorem Def14 defines =0_goto SCMFSA_2:def_14_:_ for la being Element of NAT for a being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = a =0_goto la iff ex A being Data-Location st ( a = A & b3 = A =0_goto la ) ); :: deftheorem Def15 defines >0_goto SCMFSA_2:def_15_:_ for la being Element of NAT for a being Int-Location for b3 being Instruction of SCM+FSA holds ( b3 = a >0_goto la iff ex A being Data-Location st ( a = A & b3 = A >0_goto la ) ); definition let c, i be Int-Location; let a be FinSeq-Location ; funcc := (a,i) -> Instruction of SCM+FSA equals :: SCMFSA_2:def 16 [9,{},<*c,a,i*>]; coherence [9,{},<*c,a,i*>] is Instruction of SCM+FSA proofend; func(a,i) := c -> Instruction of SCM+FSA equals :: SCMFSA_2:def 17 [10,{},<*c,a,i*>]; coherence [10,{},<*c,a,i*>] is Instruction of SCM+FSA proofend; end; :: deftheorem defines := SCMFSA_2:def_16_:_ for c, i being Int-Location for a being FinSeq-Location holds c := (a,i) = [9,{},<*c,a,i*>]; :: deftheorem defines := SCMFSA_2:def_17_:_ for c, i being Int-Location for a being FinSeq-Location holds (a,i) := c = [10,{},<*c,a,i*>]; definition let i be Int-Location; let a be FinSeq-Location ; funci :=len a -> Instruction of SCM+FSA equals :: SCMFSA_2:def 18 [11,{},<*i,a*>]; coherence [11,{},<*i,a*>] is Instruction of SCM+FSA proofend; funca :=<0,...,0> i -> Instruction of SCM+FSA equals :: SCMFSA_2:def 19 [12,{},<*i,a*>]; coherence [12,{},<*i,a*>] is Instruction of SCM+FSA proofend; end; :: deftheorem defines :=len SCMFSA_2:def_18_:_ for i being Int-Location for a being FinSeq-Location holds i :=len a = [11,{},<*i,a*>]; :: deftheorem defines :=<0,...,0> SCMFSA_2:def_19_:_ for i being Int-Location for a being FinSeq-Location holds a :=<0,...,0> i = [12,{},<*i,a*>]; theorem :: SCMFSA_2:18 for a, b being Int-Location holds InsCode (a := b) = 1 proofend; theorem :: SCMFSA_2:19 for a, b being Int-Location holds InsCode (AddTo (a,b)) = 2 proofend; theorem :: SCMFSA_2:20 for a, b being Int-Location holds InsCode (SubFrom (a,b)) = 3 proofend; theorem :: SCMFSA_2:21 for a, b being Int-Location holds InsCode (MultBy (a,b)) = 4 proofend; theorem :: SCMFSA_2:22 for a, b being Int-Location holds InsCode (Divide (a,b)) = 5 proofend; theorem :: SCMFSA_2:23 for lb being Element of NAT holds InsCode (goto lb) = 6 by RECDEF_2:def_1; theorem :: SCMFSA_2:24 for lb being Element of NAT for a being Int-Location holds InsCode (a =0_goto lb) = 7 proofend; theorem :: SCMFSA_2:25 for lb being Element of NAT for a being Int-Location holds InsCode (a >0_goto lb) = 8 proofend; theorem :: SCMFSA_2:26 for fa being FinSeq-Location for c, a being Int-Location holds InsCode (c := (fa,a)) = 9 by RECDEF_2:def_1; theorem :: SCMFSA_2:27 for fa being FinSeq-Location for a, c being Int-Location holds InsCode ((fa,a) := c) = 10 by RECDEF_2:def_1; theorem :: SCMFSA_2:28 for fa being FinSeq-Location for a being Int-Location holds InsCode (a :=len fa) = 11 by RECDEF_2:def_1; theorem :: SCMFSA_2:29 for fa being FinSeq-Location for a being Int-Location holds InsCode (fa :=<0,...,0> a) = 12 by RECDEF_2:def_1; theorem Th30: :: SCMFSA_2:30 for ins being Instruction of SCM+FSA st InsCode ins = 1 holds ex da, db being Int-Location st ins = da := db proofend; theorem Th31: :: SCMFSA_2:31 for ins being Instruction of SCM+FSA st InsCode ins = 2 holds ex da, db being Int-Location st ins = AddTo (da,db) proofend; theorem Th32: :: SCMFSA_2:32 for ins being Instruction of SCM+FSA st InsCode ins = 3 holds ex da, db being Int-Location st ins = SubFrom (da,db) proofend; theorem Th33: :: SCMFSA_2:33 for ins being Instruction of SCM+FSA st InsCode ins = 4 holds ex da, db being Int-Location st ins = MultBy (da,db) proofend; theorem Th34: :: SCMFSA_2:34 for ins being Instruction of SCM+FSA st InsCode ins = 5 holds ex da, db being Int-Location st ins = Divide (da,db) proofend; theorem Th35: :: SCMFSA_2:35 for ins being Instruction of SCM+FSA st InsCode ins = 6 holds ex lb being Element of NAT st ins = goto lb proofend; theorem Th36: :: SCMFSA_2:36 for ins being Instruction of SCM+FSA st InsCode ins = 7 holds ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb proofend; theorem Th37: :: SCMFSA_2:37 for ins being Instruction of SCM+FSA st InsCode ins = 8 holds ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb proofend; theorem Th38: :: SCMFSA_2:38 for ins being Instruction of SCM+FSA st InsCode ins = 9 holds ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a) proofend; theorem Th39: :: SCMFSA_2:39 for ins being Instruction of SCM+FSA st InsCode ins = 10 holds ex a, b being Int-Location ex fa being FinSeq-Location st ins = (fa,a) := b proofend; theorem Th40: :: SCMFSA_2:40 for ins being Instruction of SCM+FSA st InsCode ins = 11 holds ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa proofend; theorem Th41: :: SCMFSA_2:41 for ins being Instruction of SCM+FSA st InsCode ins = 12 holds ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a proofend; begin theorem :: SCMFSA_2:42 for s being State of SCM+FSA for d being Int-Location holds d in dom s proofend; theorem :: SCMFSA_2:43 for f being FinSeq-Location for s being State of SCM+FSA holds f in dom s proofend; theorem Th44: :: SCMFSA_2:44 for f being FinSeq-Location for S being State of SCM holds not f in dom S proofend; theorem Th45: :: SCMFSA_2:45 for s being State of SCM+FSA holds Int-Locations c= dom s proofend; theorem Th46: :: SCMFSA_2:46 for s being State of SCM+FSA holds FinSeq-Locations c= dom s proofend; theorem :: SCMFSA_2:47 for s being State of SCM+FSA holds dom (s | Int-Locations) = Int-Locations proofend; theorem :: SCMFSA_2:48 for s being State of SCM+FSA holds dom (s | FinSeq-Locations) = FinSeq-Locations proofend; theorem Th49: :: SCMFSA_2:49 for s being State of SCM+FSA for i being Instruction of SCM holds s | SCM-Memory is State of SCM proofend; theorem :: SCMFSA_2:50 for s being State of SCM+FSA for s9 being State of SCM holds s +* s9 is State of SCM+FSA proofend; theorem Th51: :: SCMFSA_2:51 for i being Instruction of SCM for ii being Instruction of SCM+FSA for s being State of SCM for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds Exec (ii,ss) = ss +* (Exec (i,s)) proofend; registration let s be State of SCM+FSA; let d be Int-Location; clusters . d -> integer ; coherence s . d is integer proofend; end; definition let s be State of SCM+FSA; let d be FinSeq-Location ; :: original:. redefine funcs . d -> FinSequence of INT ; coherence s . d is FinSequence of INT proofend; end; theorem Th52: :: SCMFSA_2:52 for S being State of SCM for s being State of SCM+FSA st S = s | SCM-Memory holds s = s +* S by FUNCT_4:75; theorem Th53: :: SCMFSA_2:53 for S being State of SCM for s1, s being State of SCM+FSA st s1 = s +* S holds s1 . (IC ) = S . (IC ) proofend; theorem Th54: :: SCMFSA_2:54 for A being Data-Location for a being Int-Location for S being State of SCM for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds S . A = s1 . a proofend; theorem Th55: :: SCMFSA_2:55 for A being Data-Location for a being Int-Location for S being State of SCM for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds S . A = s . a proofend; registration cluster SCM+FSA -> IC-Ins-separated strict ; coherence SCM+FSA is IC-Ins-separated proofend; end; theorem Th56: :: SCMFSA_2:56 for dl being Int-Location holds dl <> IC proofend; theorem Th57: :: SCMFSA_2:57 for dl being FinSeq-Location holds dl <> IC proofend; theorem :: SCMFSA_2:58 for il being Int-Location for dl being FinSeq-Location holds il <> dl proofend; theorem :: SCMFSA_2:59 for il being Element of NAT for dl being Int-Location holds il <> dl proofend; theorem :: SCMFSA_2:60 for il being Element of NAT for dl being FinSeq-Location holds il <> dl proofend; theorem :: SCMFSA_2:61 for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds s1 = s2 proofend; theorem Th62: :: SCMFSA_2:62 for S being State of SCM for s being State of SCM+FSA st S = s | SCM-Memory holds IC s = IC S proofend; begin theorem Th63: :: SCMFSA_2:63 for a, b being Int-Location for s being State of SCM+FSA holds ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds (Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) ) proofend; theorem Th64: :: SCMFSA_2:64 for a, b being Int-Location for s being State of SCM+FSA holds ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds (Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) ) proofend; theorem Th65: :: SCMFSA_2:65 for a, b being Int-Location for s being State of SCM+FSA holds ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds (Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) ) proofend; theorem Th66: :: SCMFSA_2:66 for a, b being Int-Location for s being State of SCM+FSA holds ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds (Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) ) proofend; theorem Th67: :: SCMFSA_2:67 for a, b being Int-Location for s being State of SCM+FSA holds ( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds (Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) ) proofend; theorem :: SCMFSA_2:68 for a being Int-Location for s being State of SCM+FSA holds ( (Exec ((Divide (a,a)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds (Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) ) proofend; theorem Th69: :: SCMFSA_2:69 for l being Element of NAT for s being State of SCM+FSA holds ( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) ) proofend; theorem Th70: :: SCMFSA_2:70 for l being Element of NAT for a being Int-Location for s being State of SCM+FSA holds ( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) ) proofend; theorem Th71: :: SCMFSA_2:71 for l being Element of NAT for a being Int-Location for s being State of SCM+FSA holds ( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) ) proofend; theorem Th72: :: SCMFSA_2:72 for g being FinSeq-Location for c, a being Int-Location for s being State of SCM+FSA holds ( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st ( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds (Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) ) proofend; theorem Th73: :: SCMFSA_2:73 for g being FinSeq-Location for a, c being Int-Location for s being State of SCM+FSA holds ( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st ( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds (Exec (((g,a) := c),s)) . f = s . f ) ) proofend; theorem Th74: :: SCMFSA_2:74 for g being FinSeq-Location for c being Int-Location for s being State of SCM+FSA holds ( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds (Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) ) proofend; theorem Th75: :: SCMFSA_2:75 for g being FinSeq-Location for c being Int-Location for s being State of SCM+FSA holds ( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st ( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds (Exec ((g :=<0,...,0> c),s)) . f = s . f ) ) proofend; begin theorem :: SCMFSA_2:76 for s being State of SCM+FSA for S being SCM+FSA-State st S = s holds IC s = IC S by FUNCT_7:def_1, SCMFSA_1:5; theorem Th77: :: SCMFSA_2:77 for i being Instruction of SCM for I being Instruction of SCM+FSA st i = I & i is halting holds I is halting proofend; theorem Th78: :: SCMFSA_2:78 for I being Instruction of SCM+FSA st ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = succ (IC s) holds not I is halting proofend; registration let a, b be Int-Location; set s = the State of SCM+FSA; clustera := b -> non halting ; coherence not a := b is halting proofend; cluster AddTo (a,b) -> non halting ; coherence not AddTo (a,b) is halting proofend; cluster SubFrom (a,b) -> non halting ; coherence not SubFrom (a,b) is halting proofend; cluster MultBy (a,b) -> non halting ; coherence not MultBy (a,b) is halting proofend; cluster Divide (a,b) -> non halting ; coherence not Divide (a,b) is halting proofend; end; theorem :: SCMFSA_2:79 for a, b being Int-Location holds not a := b is halting ; theorem :: SCMFSA_2:80 for a, b being Int-Location holds not AddTo (a,b) is halting ; theorem :: SCMFSA_2:81 for a, b being Int-Location holds not SubFrom (a,b) is halting ; theorem :: SCMFSA_2:82 for a, b being Int-Location holds not MultBy (a,b) is halting ; theorem :: SCMFSA_2:83 for a, b being Int-Location holds not Divide (a,b) is halting ; registration let la be Element of NAT ; cluster goto la -> non halting ; coherence not goto la is halting proofend; end; theorem :: SCMFSA_2:84 for la being Element of NAT holds not goto la is halting ; registration let a be Int-Location; let la be Element of NAT ; set f = the_Values_of SCM+FSA; set s = the SCM+FSA-State; clustera =0_goto la -> non halting ; coherence not a =0_goto la is halting proofend; clustera >0_goto la -> non halting ; coherence not a >0_goto la is halting proofend; end; theorem :: SCMFSA_2:85 for la being Element of NAT for a being Int-Location holds not a =0_goto la is halting ; theorem :: SCMFSA_2:86 for la being Element of NAT for a being Int-Location holds not a >0_goto la is halting ; registration let c be Int-Location; let f be FinSeq-Location ; let a be Int-Location; set s = the State of SCM+FSA; clusterc := (f,a) -> non halting ; coherence not c := (f,a) is halting proofend; cluster(f,a) := c -> non halting ; coherence not (f,a) := c is halting proofend; end; theorem :: SCMFSA_2:87 for f being FinSeq-Location for c, a being Int-Location holds not c := (f,a) is halting ; theorem :: SCMFSA_2:88 for f being FinSeq-Location for a, c being Int-Location holds not (f,a) := c is halting ; registration let c be Int-Location; let f be FinSeq-Location ; set s = the State of SCM+FSA; clusterc :=len f -> non halting ; coherence not c :=len f is halting proofend; clusterf :=<0,...,0> c -> non halting ; coherence not f :=<0,...,0> c is halting proofend; end; theorem :: SCMFSA_2:89 for f being FinSeq-Location for c being Int-Location holds not c :=len f is halting ; theorem :: SCMFSA_2:90 for f being FinSeq-Location for c being Int-Location holds not f :=<0,...,0> c is halting ; theorem :: SCMFSA_2:91 for I being Instruction of SCM+FSA st I = [0,{},{}] holds I is halting by Th77, AMI_3:26; theorem Th92: :: SCMFSA_2:92 for I being Instruction of SCM+FSA st InsCode I = 0 holds I = [0,{},{}] proofend; theorem Th93: :: SCMFSA_2:93 for I being set holds ( I is Instruction of SCM+FSA iff ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) ) proofend; Lm1: for W being Instruction of SCM+FSA st W is halting holds W = [0,{},{}] proofend; registration cluster SCM+FSA -> strict halting ; coherence SCM+FSA is halting proofend; end; theorem Th94: :: SCMFSA_2:94 for I being Instruction of SCM+FSA st I is halting holds I = halt SCM+FSA by Lm1; theorem :: SCMFSA_2:95 for I being Instruction of SCM+FSA st InsCode I = 0 holds I = halt SCM+FSA by Th92; theorem Th96: :: SCMFSA_2:96 halt SCM = halt SCM+FSA ; theorem :: SCMFSA_2:97 canceled; theorem :: SCMFSA_2:98 for i being Instruction of SCM for I being Instruction of SCM+FSA st i = I & not i is halting holds not I is halting by Th94, Th96; theorem :: SCMFSA_2:99 for i, j being Nat holds fsloc i <> intloc j proofend; theorem Th100: :: SCMFSA_2:100 Data-Locations = Int-Locations \/ FinSeq-Locations proofend; theorem :: SCMFSA_2:101 for i, j being Nat st i <> j holds intloc i <> intloc j by AMI_3:10; theorem :: SCMFSA_2:102 for l being Element of NAT for a being Int-Location holds not a in dom (Start-At (l,SCM+FSA)) proofend; theorem :: SCMFSA_2:103 for l being Element of NAT for f being FinSeq-Location holds not f in dom (Start-At (l,SCM+FSA)) proofend; theorem :: SCMFSA_2:104 for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds s1 = s2 proofend; registration let f be FinSeq-Location ; let w be FinSequence of INT ; clusterf .--> w -> data-only for PartState of SCM+FSA; coherence for b1 being PartState of SCM+FSA st b1 = f .--> w holds b1 is data-only proofend; end; registration let x be Int-Location; let i be Integer; clusterx .--> i -> data-only for PartState of SCM+FSA; coherence for b1 being PartState of SCM+FSA st b1 = x .--> i holds b1 is data-only proofend; end; registration let a, b be Int-Location; clustera := b -> No-StopCode ; coherence a := b is No-StopCode proofend; end; registration let a, b be Int-Location; cluster AddTo (a,b) -> No-StopCode ; coherence AddTo (a,b) is No-StopCode proofend; end; registration let a, b be Int-Location; cluster SubFrom (a,b) -> No-StopCode ; coherence SubFrom (a,b) is No-StopCode proofend; end; registration let a, b be Int-Location; cluster MultBy (a,b) -> No-StopCode ; coherence MultBy (a,b) is No-StopCode proofend; end; registration let a, b be Int-Location; cluster Divide (a,b) -> No-StopCode ; coherence Divide (a,b) is No-StopCode proofend; end; registration let lb be Element of NAT ; cluster goto lb -> No-StopCode ; coherence goto lb is No-StopCode proofend; end; registration let lb be Element of NAT ; let a be Int-Location; clustera =0_goto lb -> No-StopCode ; coherence a =0_goto lb is No-StopCode proofend; end; registration let lb be Element of NAT ; let a be Int-Location; clustera >0_goto lb -> No-StopCode ; coherence a >0_goto lb is No-StopCode proofend; end; registration let fa be FinSeq-Location ; let a, c be Int-Location; clusterc := (fa,a) -> No-StopCode ; coherence c := (fa,a) is No-StopCode proofend; end; registration let fa be FinSeq-Location ; let a, c be Int-Location; cluster(fa,a) := c -> No-StopCode ; coherence (fa,a) := c is No-StopCode proofend; end; registration let fa be FinSeq-Location ; let a be Int-Location; clustera :=len fa -> No-StopCode ; coherence a :=len fa is No-StopCode proofend; end; registration let fa be FinSeq-Location ; let a be Int-Location; clusterfa :=<0,...,0> a -> No-StopCode ; coherence fa :=<0,...,0> a is No-StopCode proofend; end;