:: The { \bf SCM_FSA } computer :: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki :: :: Received February 7, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, STRUCT_0, AMI_1, RELAT_1, SCMFSA_1, FUNCT_7, XBOOLE_0, TARSKI, AMI_3, ZFMISC_1, SUBSET_1, CARD_1, CAT_1, ARYTM_1, ARYTM_3, NAT_1, FINSET_1, FUNCT_1, AMI_2, XXREAL_0, FINSEQ_1, GRAPHSP, FSM_1, FUNCT_4, FUNCOP_1, INT_1, CARD_3, COMPLEX1, PARTFUN1, FINSEQ_2, GLIB_000, SCMFSA_2, RECDEF_2, GOBRD13, MEMSTR_0, AMISTD_4, SCMPDS_5; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1, XCMPLX_0, XXREAL_0, INT_1, NAT_1, RELAT_1, MCART_1, CARD_1, CARD_3, INT_2, FINSEQ_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, FINSEQ_2, FUNCT_7, RECDEF_2, NUMBERS, MEMSTR_0, COMPOS_0, COMPOS_1, AMISTD_4, EXTPRO_1, SCM_INST, SCMFSA_I, AMI_2, AMI_3, SCMFSA_1; constructors WELLORD2, DOMAIN_1, REAL_1, FINSEQ_4, AMI_3, SCMFSA_1, RELSET_1, PRE_POLY, FUNCT_7, NAT_D, AMISTD_4, XTUPLE_0, XFAMILY; registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1, CARD_3, STRUCT_0, AMI_3, SCMFSA_1, FINSET_1, CARD_2, RELSET_1, EXTPRO_1, MEMSTR_0, COMPOS_0, SCM_INST, SCMFSA_I, XTUPLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: The SCM+FSA Computer reserve J,J1,K for Element of Segm 13, b,b1,b2,c,c1,c2 for Element of SCM+FSA-Data-Loc, f,f1,f2 for Element of SCM+FSA-Data*-Loc; definition func SCM+FSA -> strict AMI-Struct over Segm 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#); end; registration cluster SCM+FSA -> non empty with_non-empty_values; end; registration cluster SCM+FSA -> with_non_trivial_Instructions; end; theorem :: SCMFSA_2:1 IC SCM+FSA = NAT; begin :: The Memory Structure reserve k for Nat, J,K,L for Element of Segm 13, O,P,R for Element of Segm 9; notation synonym Int-Locations for SCM+FSA-Data-Loc; end; definition redefine func Int-Locations -> Subset of SCM+FSA; ::$CD func FinSeq-Locations -> Subset of SCM+FSA equals :: SCMFSA_2:def 3 SCM+FSA-Data*-Loc; end; registration cluster Int-like for Object of SCM+FSA; end; definition mode Int-Location is Int-like Object of SCM+FSA; ::$CD mode FinSeq-Location -> Object of SCM+FSA means :: SCMFSA_2:def 5 it in SCM+FSA-Data*-Loc; end; reserve da for Int-Location, fa for FinSeq-Location, x,y for set; ::$CT 5 definition let k be Nat; func intloc k -> Int-Location equals :: SCMFSA_2:def 6 dl.k; func fsloc k -> FinSeq-Location equals :: SCMFSA_2:def 7 -(k+1); end; 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 Nat st dl = intloc i; theorem :: SCMFSA_2:9 for fl being FinSeq-Location ex i being Nat st fl = fsloc i; registration cluster FinSeq-Locations -> infinite; end; theorem :: SCMFSA_2:10 for I being Int-Location holds I is Data-Location; theorem :: SCMFSA_2:11 for l being Int-Location holds Values l = INT; theorem :: SCMFSA_2:12 for l being FinSeq-Location holds Values l = INT*; reserve la,lb for Nat, La for Nat, i for Instruction of SCM+FSA, I for Instruction of SCM, l for Nat, LA,LB for Nat, dA,dB,dC,dD for Element of SCM+FSA-Data-Loc, DA,DB,DC for Element of SCM-Data-Loc, fA,fB,fC for Element of SCM+FSA-Data*-Loc, f,g for FinSeq-Location, A,B for Data-Location, a,b,c,db for Int-Location; begin :: The Instruction Structure ::$CT 2 theorem :: SCMFSA_2:15 for I being Instruction of SCM+FSA st InsCode I <= 8 holds I is Instruction of SCM; theorem :: SCMFSA_2:16 for I being Instruction of SCM+FSA holds InsCode I <= 12; theorem :: SCMFSA_2:17 for I being Instruction of SCM holds I is Instruction of SCM+FSA; definition let a,b; func a := b -> Instruction of SCM+FSA means :: SCMFSA_2:def 8 ex A,B st a = A & b = B & it = A:=B; func AddTo(a,b) -> Instruction of SCM+FSA means :: SCMFSA_2:def 9 ex A,B st a = A & b = B & it = AddTo(A,B); func SubFrom(a,b) -> Instruction of SCM+FSA means :: SCMFSA_2:def 10 ex A,B st a = A & b = B & it = SubFrom(A,B); func MultBy(a,b) -> Instruction of SCM+FSA means :: SCMFSA_2:def 11 ex A,B st a = A & b = B & it = MultBy(A,B); func Divide(a,b) -> Instruction of SCM+FSA means :: SCMFSA_2:def 12 ex A,B st a = A & b = B & it = Divide(A,B); end; definition let la be Nat; func goto la -> Instruction of SCM+FSA equals :: SCMFSA_2:def 13 SCM-goto la; let a; func a=0_goto la -> Instruction of SCM+FSA means :: SCMFSA_2:def 14 ex A st a = A & it = A=0_goto la; func a>0_goto la -> Instruction of SCM+FSA means :: SCMFSA_2:def 15 ex A st a = A & it = A>0_goto la; end; definition let c,i be Int-Location; let a be FinSeq-Location; func c:=(a,i) -> Instruction of SCM+FSA equals :: SCMFSA_2:def 16 [9,{},<*c,a,i*>]; func (a,i):=c -> Instruction of SCM+FSA equals :: SCMFSA_2:def 17 [10,{},<*c,a,i*>]; end; definition let i be Int-Location; let a be FinSeq-Location; func i:=len a -> Instruction of SCM+FSA equals :: SCMFSA_2:def 18 [11,{},<*i,a*>]; func a:=<0,...,0>i -> Instruction of SCM+FSA equals :: SCMFSA_2:def 19 [12,{},<*i,a*>]; end; theorem :: SCMFSA_2:18 InsCode (a:=b) = 1; theorem :: SCMFSA_2:19 InsCode (AddTo(a,b)) = 2; theorem :: SCMFSA_2:20 InsCode (SubFrom(a,b)) = 3; theorem :: SCMFSA_2:21 InsCode (MultBy(a,b)) = 4; theorem :: SCMFSA_2:22 InsCode (Divide(a,b)) = 5; theorem :: SCMFSA_2:23 InsCode (goto lb) = 6; theorem :: SCMFSA_2:24 InsCode (a=0_goto lb) = 7; theorem :: SCMFSA_2:25 InsCode (a>0_goto lb) = 8; theorem :: SCMFSA_2:26 InsCode (c:=(fa,a)) = 9; theorem :: SCMFSA_2:27 InsCode ((fa,a):=c) = 10; theorem :: SCMFSA_2:28 InsCode (a:=len fa) = 11; theorem :: SCMFSA_2:29 InsCode (fa:=<0,...,0>a) = 12; theorem :: SCMFSA_2:30 for ins being Instruction of SCM+FSA st InsCode ins = 1 holds ex da,db st ins = da:=db; theorem :: SCMFSA_2:31 for ins being Instruction of SCM+FSA st InsCode ins = 2 holds ex da,db st ins = AddTo(da,db); theorem :: SCMFSA_2:32 for ins being Instruction of SCM+FSA st InsCode ins = 3 holds ex da,db st ins = SubFrom(da,db); theorem :: SCMFSA_2:33 for ins being Instruction of SCM+FSA st InsCode ins = 4 holds ex da,db st ins = MultBy(da,db); theorem :: SCMFSA_2:34 for ins being Instruction of SCM+FSA st InsCode ins = 5 holds ex da,db st ins = Divide(da,db); theorem :: SCMFSA_2:35 for ins being Instruction of SCM+FSA st InsCode ins = 6 holds ex lb st ins = goto lb; theorem :: SCMFSA_2:36 for ins being Instruction of SCM+FSA st InsCode ins = 7 holds ex lb,da st ins = da=0_goto lb; theorem :: SCMFSA_2:37 for ins being Instruction of SCM+FSA st InsCode ins = 8 holds ex lb,da st ins = da>0_goto lb; theorem :: SCMFSA_2:38 for ins being Instruction of SCM+FSA st InsCode ins = 9 holds ex a,b,fa st ins = b:=(fa,a); theorem :: SCMFSA_2:39 for ins being Instruction of SCM+FSA st InsCode ins = 10 holds ex a,b,fa st ins = (fa,a):=b; theorem :: SCMFSA_2:40 for ins being Instruction of SCM+FSA st InsCode ins = 11 holds ex a,fa st ins = a:=len fa; theorem :: SCMFSA_2:41 for ins being Instruction of SCM+FSA st InsCode ins = 12 holds ex a,fa st ins = fa:=<0,...,0>a; begin :: Relationship to {\bf SCM} reserve S for State of SCM, s,s1 for State of SCM+FSA; theorem :: SCMFSA_2:42 for s being State of SCM+FSA, d being Int-Location holds d in dom s; theorem :: SCMFSA_2:43 f in dom s; theorem :: SCMFSA_2:44 not f in dom S; theorem :: SCMFSA_2:45 for s being State of SCM+FSA holds Int-Locations c= dom s; theorem :: SCMFSA_2:46 for s being State of SCM+FSA holds FinSeq-Locations c= dom s; theorem :: SCMFSA_2:47 for s being State of SCM+FSA holds dom (s|Int-Locations) = Int-Locations; theorem :: SCMFSA_2:48 for s being State of SCM+FSA holds dom (s|FinSeq-Locations) = FinSeq-Locations; theorem :: SCMFSA_2:49 for s being State of SCM+FSA, i being Instruction of SCM holds s|SCM-Memory is State of SCM; theorem :: SCMFSA_2:50 for s being State of SCM+FSA, s9 being State of SCM holds s +* s9 is State of SCM+FSA; theorem :: SCMFSA_2:51 for i being Instruction of SCM, ii being Instruction of SCM+FSA, s being State of SCM, ss being State of SCM+FSA st i = ii & s = ss|SCM-Memory holds Exec(ii,ss) = ss +* Exec(i,s); registration let s be State of SCM+FSA, d be Int-Location; cluster s.d -> integer; end; definition let s be State of SCM+FSA, d be FinSeq-Location; redefine func s.d -> FinSequence of INT; end; theorem :: SCMFSA_2:52 S = s|SCM-Memory implies s = s +* S; theorem :: SCMFSA_2:53 s1 = s +* S implies s1.IC SCM+FSA = S.IC SCM; theorem :: SCMFSA_2:54 s1 = s +* S & A = a implies S.A = s1.a; theorem :: SCMFSA_2:55 S = s|SCM-Memory & A = a implies S.A = s.a; registration cluster SCM+FSA -> IC-Ins-separated; end; theorem :: SCMFSA_2:56 for dl being Int-Location holds dl <> IC SCM+FSA; theorem :: SCMFSA_2:57 for dl being FinSeq-Location holds dl <> IC SCM+FSA; theorem :: SCMFSA_2:58 for il being Int-Location, dl being FinSeq-Location holds il <> dl; theorem :: SCMFSA_2:59 for il being Nat, dl being Int-Location holds il <> dl; theorem :: SCMFSA_2:60 for il being Nat, dl being FinSeq-Location holds il <> dl; 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; theorem :: SCMFSA_2:62 S = s|SCM-Memory implies IC s = IC S; begin :: Users guide theorem :: SCMFSA_2:63 Exec(a:=b, s).IC SCM+FSA = IC s + 1 & Exec(a:=b, s).a = s.b & ( for c st c <> a holds Exec(a:=b, s).c = s.c) & for f holds Exec(a:=b, s).f = s. f; theorem :: SCMFSA_2:64 Exec(AddTo(a,b), s).IC SCM+FSA = IC s + 1 & Exec(AddTo(a,b), s) .a = s.a + s.b & (for c st c <> a holds Exec(AddTo(a,b), s).c = s.c) & for f holds Exec(AddTo(a,b), s).f = s.f; theorem :: SCMFSA_2:65 Exec(SubFrom(a,b), s).IC SCM+FSA = IC s + 1 & Exec(SubFrom(a,b) , s).a = s.a - s.b & (for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c) & for f holds Exec(SubFrom(a,b), s).f = s.f; theorem :: SCMFSA_2:66 Exec(MultBy(a,b), s).IC SCM+FSA = IC s + 1 & Exec(MultBy(a,b), s).a = s.a * s.b & (for c st c <> a holds Exec(MultBy(a,b), s).c = s.c) & for f holds Exec(MultBy(a,b), s).f = s.f; theorem :: SCMFSA_2:67 Exec(Divide(a,b), s).IC SCM+FSA = IC s + 1 & (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 st c <> a & c <> b holds Exec(Divide(a,b), s).c = s.c) & for f holds Exec(Divide(a,b), s).f = s.f; theorem :: SCMFSA_2:68 Exec(Divide(a,a), s).IC SCM+FSA = IC s + 1 & Exec(Divide(a,a), s).a = s.a mod s.a & (for c st c <> a holds Exec(Divide(a,a), s).c = s.c) & for f holds Exec(Divide(a,a), s).f = s.f; theorem :: SCMFSA_2:69 Exec(goto l, s).IC SCM+FSA = l & (for c holds Exec(goto l, s).c = s.c) & for f holds Exec(goto l, s).f = s.f; theorem :: SCMFSA_2:70 (s.a = 0 implies Exec(a =0_goto l, s).IC SCM+FSA = l) & (s.a <> 0 implies Exec(a=0_goto l, s).IC SCM+FSA = IC s + 1) & (for c holds Exec(a =0_goto l, s).c = s.c) & for f holds Exec(a=0_goto l, s).f = s.f; theorem :: SCMFSA_2:71 (s.a > 0 implies Exec(a >0_goto l, s).IC SCM+FSA = l) & (s.a <= 0 implies Exec(a>0_goto l, s).IC SCM+FSA = IC s + 1) & (for c holds Exec(a >0_goto l, s).c = s.c) & for f holds Exec(a>0_goto l, s).f = s.f; theorem :: SCMFSA_2:72 Exec(c:=(g,a), s).IC SCM+FSA = IC s + 1 & (ex k st k = |.s.a.| & Exec(c:=(g,a), s).c = (s.g)/.k) & (for b st b <> c holds Exec(c:=(g,a), s).b = s.b) & for f holds Exec(c:=(g,a), s).f = s.f; theorem :: SCMFSA_2:73 Exec((g,a):=c, s).IC SCM+FSA = IC s + 1 & (ex k st k = |.s.a.| & Exec((g,a):=c, s).g = s.g+*(k,s.c)) & (for b holds Exec((g,a):=c, s).b = s.b) & for f st f <> g holds Exec((g,a):=c, s).f = s.f; theorem :: SCMFSA_2:74 Exec(c:=len g, s).IC SCM+FSA = IC s + 1 & Exec(c:=len g, s).c = len(s.g) & (for b st b <> c holds Exec(c:=len g, s).b = s.b) & for f holds Exec(c:=len g, s).f = s.f; theorem :: SCMFSA_2:75 Exec(g:=<0,...,0>c, s).IC SCM+FSA = IC s + 1 & (ex k st k = |.s.c.| & Exec(g:=<0,...,0>c, s).g = k |-> 0) & (for b holds Exec(g:=<0,...,0> c, s).b = s.b) & for f st f <> g holds Exec(g:=<0,...,0>c, s).f = s.f; begin :: Halt Instruction theorem :: SCMFSA_2:76 for S being SCM+FSA-State st S = s holds IC s = IC S; theorem :: SCMFSA_2:77 for i being Instruction of SCM, I being Instruction of SCM+FSA st i = I & i is halting holds I is halting; theorem :: SCMFSA_2:78 for I being Instruction of SCM+FSA st ex s st Exec(I,s).IC SCM+FSA = IC s + 1 holds I is non halting; registration let a,b; cluster a := b -> non halting; cluster AddTo(a,b) -> non halting; cluster SubFrom(a,b) -> non halting; cluster MultBy(a,b) -> non halting; cluster Divide(a,b) -> non halting; end; theorem :: SCMFSA_2:79 a := b is non halting; theorem :: SCMFSA_2:80 AddTo(a,b) is non halting; theorem :: SCMFSA_2:81 SubFrom(a,b) is non halting; theorem :: SCMFSA_2:82 MultBy(a,b) is non halting; theorem :: SCMFSA_2:83 Divide(a,b) is non halting; registration let la; cluster goto la -> non halting; end; theorem :: SCMFSA_2:84 goto la is non halting; registration let a,la; cluster a=0_goto la -> non halting; cluster a>0_goto la -> non halting; end; theorem :: SCMFSA_2:85 a=0_goto la is non halting; theorem :: SCMFSA_2:86 a>0_goto la is non halting; registration let c,f,a; cluster c:=(f,a) -> non halting; cluster (f,a):=c -> non halting; end; theorem :: SCMFSA_2:87 c:=(f,a) is non halting; theorem :: SCMFSA_2:88 (f,a):=c is non halting; registration let c,f; cluster c:=len f -> non halting; cluster f:=<0,...,0>c -> non halting; end; theorem :: SCMFSA_2:89 c:=len f is non halting; theorem :: SCMFSA_2:90 f:=<0,...,0>c is non halting; theorem :: SCMFSA_2:91 for I being Instruction of SCM+FSA st I = [0,{},{}] holds I is halting; theorem :: SCMFSA_2:92 for I be Instruction of SCM+FSA st InsCode I = 0 holds I = [0,{},{}]; theorem :: SCMFSA_2:93 for I being set holds I is Instruction of SCM+FSA iff I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or (ex a,b st I = Divide(a,b)) or (ex la st I = goto la) or (ex lb,da st I = da=0_goto lb) or (ex lb,da st I = da>0_goto lb) or (ex b,a,fa st I = a:=(fa,b)) or (ex a,b,fa st I = (fa,a):=b) or (ex a,f st I = a:=len f) or ex a,f st I = f:=<0,...,0>a; registration cluster SCM+FSA -> halting; end; theorem :: SCMFSA_2:94 for I being Instruction of SCM+FSA st I is halting holds I = halt SCM+FSA; theorem :: SCMFSA_2:95 for I being Instruction of SCM+FSA st InsCode I = 0 holds I = halt SCM+FSA; theorem :: SCMFSA_2:96 halt SCM = halt SCM+FSA; ::$CT theorem :: SCMFSA_2:98 for i being Instruction of SCM, I being Instruction of SCM+FSA st i = I & i is non halting holds I is non halting; theorem :: SCMFSA_2:99 for i,j being Nat holds fsloc i <> intloc j; theorem :: SCMFSA_2:100 Data-Locations SCM+FSA = Int-Locations \/ FinSeq-Locations; theorem :: SCMFSA_2:101 for i,j being Nat st i <> j holds intloc i <> intloc j; reserve n for Nat, I for Program of SCM+FSA; theorem :: SCMFSA_2:102 not a in dom Start-At(l,SCM+FSA); theorem :: SCMFSA_2:103 not f in dom Start-At(l,SCM+FSA); 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; registration let f be FinSeq-Location, w be FinSequence of INT; cluster f .--> w -> data-only for PartState of SCM+FSA; end; registration let x be Int-Location, i be Integer; cluster x .--> i -> data-only for PartState of SCM+FSA; end; registration let a,b; cluster a:=b -> No-StopCode; end; registration let a,b; cluster AddTo(a,b) -> No-StopCode; end; registration let a,b; cluster SubFrom(a,b) -> No-StopCode; end; registration let a,b; cluster MultBy(a,b) -> No-StopCode; end; registration let a,b; cluster Divide(a,b) -> No-StopCode; end; registration let lb; cluster goto lb -> No-StopCode; end; registration let lb,a; cluster a=0_goto lb -> No-StopCode; end; registration let lb,a; cluster a>0_goto lb -> No-StopCode; end; registration let fa,a,c; cluster c:= (fa,a) -> No-StopCode; end; registration let fa,a,c; cluster (fa,a):=c -> No-StopCode; end; registration let fa,a; cluster a:=len fa -> No-StopCode; end; registration let fa,a; cluster fa:=<0,...,0>a -> No-StopCode; end;