:: On the Instructions of { \bf SCM+FSA } :: by Artur Korni{\l}owicz :: :: Received May 8, 2001 :: Copyright (c) 2001-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, SCMFSA_2, AMI_3, AMI_1, FSM_1, INT_1, FUNCOP_1, SUBSET_1, SCMFSA_1, CAT_1, XBOOLE_0, GRAPHSP, FINSEQ_1, RELAT_1, CARD_1, AMI_2, AMISTD_2, CARD_3, FUNCT_1, AMISTD_1, CIRCUIT2, FUNCT_4, SETFAM_1, XXREAL_0, TARSKI, ARYTM_3, GOBOARD5, FRECHET, ARYTM_1, COMPLEX1, PARTFUN1, FINSEQ_2, RECDEF_2, NAT_1, COMPOS_1, GOBRD13, MEMSTR_0; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, ORDINAL1, XCMPLX_0, INT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FUNCT_4, FUNCT_7, COMPLEX1, CARD_1, CARD_3, XXREAL_0, NAT_1, RECDEF_2, VALUED_1, NUMBERS, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, AMI_3, SCM_INST, SCMFSA_1, SCMFSA_3, SCMFSA_2; constructors REAL_1, NAT_D, AMI_3, SCMFSA_3, AMISTD_2, RELSET_1, AMISTD_1, SCMFSA_1, PRE_POLY, FUNCT_7, DOMAIN_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, NUMBERS, XREAL_0, NAT_1, INT_1, SCMFSA_2, AMISTD_2, CARD_3, FUNCT_4, VALUED_0, EXTPRO_1, FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0, FINSEQ_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve a, b, d1, d2, d3, d4 for Int-Location, A, B for Data-Location, f, f1, f2, f3 for FinSeq-Location, il, i1, i2 for Nat, L for Nat, I for Instruction of SCM+FSA, s,s1,s2 for State of SCM+FSA, T for InsType of the InstructionsF of SCM+FSA, k for Nat; definition let la, lb be Int-Location, a, b be Integer; redefine func (la,lb) --> (a,b) -> PartState of SCM+FSA; end; theorem :: SCMFSA10:1 for o being Object of SCM+FSA st o in Data-Locations SCM+FSA holds o is Int-Location or o is FinSeq-Location; theorem :: SCMFSA10:2 a := b = [1,{},<*a,b*>]; theorem :: SCMFSA10:3 AddTo(a,b) = [2,{},<*a,b*>]; theorem :: SCMFSA10:4 SubFrom(a,b) = [3,{},<* a,b *>]; theorem :: SCMFSA10:5 MultBy(a,b) = [4,{},<* a,b *>]; theorem :: SCMFSA10:6 Divide(a,b) = [5,{},<* a,b *>]; theorem :: SCMFSA10:7 a=0_goto il = [7, <* il*>,<*a *>]; theorem :: SCMFSA10:8 a>0_goto il = [8, <* il*>,<*a *>]; reserve J,K for Element of Segm 13, b,b1,c,c1 for Element of SCM-Data-Loc, f,f1 for Element of SCM+FSA-Data*-Loc; theorem :: SCMFSA10:9 JumpPart halt SCM+FSA = {}; reserve a, b, d1, d2, d3, d4 for Int-Location, A, B for Data-Location, f, f1, f2, f3 for FinSeq-Location; theorem :: SCMFSA10:10 JumpPart (a:=b) = {}; theorem :: SCMFSA10:11 JumpPart AddTo(a,b) = {}; theorem :: SCMFSA10:12 JumpPart SubFrom(a,b) = {}; theorem :: SCMFSA10:13 JumpPart MultBy(a,b) = {}; theorem :: SCMFSA10:14 JumpPart Divide(a,b) = {}; theorem :: SCMFSA10:15 JumpPart (a=0_goto i1) = <*i1*>; theorem :: SCMFSA10:16 JumpPart (a>0_goto i1) = <*i1*>; theorem :: SCMFSA10:17 T = 0 implies JumpParts T = {0}; theorem :: SCMFSA10:18 T = 1 implies JumpParts T = {{}}; theorem :: SCMFSA10:19 T = 2 implies JumpParts T = {{}}; theorem :: SCMFSA10:20 T = 3 implies JumpParts T = {{}}; theorem :: SCMFSA10:21 T = 4 implies JumpParts T = {{}}; theorem :: SCMFSA10:22 T = 5 implies JumpParts T = {{}}; theorem :: SCMFSA10:23 T = 6 implies dom product" JumpParts T = {1}; theorem :: SCMFSA10:24 T = 7 implies dom product" JumpParts T = {1}; theorem :: SCMFSA10:25 T = 8 implies dom product" JumpParts T = {1}; theorem :: SCMFSA10:26 T = 9 implies JumpParts T = {{}}; theorem :: SCMFSA10:27 T = 10 implies JumpParts T = {{}}; theorem :: SCMFSA10:28 T = 11 implies JumpParts T = {{}}; theorem :: SCMFSA10:29 T = 12 implies JumpParts T = {{}}; theorem :: SCMFSA10:30 (product" JumpParts InsCode goto i1).1 = NAT; theorem :: SCMFSA10:31 (product" JumpParts InsCode (a =0_goto i1)).1 = NAT; theorem :: SCMFSA10:32 (product" JumpParts InsCode (a >0_goto i1)).1 = NAT; registration cluster JUMP halt SCM+FSA -> empty; end; registration let a, b; cluster a:=b -> sequential; cluster AddTo(a,b) -> sequential; cluster SubFrom(a,b) -> sequential; cluster MultBy(a,b) -> sequential; cluster Divide(a,b) -> sequential; end; registration let a, b; cluster JUMP (a := b) -> empty; cluster JUMP AddTo(a, b) -> empty; cluster JUMP SubFrom(a, b) -> empty; cluster JUMP MultBy(a,b) -> empty; cluster JUMP Divide(a,b) -> empty; end; theorem :: SCMFSA10:33 NIC(goto i1, il) = {i1}; theorem :: SCMFSA10:34 JUMP goto i1 = {i1}; registration let i1; cluster JUMP goto i1 -> 1-element; end; theorem :: SCMFSA10:35 NIC(a=0_goto i1, il) = {i1, il + 1}; theorem :: SCMFSA10:36 JUMP (a=0_goto i1) = {i1}; registration let a, i1; cluster JUMP (a =0_goto i1) -> 1-element; end; theorem :: SCMFSA10:37 NIC(a>0_goto i1, il) = {i1, il + 1}; theorem :: SCMFSA10:38 JUMP (a>0_goto i1) = {i1}; registration let a, i1; cluster JUMP (a >0_goto i1) -> 1-element; end; registration let a, b, f; cluster a:=(f,b) -> sequential; end; registration let a, b, f; cluster JUMP (a:=(f,b)) -> empty; end; registration let a, b, f; cluster (f,b):=a -> sequential; end; registration let a, b, f; cluster JUMP ((f,b):=a) -> empty; end; registration let a, f; cluster a:=len f -> sequential; end; registration let a, f; cluster JUMP (a:=len f) -> empty; end; registration let a, f; cluster f:=<0,...,0>a -> sequential; end; registration let a, f; cluster JUMP (f:=<0,...,0>a) -> empty; end; theorem :: SCMFSA10:39 SUCC(il,SCM+FSA) = {il, il + 1}; theorem :: SCMFSA10:40 for k being Nat holds k+1 in SUCC(k,SCM+FSA) & for j being Nat st j in SUCC(k,SCM+FSA) holds k <= j; registration cluster SCM+FSA -> standard; end; registration cluster InsCode halt SCM+FSA -> jump-only for InsType of the InstructionsF of SCM+FSA; end; registration cluster halt SCM+FSA -> jump-only; end; registration let i1; cluster InsCode goto i1 -> jump-only for InsType of the InstructionsF of SCM+FSA; end; registration let i1; cluster goto i1 -> jump-only non sequential non ins-loc-free; end; registration let a, i1; cluster InsCode (a =0_goto i1) -> jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode (a >0_goto i1) -> jump-only for InsType of the InstructionsF of SCM+FSA; end; registration let a, i1; cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free; cluster a >0_goto i1 -> jump-only non sequential non ins-loc-free; end; registration let a, b; cluster InsCode (a:=b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode AddTo(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode SubFrom(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode MultBy(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode Divide(a,b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; end; registration let a, b, f; cluster InsCode (b:=(f,a)) -> non jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode ((f,a):=b) -> non jump-only for InsType of the InstructionsF of SCM+FSA; end; registration let a, b, f; cluster b:=(f,a) -> non jump-only; cluster (f,a):=b -> non jump-only; end; registration let a, f; cluster InsCode (a:=len f) -> non jump-only for InsType of the InstructionsF of SCM+FSA; cluster InsCode (f:=<0,...,0>a) -> non jump-only for InsType of the InstructionsF of SCM+FSA; end; registration let a, f; cluster a:=len f -> non jump-only; cluster f:=<0,...,0>a -> non jump-only; end; registration cluster SCM+FSA -> with_explicit_jumps; end; theorem :: SCMFSA10:41 IncAddr(goto i1,k) = goto (i1+ k); theorem :: SCMFSA10:42 IncAddr(a=0_goto i1,k) = a=0_goto (i1+k); theorem :: SCMFSA10:43 IncAddr(a>0_goto i1,k) = a>0_goto (i1+k); registration cluster SCM+FSA -> IC-relocable; end;