MEMSTR_0

:: Memory Structures
::  by Andrzej Trybulec
::
:: Received April 28, 2011
:: Copyright (c) 2011-2026 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 STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, CARD_1,
      FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FSM_1, FINSET_1, NAT_1,
      ARYTM_1, PARTFUN1, AMI_1, ARYTM_3, COMPOS_1, SCMFSA6C, XXREAL_0,
      SUPINF_2, MEMSTR_0, PBOOLE, GOBRD13, QUANTAL1, SCMFSA9A;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, PBOOLE, FUNCT_7,
      CARD_1, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, NUMBERS,
      INT_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, AFINSQ_1, FINSEQ_1, FUNCT_2,
      DOMAIN_1, VALUED_0, VALUED_1, STRUCT_0, XXREAL_0, MEASURE6;
 constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7,
      PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
      FUNCT_4, FINSET_1, XREAL_0, CARD_3, STRUCT_0, RELSET_1, PBOOLE, NAT_1,
      CARD_1, MEASURE6;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions FUNCT_1;
 equalities FUNCOP_1, STRUCT_0, FUNCT_4;
 expansions STRUCT_0, FUNCT_1;
 theorems ZFMISC_1, TARSKI, CARD_3, FUNCT_4, FUNCOP_1, FUNCT_1, GRFUNC_1,
      RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, SUBSET_1, FUNCT_7,
      PARTFUN1, PBOOLE, XREAL_1, NAT_D, NAT_2, STRUCT_0, MEASURE6, XTUPLE_0;
 schemes FRAENKEL;

begin :: Terminology

 reserve x,N for set,
         k for Nat;

definition let N;
  struct (ZeroStr) Mem-Struct over N (# carrier -> set,
    ZeroF -> Element of the carrier,
    Object-Kind -> Function of the carrier, N,
    ValuesF -> ManySortedSet of N
     #);
end;

 reserve N for with_zero set;

:: wymaganie zeby N byl 'with_zero' jest troche na zapas
:: na razie wykorzystujemy tylko rejestracje, ze 'with_zero'
:: musi byc 'non empty' i w definicji Trivial-Mem N
:: ale tutaj mozna sie tego pozbyc, biorac zamiast 0
:: the Element of N i potrzebujemy tylko to, ze N jest niepusty

definition let N;
  func Trivial-Mem N -> strict Mem-Struct over N means
:Def1:
  the carrier of it = {0} & the ZeroF of it = 0 &
  the Object-Kind of it = 0 .--> 0 &
  the ValuesF of it = N --> NAT;
  existence
  proof
    set f = 0 .--> 0;
A1: dom f = {0};
A2: rng f c= {0} by FUNCOP_1:13;
    0 in N by MEASURE6:def 2;
    then { 0 } c= N by ZFMISC_1:31;
    then rng f c= N by A2,XBOOLE_1:1;
    then reconsider f as Function of {0}, N by A1,RELSET_1:4;
    reconsider y = 0 as Element of {0} by TARSKI:def 1;
    take Mem-Struct(#{0},y,f,N --> NAT #);
    thus thesis;
  end;
  uniqueness;
end;

registration let N;
  cluster Trivial-Mem N -> 1-element;
  coherence by Def1;
end;

registration let N;
  cluster 1-element for Mem-Struct over N;
  existence
  proof
    take Trivial-Mem N;
    thus thesis;
  end;
end;

notation let N;
  let S be Mem-Struct over N;
  synonym IC S for 0.S;
  synonym Data-Locations S for NonZero S;
end;

registration
::: gdzie to ma byc, dlaczego nie dziala SETFAM_1
  cluster with_zero -> non empty for set;
  coherence;
end;

definition let N;
  let S be Mem-Struct over N;
  func the_Values_of S -> ManySortedSet of the carrier of S equals
  (the ValuesF of S)*(the Object-Kind of S);
  coherence;
end;

definition let N;
  let S be Mem-Struct over N;
  mode PartState of S is (the carrier of S)-defined
           (the_Values_of S)-compatible Function;
end;

:: Jest potrzeba zagwarantowania, ze
:: the_Values_of S is non-empty
:: to bylo wczsniej obsluzone, ze stary N byl with_non-empty_elements
:: teraz jest to wlasnosc Mem-Str
:: sa tutaj rozne warianty, najprosciej jednak napisac co wymgamy:

definition let N;
  let S be Mem-Struct over N;
  attr S is with_non-empty_values means
:Def3: the_Values_of S is non-empty;
end;

registration let N;
  cluster Trivial-Mem N ->with_non-empty_values;
  coherence
  proof let n be object;
    set S = Trivial-Mem N, F = the_Values_of S;
   assume
A1:   n in dom F;
    then
A2:  (the Object-Kind of S).n in dom the ValuesF of S by FUNCT_1:11;
A3:  the ValuesF of S = N --> NAT by Def1;
    then
A4:  (the Object-Kind of S).n in N by A2;
    F.n =(the ValuesF of S).((the Object-Kind of S).n) by A1,FUNCT_1:12
       .= NAT by A4,A3,FUNCOP_1:7;
   hence F.n is non empty;
  end;
end;

registration let N;
  cluster with_non-empty_values for Mem-Struct over N;
  existence
  proof
   take Trivial-Mem N;
   thus thesis;
  end;
end;

registration let N;
  let S be with_non-empty_values Mem-Struct over N;
  cluster the_Values_of S -> non-empty;
  coherence by Def3;
end;

definition let N;
  let S be with_non-empty_values Mem-Struct over N;
  mode State of S is total PartState of S;
end;

definition let N;
  let S be Mem-Struct over N;
  mode Object of S is Element of S;
end;

begin :: the Object Kind

definition let N;
  let S be non empty Mem-Struct over N;
  let o be Object of S;
  func ObjectKind o -> Element of N equals
  (the Object-Kind of S).o;
  correctness;
end;

definition let N;
  let S be non empty Mem-Struct over N;
  let o be Object of S;
  func Values o -> set equals
  (the_Values_of S).o;
  correctness;
end;

:: Jezeli dodamy wartosci, to pewnie nie unikniemy zdefiniowania
:: funktora, ktory odpowiada staremu Object-Kind
:: np. the_Object-Kind_of, lub the_Values_of
:: i wtedy podmiana nie powinna byc zbyt skomplikowana.
:: Poza tym trzeba bedzie zmienic komputery, dodajac pole ValuesF
:: wykorzystac mozna atrybut with_zero, ale trzeba wprowadzic nowy:
:: (the ValuesF of S).0 = NAT

definition let N;
  let IT be non empty Mem-Struct over N;
  attr IT is IC-Ins-separated means
:Def6: Values IC IT = NAT;
end;

Lm1:
  the_Values_of Trivial-Mem N = 0 .--> NAT
  proof set S = Trivial-Mem N;
   set f = the_Values_of Trivial-Mem N, g = 0 .--> NAT;
    the Object-Kind of S = 0 .--> 0 by Def1;
    then
A1:  f = (N --> NAT)*(0 .--> 0) by Def1;
A2:  dom(N --> NAT) = N;
A3:  rng(0 .--> 0) = {0} by FUNCOP_1:88;
A4:  0 in N by MEASURE6:def 2;
    then {0} c= N by ZFMISC_1:31;
    then
A5:  dom f = dom(0 .--> 0) by A1,A2,A3,RELAT_1:27
     .= {0};
   hence
   dom f = dom g;
   let x be object;
   assume
A6:  x in dom f;
    then
A7:  x = 0 by A5,TARSKI:def 1;
   thus f.x = (N --> NAT).((0 .--> 0).x) by A1,A6,FUNCT_1:12
        .= (N --> NAT).0 by A7,FUNCOP_1:72
        .= NAT by A4,FUNCOP_1:7
        .= g.x by A7,FUNCOP_1:72;
  end;

registration let N;
  cluster Trivial-Mem N -> IC-Ins-separated;
  coherence
   proof
     IC Trivial-Mem N = 0 by Def1;
    hence Values IC Trivial-Mem N
     = (0 .--> NAT).0 by Lm1
    .= NAT by FUNCOP_1:72;
   end;
end;

registration let N;
  cluster IC-Ins-separated with_non-empty_values strict
    for 1-element Mem-Struct over N;
  existence
  proof
    take Trivial-Mem N;
    thus thesis;
  end;
end;

definition
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
  let p be PartState of S;
  func IC p -> Element of NAT equals
  p.IC S;
  coherence
  proof
   per cases;
   suppose
A1: IC S in dom p;
    consider s being State of S such that
A2: p c= s by PBOOLE:141;
   reconsider ss=s as Element of product the_Values_of S by CARD_3:107;
    dom the_Values_of S = the carrier of S by PARTFUN1:def 2;
    then pi(product the_Values_of S,IC S) = Values IC S by CARD_3:12
      .= NAT by Def6;
    then ss.IC S in NAT by CARD_3:def 6;
    hence thesis by A1,A2,GRFUNC_1:2;
   end;
   suppose not IC S in dom p;
    then p.IC S = 0 by FUNCT_1:def 2;
   hence thesis;
   end;
  end;
end;

theorem
 for S being IC-Ins-separated 1-element with_non-empty_values Mem-Struct over N
  for s1, s2 being State of S st IC s1 = IC s2 holds s1= s2
proof
 let T be IC-Ins-separated 1-element with_non-empty_values Mem-Struct over N;
  let s1,s2 be State of T such that
A1: IC s1 = IC s2;
A2: dom s1 = the carrier of T by PARTFUN1:def 2;
    then
A3: dom s1 =dom s2 by PARTFUN1:def 2;
 now
    let x be object;
    assume
A4: x in dom s1;
A5:  x = IC T  by A4,A2,STRUCT_0:def 10;
     hence s1.x = IC s1
        .= s2.x by A1,A5;
  end;
  hence thesis by A3;
end;

registration
  let N;
  let S be non empty with_non-empty_values Mem-Struct over N,
      o be Object of S;
  cluster Values o -> non empty;
  coherence;
end;

registration
  let N;
  let S be IC-Ins-separated non empty
       with_non-empty_values Mem-Struct over N;
  let la be Object of S;
  let a be Element of Values la;
  cluster la .--> a -> (the_Values_of S)-compatible;
  coherence
   proof
   set p = la .--> a;
     let x be object;
     assume
     x in dom p;
     then
A2: x = la by TARSKI:def 1;
     then p.x = a by FUNCOP_1:72;
     hence p.x in (the_Values_of S).x by A2;
   end;
  let lb be Object of S;
  let b be Element of Values lb;
  cluster (la,lb) --> (a,b) -> (the_Values_of S)-compatible;
  coherence;
end;

theorem Th2:
  for S being non empty with_non-empty_values Mem-Struct over N
  for s being State of S holds IC S in dom s
proof
  let S be non empty with_non-empty_values Mem-Struct over N;
  let s be State of S;
  dom s = the carrier of S by PARTFUN1:def 2;
  hence thesis;
end;

reserve S for IC-Ins-separated non empty with_non-empty_values
     Mem-Struct over N;

definition
  let N;
  let S be Mem-Struct over N;
  let p be PartState of S;
  func DataPart p -> PartState of S equals
  p | Data-Locations S;
  coherence;
  projectivity;
end;

definition
  let N; let S be Mem-Struct over N;
  let p be PartState of S;
  attr p is data-only means
:Def9:
  dom p misses {IC S};
end;

registration
  let N; let S be Mem-Struct over N;
  cluster empty -> data-only for PartState of S;
  coherence by RELAT_1:38,XBOOLE_1:65;
end;

registration
  let N; let S be Mem-Struct over N;
  cluster empty for PartState of S;
  existence
  proof
    reconsider a = {} as PartState of S by FUNCT_1:104,RELAT_1:171;
    take a;
    thus thesis;
  end;
end;

theorem Th3:
  for N for S being Mem-Struct over N
  for p being PartState of S holds not IC S in dom DataPart p
proof
  let N; let S be Mem-Struct over N;
  let p be PartState of S;
  assume
A1: IC S in dom DataPart p;
  dom DataPart p c= (the carrier of S) \ {IC S} by RELAT_1:58;
  then not IC S in {IC S} by A1,XBOOLE_0:def 5;
  hence contradiction by TARSKI:def 1;
end;

theorem
  for N for S being Mem-Struct over N for p being
  PartState of S holds {IC S} misses dom DataPart p by Th3,ZFMISC_1:50;

theorem
  for p being data-only PartState of S, q being PartState of S
  holds p c= q iff p c= DataPart q
proof
  let p be data-only PartState of S, q be PartState of S;
  set X = (the carrier of S) \ ({IC S});
A1: q|X c= q by RELAT_1:59;
  hereby
A2:  X \/ ({IC S}) = (the carrier of S) \/ ({IC S})
     by XBOOLE_1:39;
    dom p c= the carrier of S by RELAT_1:def 18;
    then
A3: dom p c= X \/ ({IC S}) by A2,XBOOLE_1:10;
    assume
    p c= q;
    then
A4: p|X c= DataPart q by RELAT_1:76;
    dom p misses {IC S} by Def9;
    hence p c= DataPart q by A4,A3,RELAT_1:68,XBOOLE_1:73;
  end;
 thus thesis by A1,XBOOLE_1:1;
end;

registration
  let N;
  let S be Mem-Struct over N;
  let p be PartState of S;
  cluster DataPart p -> data-only;
  coherence by Th3,ZFMISC_1:50;
end;

theorem Th6:
  for S being Mem-Struct over N, p being PartState
  of S holds p is data-only iff dom p c= Data-Locations S
    by RELAT_1:def 18,XBOOLE_1:86,XBOOLE_1:106;

theorem
  for S being Mem-Struct over N, p being data-only PartState of S
   holds DataPart p = p
proof
  let S be Mem-Struct over N, p be data-only PartState of S;
     dom p c= Data-Locations S by Th6;
    hence thesis by RELAT_1:68;
end;

 reserve s for State of S;

theorem Th8:
  Data-Locations S c= dom s
proof
  dom s = the carrier of S by PARTFUN1:def 2;
  hence thesis;
end;

theorem Th9:
  dom DataPart s = Data-Locations S
proof
  Data-Locations S c= dom s by Th8;
  hence thesis by RELAT_1:62;
end;

theorem Th10:
  for d being data-only PartState of S holds not IC S in dom d
proof
  let d be data-only PartState of S;
  dom d c= Data-Locations S by Th6;
  hence thesis by STRUCT_0:3;
end;

theorem Th11:
  for p being PartState of S, d being data-only PartState of S
  holds IC(p+*d) = IC p
proof
  let p be PartState of S, d be data-only PartState of S;
A1: not IC S in dom d by Th10;
  thus IC(p+*d) = IC p by A1,FUNCT_4:11;
end;

 reserve p for PartState of S;

theorem
  for p being PartState of S holds DataPart p c=  p by RELAT_1:59;

theorem Th13:
  dom s = {IC S} \/ Data-Locations S
proof
  dom s = the carrier of S by PARTFUN1:def 2;
  hence thesis by STRUCT_0:4;
end;

theorem
  dom p /\ Data-Locations S = dom DataPart p by RELAT_1:61;

registration let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat, s be State of S;
  cluster s+*(IC S,l) -> (the_Values_of S)-compatible;
 coherence
  proof let x be object;
   assume x in dom(s+*(IC S,l));
    then
A1:   x in dom s by FUNCT_7:30;
   per cases;
   suppose
A2:   x = IC S;
    then
A3:   (s+*(IC S,l)).x = l by A1,FUNCT_7:31;
    reconsider l as Element of NAT by ORDINAL1:def 12;
    Values IC S = NAT by Def6;
   then (s+*(IC S,l)).x in (the_Values_of S).x by A2,A3;
   hence thesis;
   end;
   suppose x <> IC S;
    then (s+*(IC S,l)).x = s.x by FUNCT_7:32;
   hence (s+*(IC S,l)).x in (the_Values_of S).x by A1,FUNCT_1:def 14;
   end;
  end;
end;

begin :: The value of the Instruction Counter

definition
  let N;
  let S be IC-Ins-separated non empty
    with_non-empty_values Mem-Struct over N;
  let l be Nat;
  func Start-At(l,S) -> PartState of S equals
   IC S .--> l;
  correctness
  proof
    reconsider l as Element of NAT by ORDINAL1:def 12;
    Values IC S = NAT by Def6;
    then reconsider l as Element of Values IC S;
     IC S .--> l is PartState of S;
    hence thesis;
  end;
end;

definition
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  let p be PartState of S;
  attr p is l-started means
:Def11: IC S in dom p & IC p = l;
end;

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  cluster Start-At(l,S) -> l-started non empty;
  coherence by TARSKI:def 1,FUNCOP_1:72;
end;

theorem Th15:
  for l being Nat holds IC S in dom Start-At(l,S) by TARSKI:def 1;

theorem Th16:
  for n being Nat holds IC(p +* Start-At( n,S)) = n
proof
 let n be Nat;
A1: IC S in dom Start-At( n,S) by Th15;
  (Start-At( n,S)).IC S =  n by FUNCOP_1:72;
  hence thesis by A1,FUNCT_4:13;
end;

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  cluster l-started for State of S;
   :: dla PartState nie trzeba zaklada 'with_non-empty_values'
   :: ale chyba nie warto robic osobnej rejestracji
  existence
   proof
    take s = (the State of S)+*Start-At(l,S);
    thus IC S in dom s by Th2;
    thus IC s = l by Th16;
   end;
end;

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat,
      p being PartState of S,
      q be l-started PartState of S;
  cluster p +* q -> l-started;
  coherence
   proof
A1:   IC S in dom q by Def11;
     dom q c= dom(p+*q) by FUNCT_4:10;
    hence IC S in dom(p+*q) by A1;
     IC q = l by Def11;
    hence IC(p+*q) = l by A1,FUNCT_4:13;
   end;
end;

definition
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  let s be State of S;
  redefine attr s is l-started means  :: redefines -started (MEMSTR_0, definition)
  IC s = l;
  compatibility
   by Th2;
end;

theorem
  for S being IC-Ins-separated non empty with_non-empty_values
               Mem-Struct over N,
      l being Nat,
      p being l-started PartState of S
  for s being PartState of S st p c= s holds s is l-started
proof
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat,
      p be l-started PartState of S;
A1: IC S in dom p by Def11;
A2: IC p = l by Def11;
  let s be PartState of S;
  assume
A3:  p c= s;
   then dom p c= dom s by RELAT_1:11;
  hence IC S in dom s by A1;
  thus IC s = l by A3,A2,A1,GRFUNC_1:2;
end;

theorem Th18:
  for s being State of S holds Start-At(IC s,S) = s | {IC S}
proof
  let s be State of S;
A1: IC S in dom s by Th2;
  thus Start-At(IC s,S) = {[IC S,s.IC S]} by FUNCT_4:82
    .= s | {IC S} by A1,GRFUNC_1:28;
end;

theorem Th19:
  for S being IC-Ins-separated non empty with_non-empty_values
         Mem-Struct over N
  for p being PartState of S st IC S in
  dom p holds p = Start-At(IC p,S) +* DataPart p
proof
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
  let p be PartState of S;
  assume IC S in dom p;
  then
A1: {IC S} is Subset of dom p by SUBSET_1:41;
A2: {IC S} \/ ((the carrier of S) \ {IC S})
     = (the carrier of S) \/ {IC S} by XBOOLE_1:39
    .= the carrier of S by XBOOLE_1:12;
A3: dom p c= the carrier of S by RELAT_1:def 18;
A4: now
    let x be object;
    assume
A5: x in dom p;
    per cases by A5,A3,A2,XBOOLE_0:def 3;
    suppose
A6:   x in {IC S};
      IC S in dom Start-At(IC p,S) by TARSKI:def 1;
      then
A7:  IC S in dom (Start-At(IC p,S)) \/ dom DataPart p by XBOOLE_0:def 3;
A8:  x = IC S by A6,TARSKI:def 1;
      not IC S in dom (DataPart p) by Th3;
      then
      (Start-At(IC p,S) +* DataPart p).x
         = (Start-At(IC p,S)).x by A8,A7,FUNCT_4:def 1
        .= IC p by A8,FUNCOP_1:72;
      hence p.x = (Start-At(IC p,S) +* DataPart p).x by A6,TARSKI:def 1;
    end;
    suppose
      x in (the carrier of S) \ {IC S};
      then x in dom p /\ ((the carrier of S) \ {IC S}) by A5,XBOOLE_0:def 4;
      then
A9:  x in dom (p | ((the carrier of S) \ {IC S})) by RELAT_1:61;
      (Start-At(IC p,S) +* DataPart p).x
       = (DataPart p).x by A9,FUNCT_4:13
        .= p.x by A9,FUNCT_1:47;
      hence p.x = (Start-At(IC p,S) +* DataPart p).x;
    end;
  end;
A10: dom p c= the carrier of S by RELAT_1:def 18;
  dom(Start-At(IC p,S) +* DataPart p)
     = dom (Start-At(IC p,S) ) \/ dom (DataPart p) by FUNCT_4:def 1
    .= {IC S} \/ dom(DataPart p)
    .= dom p /\ {IC S} \/ dom(p|((the carrier of S) \ {IC S}))
         by A1,XBOOLE_1:28
    .= dom p /\ {IC S} \/ dom p /\ ((the carrier of S) \ {IC S}) by RELAT_1:61
    .= dom p /\ the carrier of S by A2,XBOOLE_1:23
    .= dom p by A10,XBOOLE_1:28;
  hence thesis by A4;
end;

theorem Th20:
  for S be IC-Ins-separated non empty
     with_non-empty_values Mem-Struct over N, l be Nat
  holds DataPart Start-At(l,S) = {}
proof
 let S be IC-Ins-separated non empty
 with_non-empty_values Mem-Struct over N, l be Nat;
  Data-Locations S misses {IC S} by XBOOLE_1:79;
  then Data-Locations S misses dom Start-At(l,S);
 hence thesis by RELAT_1:66;
end;

theorem
  for l1,l2,k being Nat holds Start-At(l1+k,S) =
  Start-At(l2+k,S) iff Start-At(l1,S) = Start-At(l2,S)
proof
  let l1,l2,k be Nat;
  hereby
    assume Start-At(l1+k,S) = Start-At(l2+k,S);
    then {[IC S, l1+k]} = IC S .--> (l2+k) by FUNCT_4:82;
    then {[IC S, l1+k]} = {[IC S, l2+k]} by FUNCT_4:82;
    then [IC S, l1+k] = [IC S, l2+k] by ZFMISC_1:3;
    then l1+k = l2+k by XTUPLE_0:1;
    hence Start-At(l1,S) = Start-At(l2,S);
  end;
  assume Start-At(l1,S) = Start-At(l2,S);
  then {[IC S, l1]} = Start-At(l2,S) by FUNCT_4:82;
  then {[IC S, l1]} = {[IC S, l2]} by FUNCT_4:82;
  then [IC S, l1] = [IC S, l2] by ZFMISC_1:3;
  hence thesis by XTUPLE_0:1;
end;

theorem
  for l1,l2,k being Nat st Start-At(l1,S) = Start-At(l2,S)
  holds Start-At(l1 -' k,S) = Start-At(l2 -' k,S)
proof
  let l1,l2,k be Nat;
  assume Start-At(l1,S) = Start-At(l2,S);
  then {[IC S, l1]} = Start-At(l2,S) by FUNCT_4:82
    .= {[IC S, l2]} by FUNCT_4:82;
  then [IC S, l1] = [IC S, l2] by ZFMISC_1:3;
  hence thesis by XTUPLE_0:1;
end;

theorem Th23:
  for d being data-only PartState of S, k being Nat
  holds d tolerates Start-At(k,S)
proof
  let d be data-only PartState of S, k be Nat;
  dom d misses dom Start-At(k,S) by Th10,ZFMISC_1:50;
  hence thesis by PARTFUN1:56;
end;

theorem Th24:
 for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
  for p being PartState of S st IC S in dom p
  holds dom p = {IC S} \/ dom DataPart p
proof
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
 let p be PartState of S;
 assume IC S in dom p;
  then
A1: p = Start-At(IC p,S) +* DataPart p by Th19;
  dom p =  dom Start-At(IC p,S) \/ dom DataPart p by A1,FUNCT_4:def 1
    .= {IC S} \/ dom DataPart p;
 hence thesis;
end;

theorem
  for S being IC-Ins-separated non empty with_non-empty_values
       Mem-Struct over N
  for s being State of S
  holds dom s = {IC S} \/ dom DataPart s by Th2,Th24;

theorem Th26:
  for p being PartState of S st IC S in dom p
  holds p = DataPart p +* Start-At (IC p,S)
proof
 let p be PartState of S;
A2: dom DataPart p misses dom Start-At (IC p,S) by Th3,ZFMISC_1:50;
A3: dom((Start-At(IC p,S))) misses dom DataPart p
                  by Th3,ZFMISC_1:50;
 assume IC S in dom p;
  then p = Start-At(IC p,S) +* DataPart p by Th19;
  then
A4:  p = (Start-At(IC p,S) ) \/  DataPart p by A3,FUNCT_4:31;
 thus thesis by A2,A4,FUNCT_4:31;
end;

theorem Th27:
  IC S in dom (p +* Start-At( k,S))
proof
  IC S in dom Start-At( k,S) by TARSKI:def 1;
  hence thesis by FUNCT_4:12;
end;

theorem
  p +* Start-At( k,S) c= s implies IC s =  k
proof
  assume
A1: p +* Start-At( k,S) c= s;
  IC S in dom (p +* Start-At( k,S)) by Th27;
  hence IC s = IC(p +* Start-At( k,S)) by A1,GRFUNC_1:2
    .=  k by Th16;
end;

theorem Th29:
  for S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat
  for p be PartState of S
  holds p is l-started iff Start-At(l,S) c= p
proof
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
     l be Nat;
 let p be PartState of S;
 thus p is l-started implies Start-At(l,S) c= p
  proof assume
A2:  p is l-started;
    IC S in dom p by A2;
    then
A3:  dom Start-At(l,S) c= dom p by ZFMISC_1:31;
    for x being object st x in dom Start-At(l,S) holds Start-At(l,S).x = p.x
     proof let x be object;
      assume
A4:     x in dom Start-At(l,S);
      hence Start-At(l,S).x = IC Start-At(l,S) by TARSKI:def 1
         .= l by FUNCOP_1:72
         .= IC p by A2
         .= p.x  by A4,TARSKI:def 1;
     end;
   hence Start-At(l,S) c= p by A3,GRFUNC_1:2;
  end;
 assume
A5: Start-At(l,S) c= p;
  then
A6:  dom Start-At(l,S) c= dom p by RELAT_1:11;
A7: IC S in dom Start-At(l,S) by TARSKI:def 1;
 hence IC S in dom p by A6;
 thus IC p = IC Start-At(l,S) by A5,A7,GRFUNC_1:2
     .= l by FUNCOP_1:72;
end;

registration let N,S; let k be Nat;
  let p be k-started PartState of S, d be data-only PartState of S;
  cluster p +* d -> k-started;
  coherence
  proof
A1: IC S in dom p by Def11;
    dom(p +* d) = dom p \/ dom d by FUNCT_4:def 1;
    hence IC S in dom(p +* d) by A1,XBOOLE_0:def 3;
    not IC S in dom d by Th10;
    hence IC(p +* d) =IC p by FUNCT_4:11
     .= k by Def11;
  end;
end;

theorem Th30:
  Start-At(IC s,S) c= s
 proof
   Start-At(IC s,S) = s | {IC S} by Th18;
   hence thesis by RELAT_1:59;
 end;

theorem
  for s being State of S
  holds s +* Start-At(IC s,S) = s by Th30,FUNCT_4:98;

theorem
  dom p c= {IC S} \/ dom DataPart p
proof
 set S0 = Start-At(0,S);
 per cases;
 suppose IC S in dom p;
  hence thesis by Th24;
 end;
 suppose
A1: not IC S in dom p;
A3:  dom (p +* S0)
     = {IC S} \/ dom DataPart(p +* S0) by Th24,Th27
    .= {IC S} \/ dom(DataPart p +* DataPart S0) by FUNCT_4:71
    .= {IC S} \/ dom(DataPart p +* {}) by Th20
    .= {IC S} \/ dom DataPart p;
  now assume dom p meets dom S0;
   then consider x being object such that
A4: x in dom p and
A5: x in dom S0 by XBOOLE_0:3;
   thus contradiction by A4,A1,A5,TARSKI:def 1;
  end;
  then p c= p +* S0 by FUNCT_4:32;
  hence dom p c= {IC S} \/ dom DataPart p by A3,RELAT_1:11;
 end;
end;

theorem Th33:
  for S being IC-Ins-separated non empty with_non-empty_values
         Mem-Struct over N
  for s be State of S holds s = s|(Data-Locations S \/ {IC S})
proof
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
 let s be State of S;
 thus s = s|dom s
     .= s|({IC S} \/ dom DataPart s) by Th2,Th24
     .= s|(Data-Locations S \/ {IC S}) by Th9;
end;

theorem
  for S being IC-Ins-separated non empty with_non-empty_values
        Mem-Struct over N
  for s1,s2 be State of S
  st s1|(Data-Locations S \/ {IC S}) = s2|(Data-Locations S \/ {IC S})
  holds s1 =  s2
proof
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
 let s1,s2 be State of S;
  s1 = s1|(Data-Locations S \/ {IC S}) by Th33;
 hence thesis by Th33;
end;

theorem
  IC S in dom p implies p = Start-At(IC p,S) +* DataPart p by Th19;

theorem Th36:
  for p being PartState of S, k,l being Nat
  holds p +* Start-At(k,S) +* Start-At(l,S)  = p +* Start-At(l,S)
proof let p be PartState of S, k,l be Nat;
  dom Start-At(k,S) = {IC S}
    .= dom Start-At(l,S);
 hence p +* Start-At(k,S) +* Start-At(l,S)  = p +* Start-At(l,S) by FUNCT_4:74;
end;

theorem
  for p being PartState of S st IC S in dom p
  holds p +* Start-At(IC p,S) = p by FUNCT_4:7,98;

theorem
  p +* Start-At(k,S) c= s implies IC s = k
proof
  assume
A1: p +* Start-At(k,S) c= s;
  IC S in dom (p +* Start-At( k,S)) by Th27;
  hence IC s = IC (p +* Start-At( k,S)) by A1,GRFUNC_1:2
    .=  k by Th16;
end;

theorem
  for p being PartState of S holds Start-At(0,S) c= p implies IC p = 0
proof let p be PartState of S;
A1: IC Start-At(0,S) = 0 by Def11;
 IC S in dom Start-At(0,S) by Def11;
  hence thesis by A1,GRFUNC_1:2;
end;

theorem
  for p being PartState of S st Start-At(k,S) c= p holds IC p = k
proof
 let p be PartState of S;
 assume Start-At(k,S) c= p;
  then p is k-started by Th29;
 hence IC p = k;
end;

registration let N;
  let S be IC-Ins-separated non empty
     with_non-empty_values Mem-Struct over N;
  cluster non empty for PartState of S;
  existence
  proof
    take Start-At(0,S);
    thus thesis;
  end;
end;

theorem
  for S being IC-Ins-separated non empty with_non-empty_values
    Mem-Struct over N
  for p being non empty PartState of S
  holds dom p meets {IC S} \/ Data-Locations S
  proof let S being IC-Ins-separated non empty
       with_non-empty_values Mem-Struct over N;
  let p be non empty PartState of S;
   dom p c= the carrier of S by RELAT_1:def 18;
   then dom p meets the carrier of S by XBOOLE_1:69;
   hence dom p meets {IC S} \/ Data-Locations S by STRUCT_0:4;
  end;

begin :: Initialize

definition let N;
  let S be IC-Ins-separated non empty
    with_non-empty_values Mem-Struct over N;
  let p be PartState of S;
  func Initialize p -> PartState of S equals
  p +* Start-At(0,S);
  coherence;
  projectivity;
end;

registration let N,S;
  let p be PartState of S;
  cluster Initialize p -> 0-started;
  coherence;
end;

theorem Th42:
  for S being IC-Ins-separated non empty
  with_non-empty_values Mem-Struct over N,
      p being PartState of S
  holds dom Initialize p = dom p \/ {IC S}
proof let S be IC-Ins-separated non empty
   with_non-empty_values Mem-Struct over N;
  let p being PartState of S;
  thus dom Initialize p
     = dom p \/ dom Start-At(0,S) by FUNCT_4:def 1
    .= dom p \/ {IC S};
end;

theorem
  for x being set st x in dom Initialize p holds x in dom p or x = IC S
proof
  let x be set;
  assume
A1: x in dom Initialize p;
  dom Initialize p = dom p \/ {IC S} by Th42;
  then x in dom p or x in {IC S} by A1,XBOOLE_0:def 3;
  hence thesis by TARSKI:def 1;
end;

theorem
  for p being 0-started PartState of S
  holds Initialize p = p
 proof let p be 0-started PartState of S;
   IC S in dom p & IC p = 0 by Def11;
  hence Initialize p = p by FUNCT_4:85,98;
 end;

theorem Th45:
  for p being PartState of S
  holds DataPart Initialize p = DataPart p
 proof let p be PartState of S;
  thus DataPart Initialize p
        = DataPart p +* DataPart Start-At(0,S) by FUNCT_4:71
       .= DataPart p +* {} by Th20
       .= DataPart p;
 end;

theorem
  for s being State of S st IC s =  0 holds Initialize s = s
proof let s be State of S;
  IC S in dom s by Th2;
  hence thesis by FUNCT_7:96;
end;

registration let N,S;
  let s be State of S;
  cluster Initialize s -> total;
  coherence;
end;

theorem Th47:
  for p being PartState of S
  holds Initialize p c= s implies IC s = 0
proof let p be PartState of S;
A1: IC Initialize p =  0 by Def11;
A2: IC S in dom Initialize p by Def11;
  assume Initialize p c= s;
  hence thesis by A1,A2,GRFUNC_1:2;
end;

theorem Th48:
  for p being PartState of S holds IC S in dom Initialize p
proof let p be PartState of S;
A1: dom Initialize p = dom p \/ {IC S} by Th42;
  IC S in {IC S} by TARSKI:def 1;
 hence IC S in dom Initialize p by A1,XBOOLE_0:def 3;
end;

theorem
  for p,q being PartState of S holds IC S in dom(p +* Initialize q)
proof let p,q be PartState of S;
A1: dom(p +* Initialize q) =  dom p \/ dom Initialize q by FUNCT_4:def 1;
  IC S in dom Initialize q by Th48;
 hence IC S in dom(p +* Initialize q) by A1,XBOOLE_0:def 3;
end;

theorem
  for S being IC-Ins-separated non empty
    with_non-empty_values Mem-Struct over N
  for p,q being PartState of S
  holds Initialize p c= q implies Start-At(0,S) c= q
proof
 let S be IC-Ins-separated non empty
 with_non-empty_values Mem-Struct over N;
 let p,q be PartState of S;
  Start-At(0,S) c= Initialize p by FUNCT_4:25;
 hence thesis by XBOOLE_1:1;
end;

begin :: Increment & Decrement, of the Instruction Counter

definition let N,S;
  let p be PartState of S, k be Nat;
  func IncIC(p,k) -> PartState of S equals
  p +* Start-At(IC p+k,S);
  correctness;
end;

theorem Th51:
  for p being PartState of S, k being Nat
  holds DataPart IncIC(p,k) = DataPart p
proof
  let p be PartState of S, k be Nat;
  thus DataPart IncIC(p,k)
  = DataPart p +* DataPart Start-At(IC p+k,S) by FUNCT_4:71
    .= DataPart p +* {} by Th20
    .= DataPart p;
end;

theorem Th52:
  for p being PartState of S, k being Nat holds IC S in dom IncIC(p,k)
proof let p be PartState of S, k be Nat;
A1: dom IncIC(p,k) = dom p \/ dom Start-At(IC p+k,S) by FUNCT_4:def 1;
  IC S in dom Start-At(IC p+k,S) by Th15;
  hence thesis by A1,XBOOLE_0:def 3;
end;

theorem Th53:
  for p being PartState of S, k being Nat
   holds IC IncIC (p,k) = IC p + k
proof
  let p be PartState of S, k be Nat;
   IC S in dom Start-At(IC p+k,S) by TARSKI:def 1;
  hence IC IncIC (p,k) = (Start-At((IC p)+k,S)).IC S by FUNCT_4:13
    .= IC p +k by FUNCOP_1:72;
end;

theorem
  for d being data-only PartState of S, k being Nat
  holds IncIC(p+*d,k) = IncIC(p,k) +* d
proof
  let d be data-only PartState of S, k be Nat;
A1: d tolerates Start-At(IC p+k,S) by Th23;
  thus IncIC(p+*d,k) = p +* d +* Start-At(IC p+k,S) by Th11
    .= p +* (d +* Start-At(IC p+k,S)) by FUNCT_4:14
    .= p +* (Start-At(IC p+k,S) +* d) by A1,FUNCT_4:34
    .= IncIC(p,k) +* d by FUNCT_4:14;
end;

theorem
  for p being PartState of S, k being Nat holds
  Start-At(IC p+k,S) c= IncIC (p,k)
proof
  let p be PartState of S, k be Nat;
A1: IC IncIC(p,k) = IC p + k by Th53;
A2: IC S in dom (IncIC(p,k)) by Th52;
A3: Start-At(IC p+k,S) = {[IC S,IC p + k]} & [IC S,IC p + k] in
  IncIC(p,k) by A2,A1,FUNCT_1:def 2,FUNCT_4:82;
  for x being object st x in Start-At(IC p+k,S)
    holds x in IncIC (p,k) by A3,TARSKI:def 1;
 hence thesis by TARSKI:def 3;
end;

theorem
  for p being PartState of S st IC S in dom p
  holds IncIC( p,k) = DataPart p +* Start-At ((IC p) +k,S)
 proof let p be PartState of S;
A1: dom Start-At ((IC p) +k,S) = {IC S}
     .= dom Start-At (IC p,S);
  assume
A2: IC S in dom p;
  thus IncIC( p,k)
     = DataPart p +* Start-At (IC p,S) +* Start-At ((IC p) +k,S) by A2,Th26
    .= DataPart p +* Start-At ((IC p) +k,S) by A1,FUNCT_4:74;
 end;

registration
  let N,S;
  let s be State of S, k be Nat;
  cluster IncIC(s,k) -> total;
  coherence;
end;

theorem
  for p being PartState of S, i,j being Nat
  holds IncIC(IncIC(p,i),j) = IncIC(p,i+j)
 proof let p be PartState of S, i,j being Nat;
  thus IncIC(IncIC(p,i),j)
        = p +* Start-At(IC p+i,S) +* Start-At(IC p + i +j,S) by Th53
       .= IncIC(p,i+j) by FUNCT_4:114;
 end;

theorem
  for p being PartState of S, j,k being Nat
  holds IncIC(p +* Start-At(j,S),k) = p +* Start-At(j+k,S)
proof
 let p be PartState of S, j,k be Nat;
 thus IncIC(p +* Start-At(j,S),k)
   = p +* Start-At(IC(p +* Start-At(j,S))+k,S) by FUNCT_4:114
  .= p +* Start-At(j+k,S) by Th16;
end;

theorem
  for k being Nat
  holds IC IncIC(s,k) -' k = IC s
proof
 let k be Nat;
 thus IC IncIC(s,k) -' k = IC s + k -' k by Th53
    .= IC s by NAT_D:34;
end;

theorem
  for p,q being PartState of S, k being Nat st IC S in dom q
  holds IncIC(p+*q,k) = p +* IncIC(q,k)
proof let p,q be PartState of S, k be Nat;
  assume IC S in dom q;
   then IC(p+*q) = IC q by FUNCT_4:13;
 hence IncIC(p+*q,k) = p +* IncIC(q,k) by FUNCT_4:14;
end;

theorem
 for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
  for k being Nat, p being PartState of S,
      s1, s2 being State of S st p c= s1 & IncIC(p,k) c= s2
   holds p c= s1 +* DataPart s2
proof
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
  let k be Nat, p be PartState of S,
      s1, s2 be State of S such that
A1: p c= s1 and
A2: IncIC(p,k) c= s2;
  set s3 = DataPart s2;
  reconsider s = s1 +* DataPart s2 as State of S;
A3:  dom p c= the carrier of S by RELAT_1:def 18;
  then
A4: dom p c= {IC S} \/ Data-Locations S by STRUCT_0:4;
A5: now
    Data-Locations S = dom s2 /\ Data-Locations S
       by Th8,XBOOLE_1:28;
    then
A6: dom s3 = Data-Locations S by RELAT_1:61;
    let x be object such that
A7: x in dom p;
    per cases by A4,A7,XBOOLE_0:def 3;
    suppose
A8:   x in {IC S};
      x = IC S by A8,TARSKI:def 1;
      then s1.x = s.x by A6,FUNCT_4:11,STRUCT_0:3;
      hence (p).x = s.x by A1,A7,GRFUNC_1:2;
    end;
    suppose
A9:  x in Data-Locations S;
      set DPp = DataPart p;
      x in dom p /\ Data-Locations S by A9,A7,XBOOLE_0:def 4;
      then
A10:  x in dom DPp by RELAT_1:61;
A11:   DataPart IncIC(p,k) = DPp by Th51;
      DPp c= IncIC(p,k) by A11,RELAT_1:59;
      then
A12:  DPp c= s2 by A2,XBOOLE_1:1;
      then dom DPp c= dom s2 by GRFUNC_1:2;
      then x in dom s2 /\ Data-Locations S by A9,A10,XBOOLE_0:def 4;
      then
A13:  x in dom s3 by RELAT_1:61;
      DPp c= p by RELAT_1:59;
      then
A14:  DPp.x = (p).x by A10,GRFUNC_1:2;
A15:  s2.x = s3.x by A9,FUNCT_1:49;
      DPp.x = s2.x by A10,A12,GRFUNC_1:2;
      hence (p).x = s.x by A14,A15,A13,FUNCT_4:13;
    end;
  end;
  dom p c= dom s by A3,PARTFUN1:def 2;
  hence thesis by A5,GRFUNC_1:2;
end;

theorem
 for S being IC-Ins-separated non empty with_non-empty_values Mem-Struct over N
 for p being PartState of S, k being Nat
 holds DataPart p c= IncIC(p,k)
proof
 let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
 let p being PartState of S, k be Nat;
  DataPart IncIC(p,k) = DataPart p by Th51;
 hence DataPart p c= IncIC(p,k) by RELAT_1:59;
end;

definition let N,S;
  let p be PartState of S, k be Nat;
  func DecIC(p,k) -> PartState of S equals
  p +* Start-At(IC p-'k,S);
  correctness;
end;

theorem
  for p being PartState of S, k being Nat
  holds DataPart DecIC(p,k) = DataPart p
proof
  let p be PartState of S, k be Nat;
  thus DataPart DecIC(p,k)
  = DataPart p +* DataPart Start-At(IC p-'k,S) by FUNCT_4:71
    .= DataPart p +* {} by Th20
    .= DataPart p;
end;

theorem Th64:
  for k being Nat holds IC S in dom DecIC(p,k)
proof let k be Nat;
A1: dom DecIC(p,k) = dom p \/ dom Start-At(IC p-'k,S) by FUNCT_4:def 1;
  IC S in dom Start-At(IC p-'k,S) by Th15;
  hence thesis by A1,XBOOLE_0:def 3;
end;

theorem Th65:
  for p being PartState of S, k being Nat
   holds IC DecIC (p,k) = IC p -' k
proof
  let p be PartState of S, k be Nat;
   IC S in dom Start-At(IC p-'k,S) by TARSKI:def 1;
  hence IC DecIC (p,k) = (Start-At((IC p)-'k,S)).IC S by FUNCT_4:13
    .= IC p -' k by FUNCOP_1:72;
end;

theorem
  for p being PartState of S,
   d being data-only PartState of S, k being Nat
  holds DecIC(p+*d,k) = DecIC(p,k) +* d
proof let p be PartState of S;
  let d be data-only PartState of S, k being Nat;
A1: d tolerates Start-At(IC p-'k,S) by Th23;
  thus DecIC(p+*d,k)
     = p +* d +* Start-At((IC p)-'k,S) by Th11
    .= p +* (d +* Start-At(IC p-'k,S)) by FUNCT_4:14
    .= p +* (Start-At(IC p-'k,S) +* d) by A1,FUNCT_4:34
    .= DecIC(p,k) +* d by FUNCT_4:14;
end;

theorem
  for p being PartState of S,k being Nat holds
  Start-At(IC p-'k,S) c= DecIC (p,k)
proof
  let p be PartState of S, k be Nat;
A1: IC DecIC(p,k) = IC p -' k by Th65;
A2: IC S in dom (DecIC(p,k)) by Th64;
A3: Start-At(IC p-'k,S) = {[IC S,IC p -' k]} & [IC S,IC p -' k] in
  DecIC(p,k) by A2,A1,FUNCT_1:def 2,FUNCT_4:82;
  for x being object st x in Start-At(IC p-'k,S)
    holds x in DecIC (p,k) by A3,TARSKI:def 1;
 hence thesis by TARSKI:def 3;
end;

theorem
 for p being PartState of S, k being Nat st IC S in dom p
  holds DecIC( p,k) = DataPart p +* Start-At ((IC p) -'k,S)
 proof let p be PartState of S, k being Nat;
A1: dom Start-At ((IC p) -'k,S) = {IC S}
     .= dom Start-At (IC p,S);
  assume
A2: IC S in dom p;
  thus DecIC( p,k)
     = DataPart p +* Start-At (IC p,S) +* Start-At ((IC p) -'k,S) by A2,Th26
    .= DataPart p +* Start-At ((IC p) -'k,S) by A1,FUNCT_4:74;
 end;

registration
  let N,S;
  let s be State of S, k be Nat;
  cluster DecIC(s,k) -> total;
  coherence;
end;

theorem
 for p being PartState of S, i,j being Nat
 holds DecIC(DecIC(p,i),j) = DecIC(p,i+j)
 proof let p be PartState of S, i,j being Nat;
  thus DecIC(DecIC(p,i),j)
        = p +* Start-At(IC p-'i,S) +* Start-At(IC p -' i -' j,S) by Th65
       .= p +* Start-At(IC p-'i,S) +* Start-At(IC p -' (i + j),S) by NAT_2:30
       .= DecIC(p,i+j) by FUNCT_4:114;
 end;

theorem
 for p being PartState of S, j,k being Nat
 holds DecIC(p +* Start-At(j,S),k) = p +* Start-At(j-'k,S)
proof
 let p be PartState of S, j,k be Nat;
 thus DecIC(p +* Start-At(j,S),k)
   = p +* Start-At(IC(p +* Start-At(j,S))-'k,S) by FUNCT_4:114
  .= p +* Start-At(j-'k,S) by Th16;
end;

theorem
 for s being State of S, k being Nat st k <= IC s
 holds IC DecIC(s,k) + k = IC s
proof
 let s be State of S, k be Nat such that
A1: k <= IC s;
 thus IC DecIC(s,k) + k = IC s -' k + k by Th65
    .= IC s by A1,XREAL_1:235;
end;

theorem Th72:
 for p,q being PartState of S, k being Nat st IC S in dom q
  holds DecIC(p+*q,k) = p +* DecIC(q,k)
proof let p,q be PartState of S, k be Nat;
  assume IC S in dom q;
   then IC(p+*q) = IC q by FUNCT_4:13;
 hence DecIC(p+*q,k) = p +* DecIC(q,k) by FUNCT_4:14;
end;

theorem Th73:
 for p being PartState of S, k being Nat st IC S in dom p
  holds DecIC(IncIC(p,k),k) = p
proof let p be PartState of S, k be Nat such that
A1: IC S in dom p;
 thus DecIC(IncIC(p,k),k)
     = IncIC(p,k) +* Start-At(IC p + k -'k,S) by Th53
    .= IncIC(p,k) +* Start-At(IC p, S) by NAT_D:34
    .= p +* Start-At(IC p, S) by Th36
    .= p by A1,FUNCT_4:7,98;
end;

theorem
 for p,q being PartState of S, k being Nat st IC S in dom q
  holds DecIC(p+*IncIC(q,k),k) = p +* q
proof let p,q be PartState of S, k being Nat such that
A1: IC S in dom q;
  IC S in dom IncIC(q,k) by Th52;
 hence DecIC(p+*IncIC(q,k),k) = p +* DecIC(IncIC(q,k),k) by Th72
      .= p +* q by A1,Th73;
end;

registration let N,S; let k be Nat;
 let p be k-started PartState of S;
 cluster DecIC(p,k) -> 0-started;
 coherence
  proof
   thus IC S in dom DecIC(p,k) by Th64;
   thus IC DecIC(p,k) = IC p -' k by Th65
         .= k -' k by Def11
         .= 0 by XREAL_1:232;
  end;
end;

begin :: Finite Partial States

registration
  let N;
  let S be IC-Ins-separated non empty
    with_non-empty_values Mem-Struct over N;
  let l be Nat;
  cluster Start-At(l,S) -> finite;
  correctness;
end;

definition let N;
  let S be Mem-Struct over N;
  mode FinPartState of S is finite PartState of S;
end;

registration
  let N;
  let S be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N,
      l be Nat;
  cluster l-started for FinPartState of S;
  existence
  proof
    take Start-At(l,S);
    thus thesis;
  end;
end;

registration
  let N;
  let S be Mem-Struct over N;
  let p be FinPartState of S;
  cluster DataPart p -> finite;
  coherence;
end;

registration let N,S;
  let p be FinPartState of S;
  cluster Initialize p -> finite;
  coherence;
end;

registration let N,S;
  let p be FinPartState of S, k be Nat;
  cluster IncIC(p,k) -> finite;
  coherence;
end;

registration let N,S;
  let p be FinPartState of S, k be Nat;
  cluster DecIC(p,k) -> finite;
  coherence;
end;

definition
  let N;
  let S be with_non-empty_values Mem-Struct over N;
  func FinPartSt S -> Subset of sproduct the_Values_of S equals
  { p where p is Element of sproduct the_Values_of S: p is finite };
  coherence
  proof
    defpred P[set] means $1 is finite;
    { p where p is Element of sproduct the_Values_of S: P[p] } c=
    sproduct the_Values_of S from FRAENKEL:sch 10;
    hence thesis;
  end;
end;

theorem Th75:
 for S be with_non-empty_values Mem-Struct over N
 for p being FinPartState of S holds p in FinPartSt S
proof
  let S be with_non-empty_values Mem-Struct over N;
  let p be FinPartState of S;
  p in sproduct the_Values_of S by CARD_3:103;
  hence thesis;
end;

registration
  let N;
  let S be with_non-empty_values Mem-Struct over N;
  cluster FinPartSt S -> non empty;
  coherence by Th75;
end;

theorem
  for S being with_non-empty_values Mem-Struct over N,
      p being Element of FinPartSt S holds
  p is FinPartState of S
proof
  let S be with_non-empty_values Mem-Struct over N;
  let p be Element of FinPartSt S;
  p in FinPartSt S;
  then ex q being Element of sproduct the_Values_of S st
  q = p & q is finite;
  hence thesis;
end;

definition
  let N,S;
  let IT be PartFunc of FinPartSt S,FinPartSt S;
  attr IT is data-only means
  for p being PartState of S st p in dom IT holds p is data-only &
   for q being PartState of S st q = IT.p holds q is data-only;
end;

registration let N,S;
  cluster data-only for PartFunc of FinPartSt S, FinPartSt S;
  existence
  proof
    reconsider f = {} as PartFunc of FinPartSt S, FinPartSt S by RELSET_1:12;
    take f;
    let p being PartState of S;
    thus thesis;
  end;
end;

begin :: Addenda

theorem
  for A being non empty with_non-empty_values Mem-Struct over N,
      s being State of A, o being Object of A holds s.o in Values o
proof
  let A be non empty with_non-empty_values Mem-Struct over N,
      s be State of A, o be Object of A;
  dom s = the carrier of A by PARTFUN1:def 2;
  hence thesis by FUNCT_1:def 14;
end;

theorem Th78:
  for A being IC-Ins-separated non empty with_non-empty_values
        Mem-Struct over N
  for s1,s2 being State of A st IC s1= IC s2 & DataPart s1 =
  DataPart s2 holds s1=s2
proof
  let A be IC-Ins-separated non empty with_non-empty_values Mem-Struct over N;
   set D = Data-Locations A;
  let s1,s2 be State of A;
  assume that
A1: IC s1= IC s2 and
A2: DataPart s1 = DataPart s2;
A3: dom s2 ={IC A} \/ D by Th13;
A4: dom s1 ={IC A} \/ D by Th13;
  then s1|{IC A} = s2|{IC A} by A1,A3,GRFUNC_1:29;
  then s1|({IC A} \/ D) = s2| ({IC A} \/ D) by A2,RELAT_1:150;
  then s1|({IC A} \/ D) = s2| ({IC A} \/ D);
  hence s1=s2 | dom s2 by A4,A3
    .=s2;
end;

theorem
  for s being State of S, l being Nat
  holds DataPart s = DataPart(s +* Start-At(l,S))
proof
  let s be State of S;
  let l be Nat;
  thus DataPart s =  DataPart s +* {}
      .=  DataPart s +* DataPart Start-At(l,S) by Th20
      .= DataPart(s +* Start-At(l,S))by FUNCT_4:71;
end;

theorem
  for s1,s2 be State of S holds
  DataPart s1 = DataPart s2 implies
    Initialize s1 =  Initialize s2
proof
  let s1,s2 be State of S;
  assume
A1: DataPart s1 = DataPart s2;
  set S1 = Initialize s1, S2 = Initialize s2;
A2: IC S1 =  0 & IC S2 =  0 by Th47;
  DataPart S1 = DataPart s1 by Th45
    .= DataPart S2 by A1,Th45;
  hence thesis by A2,Th78;
end;

theorem
  the_Values_of Trivial-Mem N = 0 .--> NAT by Lm1;

:: from SCMFSA9A

definition let N,S;
  let f be Function of product the_Values_of S, NAT;
  attr f is on_data_only means
  for s1, s2 being State of S st DataPart s1 = DataPart s2
  holds f.s1 = f.s2;
end;

theorem
  for d being data-only PartState of S holds
  d +* Start-At(k,S) = Start-At(k,S) +* d
proof
  let d be data-only PartState of S;
  d tolerates Start-At(k,S) by Th23;
  hence thesis by FUNCT_4:34;
end;