:: Weakly Standard Ordering of Instruction Locations
::  by Andrzej Trybulec , Piotr Rudnicki and Artur Korni{\l}owicz
::
:: Received April 22, 2010
:: Copyright (c) 2010-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, XBOOLE_0, SUBSET_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1,
      RELAT_1, TARSKI, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, NAT_1, GLIB_000,
      XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, GRAPH_2, CARD_1, FUNCT_2,
      FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, WAYBEL_0, MEMBERED, AMISTD_1,
      EXTPRO_1, AMI_WSTD, STRUCT_0, COMPOS_1, QUANTAL1, GOBRD13, MEMSTR_0,
      FUNCT_7, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, ORDINAL1,
      CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1,
      PARTFUN1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1,
      FUNCT_4, FUNCT_7, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0,
      COMPOS_0, FINSEQ_6, COMPOS_1, EXTPRO_1, FUNCT_2, AMISTD_1;
 constructors WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, RELSET_1,
      PRE_POLY, GRAPH_2, AMISTD_1, FUNCT_7, FUNCT_4, PBOOLE, FINSEQ_6,
      XTUPLE_0;
 registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1,
      XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, JORDAN1J, CARD_1,
      XXREAL_2, RELSET_1, FUNCT_4, AMISTD_1, EXTPRO_1, PRE_POLY, MEMSTR_0,
      MEASURE6, COMPOS_0, XTUPLE_0;
 requirements NUMERALS, BOOLE, REAL, SUBSET, ARITHM;


begin :: Ami-Struct

reserve x for set,
  D for non empty set,
  k, n for Element of NAT,
  z for Nat;
reserve N for with_zero set,
  S for
    IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
  i for Element of the InstructionsF of S,
  l, l1, l2, l3 for Element of NAT,
  s for State of S;
reserve ss for Element of product the_Values_of S;

begin :: Ordering of Instruction Locations

definition
  let N,S; let l1,l2 be Nat;
  pred l1 <= l2, S means
:: AMI_WSTD:def 1
  ex f being non empty FinSequence of NAT st f/.1
= l1 & f/.len f = l2 & for n st 1 <= n & n < len f
 holds f/.(n+1) in SUCC(f/.n,S);
end;

theorem :: AMI_WSTD:1
 for N,S for l1,l2 being Nat holds
  l1 <= l2,S & l2 <= l3, S implies l1 <= l3, S;

definition
  let N, S;
  attr S is InsLoc-antisymmetric means
:: AMI_WSTD:def 2
  for l1, l2 st l1 <= l2, S & l2 <= l1, S holds
  l1 = l2;
end;

definition
  let N, S;
  attr S is weakly_standard means
:: AMI_WSTD:def 3

  ex f being sequence of NAT st f is
  bijective & for m, n being Element of NAT holds m <= n iff f.m <= f.n, S;
end;

theorem :: AMI_WSTD:2
  for f1, f2 being sequence of NAT st f1 is bijective & (for
m, n being Element of NAT holds m <= n iff f1.m <= f1.n,S) & f2 is bijective &
 (for m, n being Element of NAT holds m <= n iff f2.m <= f2.n, S) holds f1 = f2
;

theorem :: AMI_WSTD:3
  for f being sequence of NAT st f is bijective holds
  (for m, n being Element of NAT holds m <= n iff f.m <= f.n, S)
   iff for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) &
    for j being Element of NAT st f.j in SUCC(f.k,S) holds k <= j;

theorem :: AMI_WSTD:4
  S is weakly_standard iff ex f being sequence of NAT st f is
  bijective & for k being Element of NAT holds f.(k+1) in SUCC(f.k,S) & for j
  being Element of NAT st f.j in SUCC(f.k,S) holds k <= j;

begin

registration
  let N be with_zero set;
  cluster STC N -> weakly_standard;
end;

registration
  let N be with_zero set;
  cluster weakly_standard halting
    for IC-Ins-separated non empty with_non-empty_values AMI-Struct
    over N;
end;

reserve T for weakly_standard
 IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N, k be natural Number;
  func il.(S,k) -> Element of NAT means
:: AMI_WSTD:def 4

  ex f being
sequence of NAT st f is bijective & (for m, n being Element of NAT holds
  m <= n iff f.m <= f.n, S) & it = f.k;
end;

theorem :: AMI_WSTD:5
  for N,T
  for k1, k2 being Nat st il.(T,k1) = il.(T,k2) holds
  k1 = k2;

theorem :: AMI_WSTD:6
  for l being Nat ex k being Nat st l = il.(T,k);

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, l be Nat;
  func locnum(l,S) -> Nat means
:: AMI_WSTD:def 5

  il.(S,it) = l;
end;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, l be Nat;
  redefine func locnum(l,S) -> Element of NAT;
end;

theorem :: AMI_WSTD:7
  for l1, l2 being Element of NAT holds locnum(l1,T) =
  locnum(l2,T) implies l1 = l2;

theorem :: AMI_WSTD:8
  for N,T
  for k1, k2 being natural Number holds
  il.(T,k1) <= il.(T,k2), T iff k1 <= k2;

theorem :: AMI_WSTD:9
  for N,T
  for l1, l2 being Element of NAT holds locnum(l1,T) <=
  locnum(l2,T) iff l1 <= l2, T;

theorem :: AMI_WSTD:10
  for N,T holds T is InsLoc-antisymmetric;

registration
  let N;
  cluster weakly_standard -> InsLoc-antisymmetric
   for IC-Ins-separated non
    empty with_non-empty_values AMI-Struct over N;
end;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, f be
  Element of NAT, k be Nat;
  func f +(k,S) -> Element of NAT equals
:: AMI_WSTD:def 6
  il.(S,locnum(f,S) + k);
end;

theorem :: AMI_WSTD:11
  for f being Element of NAT holds f + (0,T) = f;

theorem :: AMI_WSTD:12
  for f, g being Element of NAT st f + (z,T) = g + (z,T)
   holds f = g;

theorem :: AMI_WSTD:13
  for f being Element of NAT
   holds locnum(f,T) + z = locnum(f+(z,T),T);

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, f be
  Element of NAT;
  func NextLoc(f,S) -> Element of NAT equals
:: AMI_WSTD:def 7
  f + (1,S);
end;

theorem :: AMI_WSTD:14
  for f being Element of NAT
   holds NextLoc(f,T) = il.(T,locnum(f,T)+ 1);

theorem :: AMI_WSTD:15
  for f being Element of NAT holds f <> NextLoc(f,T);

theorem :: AMI_WSTD:16
  for f, g being Element of NAT st NextLoc(f,T) = NextLoc(g,T)
  holds f = g;

theorem :: AMI_WSTD:17
  il.(STC N, z) = z;

theorem :: AMI_WSTD:18
  for i being Instruction of STC N, s being State of STC N st InsCode i
  = 1 holds IC Exec(i,s) = NextLoc(IC s,STC N);

theorem :: AMI_WSTD:19
  for l being Element of NAT, i being Element of the
  InstructionsF of STC N st InsCode i = 1 holds NIC(i, l) = {NextLoc(l,STC N)};

theorem :: AMI_WSTD:20
  for l being Element of NAT holds SUCC(l,STC N) = {l, NextLoc(l,STC N)};

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N, i be Instruction of
  S;
  attr i is sequential means
:: AMI_WSTD:def 8
  for s being State of S holds Exec(i, s).IC S = NextLoc(IC s,S);
end;

theorem :: AMI_WSTD:21
  for S being weakly_standard IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N, il being Element of NAT,
  i being Instruction of S st i is sequential holds NIC(i,il)
   = {NextLoc(il,S)};

theorem :: AMI_WSTD:22
  for S being weakly_standard IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N,
    i being Instruction of S st i is sequential
   holds i is non halting;

registration
  let N;
  let S be weakly_standard IC-Ins-separated
    non empty with_non-empty_values AMI-Struct over N;
  cluster sequential -> non halting for Instruction of S;
  cluster halting -> non sequential for Instruction of S;
end;

begin :: Closedness of finite partial states

definition
  let N be with_zero set;
  let S be weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  let F be NAT-defined (the InstructionsF of S)-valued Function;
  attr F is para-closed means
:: AMI_WSTD:def 9
  for s being State of S st IC s = il.(S,0)
   for k being Element of NAT holds IC Comput(F,s,k) in dom F;
end;

theorem :: AMI_WSTD:23
  for S being weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N,
   F being NAT-defined (the InstructionsF of S)-valued
 finite Function st F is really-closed & il.(S,0) in dom F holds F is
  para-closed;

theorem :: AMI_WSTD:24
  for S being weakly_standard halting IC-Ins-separated
 non empty with_non-empty_values AMI-Struct over N holds il.(S,0) .-->
  halt S qua NAT-defined (the InstructionsF of S)-valued
   finite Function is really-closed;

definition
  let N be with_zero set;
  let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over
  N;
  let F be (the InstructionsF of S)-valued NAT-defined finite Function;
  attr F is lower means
:: AMI_WSTD:def 10

  for l being Element of NAT st l in
  dom F holds for m being Element of NAT st m <= l, S
   holds m in dom F;
end;

registration
  let N be with_zero set,
  S be IC-Ins-separated non
  empty with_non-empty_values AMI-Struct over N;
  cluster empty -> lower
    for finite (the InstructionsF of S)-valued NAT-defined Function;
end;

theorem :: AMI_WSTD:25
  for i being Element of the InstructionsF of T
   holds il.(T,0) .--> i is lower;

registration
  let N be with_zero set;
  let S be weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  cluster lower 1-element for NAT-defined
     (the InstructionsF of S)-valued finite Function;
end;

theorem :: AMI_WSTD:26
  for F being lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
   holds il.(T,0) in dom F;

theorem :: AMI_WSTD:27
  for P being lower
  NAT-defined (the InstructionsF of T)-valued finite Function
   holds z < card P iff il.(T,z) in dom P;

definition
  let N be with_zero set;
  let S be weakly_standard IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  let F be non empty
   NAT-defined (the InstructionsF of S)-valued finite Function;
  func LastLoc F -> Element of NAT means
:: AMI_WSTD:def 11

  ex M being finite non empty natural-membered set
   st M = { locnum(l,S) where l is
  Element of NAT : l in dom F } & it = il.(S, max M);
end;

theorem :: AMI_WSTD:28
  for F being non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
   holds LastLoc F in dom F;

theorem :: AMI_WSTD:29
  for F, G being non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
    st F c= G
  holds LastLoc F <= LastLoc G, T;

theorem :: AMI_WSTD:30
  for F being non empty
  NAT-defined (the InstructionsF of T)-valued finite Function,
      l being
  Element of NAT st l in dom F holds l <= LastLoc F, T;

theorem :: AMI_WSTD:31
  for F being lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function,
  G being non empty NAT-defined
   NAT-defined (the InstructionsF of T)-valued finite Function
    holds F c= G & LastLoc F = LastLoc G
  implies F = G;

theorem :: AMI_WSTD:32
  for F being lower non empty
   NAT-defined (the InstructionsF of T)-valued finite Function
  holds LastLoc F = il.(T, card F -' 1);

registration
  let N be with_zero set,
  S be weakly_standard
  IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
  cluster really-closed lower non empty -> para-closed for NAT-defined
    (the InstructionsF of S)-valued finite Function;
end;

definition
  let N be with_zero set,
  S be weakly_standard halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, F
  be non empty NAT-defined (the InstructionsF of S)-valued finite Function;
  attr F is halt-ending means
:: AMI_WSTD:def 12

  F.(LastLoc F) = halt S;
  attr F is unique-halt means
:: AMI_WSTD:def 13

  for f being Element of NAT st
  F.f = halt S & f in dom F holds f = LastLoc F;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  cluster halt-ending unique-halt trivial
   for lower non empty
    NAT-defined (the InstructionsF of S)-valued finite Function;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated
    non empty
  with_non-empty_values AMI-Struct over N;
  cluster trivial really-closed lower non empty
  for NAT-defined (the InstructionsF of S)-valued finite Function;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated
    non empty
  with_non-empty_values AMI-Struct over N;
  cluster halt-ending unique-halt trivial really-closed
  for lower non empty
   NAT-defined (the InstructionsF of S)-valued finite Function;
end;

definition
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated non empty
  with_non-empty_values AMI-Struct over N;
  mode pre-Macro of S is halt-ending unique-halt
   lower non empty
   NAT-defined (the InstructionsF of S)-valued finite Function;
end;

registration
  let N be with_zero set;
  let S be weakly_standard halting IC-Ins-separated
   non empty with_non-empty_values AMI-Struct over N;
  cluster really-closed for pre-Macro of S;
end;

theorem :: AMI_WSTD:33
  for N being with_zero set,
      S being IC-Ins-separated
       non empty with_non-empty_values AMI-Struct over N,
  l1, l2 being Element of NAT st SUCC(l1,S) = NAT
   holds l1 <= l2, S;

:: from SCMRING4, 2008.03.13, A.T.

reserve i, j, k for Nat,
  n for Element of NAT,
  N for with_zero set,
  S for weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N,
  l for Element of NAT,
  f for FinPartState of S;

definition
  let N be with_zero set,
  S be weakly_standard IC-Ins-separated
  non empty with_non-empty_values AMI-Struct over N, loc be
  Element of NAT, k be Nat;
  func loc -' (k,S) -> Element of NAT equals
:: AMI_WSTD:def 14
  il.(S, (locnum(loc,S)) -' k);
end;

theorem :: AMI_WSTD:34
  l -' (0,S) = l;

theorem :: AMI_WSTD:35
  l + (k,S) -' (k,S) = l;