:: Computation in { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 7, 1996
:: Copyright (c) 1996-2016 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, SUBSET_1, SCMFSA_2, AMI_1, RELAT_1, AMI_3, FSM_1,
STRUCT_0, FUNCT_4, FUNCOP_1, XBOOLE_0, TARSKI, FUNCT_1, XXREAL_0,
ARYTM_3, GRAPHSP, EXTPRO_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2,
CARD_1, INT_1, CIRCUIT2, ARYTM_1, AMISTD_5, FINSET_1, COMPOS_1, GOBRD13,
NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
INT_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1, NAT_1, STRUCT_0,
FUNCOP_1, FINSEQ_1, FINSEQ_2, MEMSTR_0, COMPOS_1, EXTPRO_1, FUNCT_7,
SCMFSA_2, XXREAL_0, AMISTD_5;
constructors DOMAIN_1, INT_2, AMI_3, SCMFSA_2, RELSET_1, PRE_POLY, SCMFSA_1,
AMISTD_5, FUNCT_7;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0,
AMI_3, SCMFSA_2, FINSET_1, ORDINAL1, COMPOS_1, EXTPRO_1, CARD_1,
MEMSTR_0, FUNCT_4, FUNCOP_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Finite partial states of SCM+FSA
::$CT 2
reserve k for Nat,
da,db for Int-Location,
fa for FinSeq-Location;
theorem :: SCMFSA_3:3
for s being State of SCM+FSA, iloc being Nat
, a being Int-Location holds s.a = (s +* Start-At(iloc,SCM+FSA)).a;
theorem :: SCMFSA_3:4
for s being State of SCM+FSA, iloc being Nat
, a being FinSeq-Location holds s.a = (s +* Start-At(iloc,SCM+FSA)).a;
begin :: Autonomic finite partial states of SCM+FSA
definition
let la be Int-Location;
let a be Integer;
redefine func la .--> a -> FinPartState of SCM+FSA;
end;
registration
cluster SCM+FSA -> IC-recognized;
end;
registration
cluster SCM+FSA -> CurIns-recognized;
end;
theorem :: SCMFSA_3:5
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,i)) = da := db & da in dom p
holds Comput(P1,s1,i).db = Comput(P2,s2,i).db;
theorem :: SCMFSA_3:6
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,i)) = AddTo(da, db)
& da in dom
p holds Comput(P1,s1,i).da + Comput(P1,s1,i).db =
Comput(P2,s2,i).da + Comput(P2,s2,i).db;
theorem :: SCMFSA_3:7
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,
i)) = SubFrom(da, db)
& da in
dom p holds Comput(P1,s1,i).da - Comput(P1,s1,i).db =
Comput(P2,s2,i).da
- Comput(P2,s2,i).db;
theorem :: SCMFSA_3:8
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,
i)) = MultBy(da, db)
& da in
dom p holds Comput(P1,s1,i).da * Comput(P1,s1,i).db =
Comput(P2,s2,i).da
* Comput(P2,s2,i).db;
theorem :: SCMFSA_3:9
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,
i)) = Divide(da, db)
& da in
dom p & da <> db holds Comput(P1,s1,i).da div
Comput(P1,s1,i).db =
Comput(P2,s2,i).da div Comput(P2,s2,i).db;
theorem :: SCMFSA_3:10
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location st
CurInstr(P1,Comput(P1,s1,i)) = Divide(da, db)
& db in
dom p holds Comput(P1,s1,i).da mod Comput(P1,s1,i).db
= Comput(P2,s2,i).
da mod Comput(P2,s2,i).db;
theorem :: SCMFSA_3:11
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da being Int-Location, loc being Nat st
CurInstr(P1,Comput(P1,s1,i)) = da=0_goto loc &
loc <> (IC Comput(P1,s1,i))+1 holds (
Comput(P1,s1,i).da = 0 iff Comput(P2,s2,i).da = 0);
theorem :: SCMFSA_3:12
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da being Int-Location, loc being Nat st
CurInstr(P1,Comput(P1,s1,i)) = da>0_goto loc &
loc <> (IC Comput(P1,s1,i))+1 holds
Comput(P1,s1,i).da > 0 iff Comput(P2,s2,i).da > 0;
theorem :: SCMFSA_3:13
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)
) =
da := (f,db) & da in dom p for k1,k2 being Element of NAT st k1 = |.
Comput(P1,s1,i).db.| & k2 = |. Comput(P2,s2,i).db.|
holds ( Comput(P1,s1,
i).f)/.k1 = ( Comput(P2,s2,i).f)/.k2;
theorem :: SCMFSA_3:14
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da, db being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)
) =
(f,db):=da & f in dom p for k1,k2 being Nat st k1 = |. Comput(
P1,s1,i).db.| & k2 = |. Comput(P2,s2,i).db.| holds
Comput(P1,s1,i).f+*(k1,
Comput(P1,s1,i).da) = Comput(P2,s2,i).f+*(k2,
Comput(P2,s2,i).da);
theorem :: SCMFSA_3:15
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da
being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)) =
da :=len f & da in dom p holds len( Comput(P1,s1,i).f)
= len(Comput(P2,s2,i).f);
theorem :: SCMFSA_3:16
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM+FSA,
s1, s2
being State of SCM+FSA st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
st q c= P1 & q c= P2
for i being Nat, da being Int-Location, f being FinSeq-Location st
CurInstr(P1,Comput(P1,s1,i)) =
f:=<0,...,0>da & f in dom p for k1,k2 being Nat st k1 = |.
Comput(P1,s1,i).da.| & k2 = |. Comput(P2,s2,i).da.|
holds k1 |-> 0 = k2 |-> 0;