:: Computation in { \bf SCM_FSA }
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: 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, 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,
      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;