:: On the Decomposition of the States of SCM
::  by Yasushi Tanaka
::
:: Received November 23, 1993
:: Copyright (c) 1993 Association of Mizar Users

environ

 vocabularies BOOLE, NAT_1, ARYTM_1, FUNCT_1, RELAT_1, FUNCT_4, AMI_3, AMI_1,
      AMI_2, GR_CY_1, FINSEQ_1, FINSET_1, TARSKI, CAT_1, FUNCOP_1, MCART_1,
      ORDINAL2, QC_LANG1, AMI_4, AMI_5, INT_1, ARYTM;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, XCMPLX_0, ZFMISC_1,
      MCART_1, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1, STRUCT_0,
      FINSET_1, FINSEQ_1, AMI_1, SCMNORM, AMI_2, AMI_3, AMI_4, XXREAL_0;
 constructors DOMAIN_1, XXREAL_0, NAT_1, FINSEQ_4, AMI_4;
 registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FRAENKEL,
      NUMBERS, XREAL_0, INT_1, FINSEQ_1, CARD_3, AMI_1, AMI_2, AMI_3, FINSET_1,
      CARD_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

canceled 17;

reserve x,y for set;

theorem :: AMI_5:18
  for dl being Data-Location ex i being Element of NAT st dl = dl.i;

canceled;

theorem :: AMI_5:20
  for dl being Data-Location holds dl <> IC SCM;

canceled;

theorem :: AMI_5:22
  for il being Instruction-Location of SCM, dl being Data-Location holds
  il <> dl;

reserve i, j, k for Element of NAT;

theorem :: AMI_5:23
  the carrier of SCM = {IC SCM} \/ SCM-Data-Loc \/ NAT;

theorem :: AMI_5:24
  for s being State of SCM, d being Data-Location,
  l being Instruction-Location of SCM holds d in dom s & l in dom s;

canceled;

theorem :: AMI_5:26
  for s1,s2 being State of SCM st IC(s1) = IC(s2) &
  (for a being Data-Location holds s1.a = s2.a) &
  (for i being Instruction-Location of SCM holds s1.i = s2.i) holds s1 = s2;

theorem :: AMI_5:27
  for s being State of SCM holds SCM-Data-Loc c= dom s;

theorem :: AMI_5:28
  for s being State of SCM holds NAT c= dom s;

theorem :: AMI_5:29
  for s being State of SCM holds dom (s|SCM-Data-Loc) = SCM-Data-Loc;

theorem :: AMI_5:30
  for s being State of SCM holds dom (s|NAT) = NAT;

theorem :: AMI_5:31
  SCM-Data-Loc is not finite;

theorem :: AMI_5:32
  NAT is not finite;

registration
  cluster SCM-Data-Loc -> infinite;
end;

registration
  let I be Instruction of SCM;
  cluster InsCode I -> natural;
end;

definition
  canceled;
  let I be Instruction of SCM;
  func @I -> Element of SCM-Instr equals
:: AMI_5:def 2

  I;
end;

definition
  let loc be Element of NAT;
  func loc@ -> Instruction-Location of SCM equals
:: AMI_5:def 3

  loc;
end;

definition
  let loc be Element of SCM-Data-Loc;
  func loc@ -> Data-Location equals
:: AMI_5:def 4

  loc;
end;

reserve I,J,K for Element of Segm 9,
  a,a1 for Element of NAT,
  b,b1,c for Element of SCM-Data-Loc;

canceled 3;

theorem :: AMI_5:36
  for l being Instruction of SCM holds InsCode(l) <= 8;

reserve a, b for Data-Location,
  loc for Instruction-Location of SCM;

theorem :: AMI_5:37
  InsCode (halt SCM) = 0;

reserve I,J,K for Element of Segm 9,
  a,a1 for Element of NAT,
  b,b1,c for Element of SCM-Data-Loc,
  da,db for Data-Location,
  loc for Instruction-Location of SCM;

canceled 8;

theorem :: AMI_5:46
  for ins being Instruction of SCM st InsCode ins = 0 holds ins = halt SCM;

theorem :: AMI_5:47
  for ins being Instruction of SCM st InsCode ins = 1
  holds ex da,db st ins = da:=db;

theorem :: AMI_5:48
  for ins being Instruction of SCM st InsCode ins = 2
  holds ex da,db st ins = AddTo(da,db);

theorem :: AMI_5:49
  for ins being Instruction of SCM st InsCode ins = 3
  holds ex da,db st ins = SubFrom(da,db);

theorem :: AMI_5:50
  for ins being Instruction of SCM st InsCode ins = 4
  holds ex da,db st ins = MultBy(da,db);

theorem :: AMI_5:51
  for ins being Instruction of SCM st InsCode ins = 5
  holds ex da,db st ins = Divide(da,db);

theorem :: AMI_5:52
  for ins being Instruction of SCM st InsCode ins = 6
  holds ex loc st ins = goto loc;

theorem :: AMI_5:53
  for ins being Instruction of SCM st InsCode ins = 7
  holds ex loc,da st ins = da=0_goto loc;

theorem :: AMI_5:54
  for ins being Instruction of SCM st InsCode ins = 8
  holds ex loc,da st ins = da>0_goto loc;

theorem :: AMI_5:55
  for loc being Instruction-Location of SCM
  holds (@(goto loc)) jump_address = loc;

theorem :: AMI_5:56
  for loc being Instruction-Location of SCM, a being Data-Location
  holds (@(a=0_goto loc)) cjump_address = loc &
  (@(a=0_goto loc)) cond_address = a;

theorem :: AMI_5:57
  for loc being Instruction-Location of SCM, a being Data-Location
  holds (@(a>0_goto loc)) cjump_address = loc &
  (@(a>0_goto loc)) cond_address = a;

theorem :: AMI_5:58
  for s1,s2 being State of SCM st
  (s1 | (SCM-Data-Loc \/ {IC SCM})) = (s2 | (SCM-Data-Loc \/ {IC SCM}))
  for l being Instruction of SCM holds
  Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM})
  = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM});

theorem :: AMI_5:59
  for i being Instruction of SCM, s being State of SCM holds
  Exec (i, s) | NAT = s | NAT;

begin

canceled 9;

theorem :: AMI_5:69
  for p being FinPartState of SCM holds dom DataPart p c= SCM-Data-Loc;

canceled 7;

theorem :: AMI_5:77
  for i being Instruction of SCM, s being State of SCM,
  p being programmed FinPartState of SCM holds
  Exec (i, s +* p) = Exec (i,s) +* p;

canceled 2;

theorem :: AMI_5:80
  for s being State of SCM, iloc being Instruction-Location of SCM,
  a being Data-Location holds s.a = (s +* Start-At iloc).a;

begin :: Autonomic finite partial states of SCM

canceled 2;

theorem :: AMI_5:83
  for p being autonomic FinPartState of SCM st DataPart p <> {}
  holds IC SCM in dom p;

registration
  cluster autonomic non programmed FinPartState of SCM;
end;

theorem :: AMI_5:84
  for p being autonomic non programmed FinPartState of SCM holds
  IC SCM in dom p;

theorem :: AMI_5:85
  for p being autonomic FinPartState of SCM st IC SCM in dom p
  holds IC p in dom p;

theorem :: AMI_5:86
  for p being autonomic non programmed FinPartState of SCM,
  s being State of SCM st p c= s for i being Element of NAT
  holds IC  Computation(s,i) in dom ProgramPart(p);

theorem :: AMI_5:87
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  I being Instruction of SCM st I = CurInstr ( Computation(s1,i))
  holds IC  Computation(s1,i) = IC  Computation(s2,i) &
  I = CurInstr ( Computation(s2,i));

theorem :: AMI_5:88
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da, db being Data-Location, I being Instruction of SCM
  st I = CurInstr ( Computation(s1,i)) holds I = da := db & da in dom p
  implies  Computation(s1,i).db =  Computation(s2,i).db;

theorem :: AMI_5:89
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da, db being Data-Location, I being Instruction of SCM
  st I = CurInstr ( Computation(s1,i)) holds I = AddTo(da, db) & da in dom p
  implies  Computation(s1,i).da +  Computation(s1,i).db
  =  Computation(s2,i).da +  Computation(s2,i).db;

theorem :: AMI_5:90
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da, db being Data-Location, I being Instruction of SCM
  st I = CurInstr ( Computation(s1,i)) holds I = SubFrom(da, db) & da in dom p
  implies  Computation(s1,i).da -  Computation(s1,i).db
  =  Computation(s2,i).da -  Computation(s2,i).db;

theorem :: AMI_5:91
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da, db being Data-Location, I being Instruction of SCM
  st I = CurInstr ( Computation(s1,i)) holds I = MultBy(da, db) & da in dom p
  implies  Computation(s1,i).da *  Computation(s1,i).db
  =  Computation(s2,i).da *  Computation(s2,i).db;

theorem :: AMI_5:92
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da, db being Data-Location, I being Instruction of SCM
  st I = CurInstr ( Computation(s1,i))
  holds I = Divide(da, db) & da in dom p & da <> db
  implies  Computation(s1,i).da div  Computation(s1,i).db
  =  Computation(s2,i).da div  Computation(s2,i).db;

theorem :: AMI_5:93
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da, db being Data-Location, I being Instruction of SCM
  st I = CurInstr ( Computation(s1,i))
  holds I = Divide(da, db) & db in dom p & da <> db
  implies  Computation(s1,i).da mod  Computation(s1,i).db
  =  Computation(s2,i).da mod  Computation(s2,i).db;

theorem :: AMI_5:94
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da being Data-Location, loc being Instruction-Location of SCM,
  I being Instruction of SCM st I = CurInstr ( Computation(s1,i))
  holds I = da=0_goto loc & loc <> Next (IC  Computation(s1,i))
  implies ( Computation(s1,i).da = 0 iff  Computation(s2,i).da = 0);

theorem :: AMI_5:95
  for p being autonomic non programmed FinPartState of SCM,
  s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT,
  da being Data-Location, loc being Instruction-Location of SCM,
  I being Instruction of SCM st I = CurInstr ( Computation(s1,i))
  holds I = da>0_goto loc & loc <> Next (IC  Computation(s1,i))
  implies ( Computation(s1,i).da > 0 iff  Computation(s2,i).da > 0);

theorem :: AMI_5:96
  for p being FinPartState of SCM holds DataPart p = p | SCM-Data-Loc;

theorem :: AMI_5:97
  for f being FinPartState of SCM holds
  f is data-only iff dom f c= SCM-Data-Loc;