:: SCMPDS Is Not Standard
::  by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 27, 2003
:: Copyright (c) 2003-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, SCMPDS_2, AMI_1, INT_1, FUNCOP_1, SUBSET_1, FSM_1,
      FUNCT_1, AMISTD_1, FUNCT_4, XBOOLE_0, SETFAM_1, AMI_3, COMPLEX1, ARYTM_3,
      XXREAL_0, ARYTM_1, CARD_1, AMI_2, RELAT_1, GRAPHSP, TARSKI, FINSET_1,
      CARD_3, AMI_WSTD, NAT_1, GOBRD13, MEMSTR_0, REAL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, CARD_3, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, INT_1, NAT_1, FINSET_1, COMPLEX1,
      INT_2, RELAT_1, FUNCT_4, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2,
      SCMPDS_3, AMISTD_1, AMI_WSTD;
 constructors REAL_1, NAT_D, SCMPDS_1, SCMPDS_3, AMI_WSTD, PRE_POLY, AMISTD_1,
      FUNCT_4, FUNCT_7;
 registrations XREAL_0, NAT_1, INT_1, CARD_3, SCMPDS_2, FUNCT_1, FUNCT_4,
      MEMSTR_0, AMI_3, ORDINAL1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin

reserve a, b for Int_position,
  i for Instruction of SCMPDS,
  l for Element of NAT,
  k, k1, k2 for Integer;

definition
  let la, lb be Int_position, a, b be Integer;
  redefine func (la,lb) --> (a,b) -> PartState of SCMPDS;
end;

registration
  let k;
  cluster JUMP (goto k) -> empty;
end;

theorem :: SCMPDS_9:1
  (for s being State of SCMPDS st IC s = l
   holds Exec(i,s).IC SCMPDS = IC s + 1) implies NIC(i, l) = {l + 1};

theorem :: SCMPDS_9:2
  (for l being Element of NAT holds NIC(i,l)={l+1}) implies JUMP i is empty;

theorem :: SCMPDS_9:3
  NIC(goto k,l) = { |.k+l.| };

theorem :: SCMPDS_9:4
  NIC(return a,l) = {k where k is Nat: k > 1};

theorem :: SCMPDS_9:5
  NIC(saveIC(a,k1), l) = {l+1};

theorem :: SCMPDS_9:6
  NIC(a:=k1, l) = {l+1};

theorem :: SCMPDS_9:7
  NIC((a,k1):=k2, l) = {l+1};

theorem :: SCMPDS_9:8
  NIC((a,k1):=(b,k2), l) = {l+1};

theorem :: SCMPDS_9:9
  NIC(AddTo(a,k1,k2), l) = {l+1};

theorem :: SCMPDS_9:10
  NIC(AddTo(a,k1,b,k2), l) = {l+1};

theorem :: SCMPDS_9:11
  NIC(SubFrom(a,k1,b,k2), l) = {l+1};

theorem :: SCMPDS_9:12
  NIC(MultBy(a,k1,b,k2), l) = {l+1};

theorem :: SCMPDS_9:13
  NIC(Divide(a,k1,b,k2), l) = {l+1};

theorem :: SCMPDS_9:14
  NIC((a,k1)<>0_goto k2,l) = { l+1, |. (k2+ l) .| };

theorem :: SCMPDS_9:15
  NIC((a,k1)<=0_goto k2,l) = { l+1, |. (k2+ l) .| };

theorem :: SCMPDS_9:16
  NIC((a,k1)>=0_goto k2,l) = { l+1, |. (k2+ l) .| };

theorem :: SCMPDS_9:17
  JUMP (return a) = {k where k is Nat: k > 1};

registration
  let a;
  cluster JUMP (return a) -> infinite;
end;

registration
  let a,k1;
  cluster JUMP (saveIC(a,k1)) -> empty;
end;

registration
  let a,k1;
  cluster JUMP (a:=k1) -> empty;
end;

registration
  let a,k1,k2;
  cluster JUMP ((a,k1):=k2) -> empty;
end;

registration
  let a,b,k1,k2;
  cluster JUMP ((a,k1):=(b,k2)) -> empty;
end;

registration
  let a,k1,k2;
  cluster JUMP (AddTo(a,k1,k2)) -> empty;
end;

registration
  let a,b,k1,k2;
  cluster JUMP (AddTo(a,k1,b,k2)) -> empty;
  cluster JUMP (SubFrom(a,k1,b,k2)) -> empty;
  cluster JUMP (MultBy(a,k1,b,k2)) -> empty;
  cluster JUMP (Divide(a,k1,b,k2)) -> empty;
end;

registration
  let a,k1,k2;
  cluster JUMP ((a,k1)<>0_goto k2) -> empty;
  cluster JUMP ((a,k1)<=0_goto k2) -> empty;
  cluster JUMP ((a,k1)>=0_goto k2) -> empty;
end;

theorem :: SCMPDS_9:18
  SUCC(l,SCMPDS) = NAT;

registration
  cluster SCMPDS -> non InsLoc-antisymmetric;
end;

registration
  cluster SCMPDS -> non weakly_standard;
end;