:: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA}
::  by Noriko Asamoto
::
:: Received October 29, 1997
:: Copyright (c) 1997-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, FSM_1, SCMFSA_2, CAT_1, AMI_1, SCMFSA8A,
      XXREAL_0, CIRCUIT2, FUNCT_4, CARD_1, RELAT_1, ARYTM_3, AMISTD_2, GRAPHSP,
      AMI_3, EXTPRO_1, TARSKI, FUNCT_1, ARYTM_1, SCMFSA6C, FUNCOP_1, SCMFSA6A,
      SCMFSA6B, MSUALG_1, SCMFSA7B, SF_MASTR, STRUCT_0, NAT_1, SCMFSA8B,
      SCMFSA8C, COMPOS_1, PARTFUN1, RELOC, SCMPDS_4, AMISTD_1, TURING_1,
      SCMFSA_9;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, NAT_1, FUNCOP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, FUNCT_7,
      PBOOLE, VALUED_1, AFINSQ_1, STRUCT_0, COMPOS_0, COMPOS_1, COMPOS_2,
      MEMSTR_0, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, SF_MASTR, SCMFSA6A,
      SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, NAT_D, XXREAL_0,
      SCMFSA_M, SCMFSA_X;
 constructors DOMAIN_1, XXREAL_0, REAL_1, SCMFSA6A, SF_MASTR, SCMFSA6B,
      SCMFSA6C, SCMFSA8A, SCMFSA8B, AMISTD_2, NAT_D, AMI_3, RELSET_1, PRE_POLY,
      SCMFSA7B, AMISTD_1, PBOOLE, SCMFSA_7, MEMSTR_0, WELLORD2, INT_2,
      SCMFSA_2, VALUED_1, SCMFSA_M, FUNCT_7, SCMFSA_X, AMISTD_4, COMPOS_2;
 registrations FUNCOP_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6A, SCMFSA6B,
      SCMFSA6C, SCMFSA7B, ORDINAL1, AFINSQ_1, SCMFSA10, COMPOS_1, EXTPRO_1,
      FUNCT_4, MEMSTR_0, STRUCT_0, AMI_3, COMPOS_0, SCMFSA_M, AMISTD_1,
      SCMFSA_X, COMPOS_2, VALUED_1;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin :: Preliminaries

reserve m for Nat;
reserve P,PP,P1,P2 for Instruction-Sequence of SCM+FSA;

theorem :: SCMFSA8C:1
  for s being State of SCM+FSA,I being initial Program of SCM+FSA
   st I is_pseudo-closed_on s,P
  for k being Nat st
    for n being Nat st n <= k
     holds IC Comput(P +* I,Initialize s,n) in dom I
  holds k < pseudo-LifeSpan(s,P,I);

theorem :: SCMFSA8C:2
  for I,J being Program of SCM+FSA, k being Nat
     st card I <= k & k < card I + card J
  for i being Instruction of SCM+FSA st i = J.(k -' card I)
   holds (I ";" J). k = IncAddr(i,card I);

theorem :: SCMFSA8C:3
  for s being State of SCM+FSA, I being Program of SCM+FSA holds
  IExec(I,P,s) = IExec(I,P,Initialized s);

::$CT

theorem :: SCMFSA8C:5
  for I being Program of SCM+FSA st
   for s being State of SCM+FSA, P holds I is_halting_on Initialized s,P
  holds Initialize((intloc 0).-->1) is I-halted;

theorem :: SCMFSA8C:6
  for I being Program of SCM+FSA holds (for s being State of
  SCM+FSA, P holds I is_halting_on Initialized s,P)
   implies Initialize((intloc 0).-->1) is I-halted;

::$CT 5

theorem :: SCMFSA8C:12
  for s being State of SCM+FSA, i being Instruction of SCM+FSA st
  InsCode i in {0,6,7,8} holds DataPart Exec(i,s) = DataPart s;

::$CT

theorem :: SCMFSA8C:14
  for s being State of SCM+FSA holds IExec(Stop SCM+FSA,P,s) = Initialized s;

::$CT

theorem :: SCMFSA8C:16
  for s1 being 0-started State of SCM+FSA,
      s2 being State of SCM+FSA,I being really-closed Program of SCM+FSA
   st I c= P1
  for n being Nat st
   Reloc(I,n) c= P2 & IC s2 =  n & DataPart s1 = DataPart s2
  for i being Nat holds
   IC Comput(P1, s1,i) + n = IC Comput(P2, s2,i) &
   IncAddr(CurInstr(P1,Comput(P1,s1,i)),n)
        = CurInstr(P2,Comput(P2,s2,i)) &
  DataPart Comput(P1, s1,i) = DataPart Comput(P2,s2,i);

theorem :: SCMFSA8C:17
  for s1,s2 being 0-started State of SCM+FSA,
      I being really-closed Program of SCM+FSA
   st I c= P1 & I c= P2 & DataPart s1 = DataPart s2
  for i being Nat
  holds IC Comput(P1, s1,i) = IC Comput(P2, s2,i) &
  CurInstr(P1,Comput(P1,s1,i)) = CurInstr(P2,Comput(P2,s2,i)) &
  DataPart Comput(P1, s1,i) = DataPart Comput(P2,s2,i);

theorem :: SCMFSA8C:18
  for s1,s2 being 0-started State of SCM+FSA,
      I being really-closed Program of SCM+FSA
    st I is_halting_on s1,P1 & I c= P1 & I c= P2 &
       DataPart s1 = DataPart s2
  holds LifeSpan(P1,s1) = LifeSpan(P2,s2);

theorem :: SCMFSA8C:19
  for s1,s2 being State of SCM+FSA,I being really-closed Program of SCM+FSA st
  s1.intloc 0 = 1 & I is_halting_on s1,P1 &
   ((for a being read-write Int-Location holds s1.a = s2.a) &
  for f being FinSeq-Location holds s1.f = s2.f)
  holds DataPart IExec(I,P1,s1) = DataPart IExec(I,P2,s2);

theorem :: SCMFSA8C:20
  for s1,s2 being State of SCM+FSA,
      I being really-closed Program of SCM+FSA
   st s1.intloc 0 = 1 & I is_halting_on s1,P1 &
      DataPart s1 = DataPart s2
  holds DataPart IExec(I,P1,s1) = DataPart IExec(I,P2,s2);

theorem :: SCMFSA8C:21
  for s being State of SCM+FSA,
      I being Program of SCM+FSA
       st I is_pseudo-closed_on s,P
 holds I is_pseudo-closed_on Initialize s,P+*I &
   pseudo-LifeSpan(s,P,I) = pseudo-LifeSpan(Initialize s,P+*I,I);

theorem :: SCMFSA8C:22
  for s1 being 0-started State of SCM+FSA,
      s2 being State of SCM+FSA, I being Program of SCM+FSA st
   I c= P1 & I is_pseudo-closed_on s1,P1
   for n being Nat st Reloc(I,n) c= P2 &
    IC s2 =  n & DataPart s1 =
  DataPart s2 holds ((for i being Nat
   st i < pseudo-LifeSpan(s1,P1,I)
  holds IncAddr(CurInstr(P1,Comput(P1,s1,i)),n)
   = CurInstr(P2,Comput(P2,s2,i))) &
for i being Nat st i <= pseudo-LifeSpan(s1,P1,I)
holds IC Comput(P1, s1,i) + n = IC Comput(P2, s2,i) &
  DataPart Comput(P1, s1,i) = DataPart Comput(P2, s2,i));

theorem :: SCMFSA8C:23
  for s1,s2 being State of SCM+FSA, I being Program of SCM+FSA st
  DataPart s1 = DataPart s2 holds I is_pseudo-closed_on s1,P1 implies I
  is_pseudo-closed_on s2,P2;

theorem :: SCMFSA8C:24
  for s being State of SCM+FSA, I being Program of SCM+FSA st s.
intloc 0 = 1 holds I is_pseudo-closed_on s,P iff
I is_pseudo-closed_on Initialized s,P;

theorem :: SCMFSA8C:25
  for a being Int-Location, I,J being MacroInstruction of SCM+FSA holds
:::   0 in dom if=0(a,I,J) &
   1 in dom if=0(a,I,J) &
:::    0 in dom  if>0(a,I,J) &
1 in dom if>0(a,I,J);

theorem :: SCMFSA8C:26
  for a being Int-Location, I,J being MacroInstruction of SCM+FSA
   holds
  if=0(a,I,J). 0 = a =0_goto  (card J + 3) & if=0(a,I,J). 1 =
goto  2 & if>0(a,I,J). 0 = a >0_goto  (card J + 3) & if>0(a,I
  ,J). 1 = goto  2;

theorem :: SCMFSA8C:27
  for a being Int-Location, I,J being MacroInstruction of SCM+FSA, n being
Element of NAT st n < card I + card J + 3 holds n in dom if=0(a,I,J) & if=0(a,I
  ,J).n <> halt SCM+FSA;

theorem :: SCMFSA8C:28
  for a being Int-Location, I,J being MacroInstruction of SCM+FSA, n being
Element of NAT st n < card I + card J + 3 holds n in dom if>0(a,I,J) & if>0(a,I
  ,J).n <> halt SCM+FSA;

theorem :: SCMFSA8C:29
  for s being State of SCM+FSA, I being Program of SCM+FSA st
  Directed I is_pseudo-closed_on s,P
   holds I ";" Stop SCM+FSA is_halting_on s,P &
   LifeSpan(P +* (I ";" Stop SCM+FSA),
         Initialize s) =
   pseudo-LifeSpan(s,P,Directed I) &
  (for n being Nat st n < pseudo-LifeSpan(s,P,Directed I) holds
   IC Comput(P +* I, (Initialize s),n)
     = IC Comput(P +* (I ";" Stop SCM+FSA),
     (Initialize s),n)) &
for n being Nat st n <= pseudo-LifeSpan(s,P,Directed I)
 holds DataPart Comput(P +* I, (Initialize s),n)
   = DataPart Comput(P+* (I ";" Stop SCM+FSA),
    Initialize s,n);

theorem :: SCMFSA8C:30
  for s being State of SCM+FSA, I being Program of SCM+FSA st
  Directed I is_pseudo-closed_on s,P holds
   DataPart Result(P +* (I ";" Stop SCM+FSA),
   Initialize s) =
  DataPart Comput(P +* I, (Initialize s),
  pseudo-LifeSpan(s,P,Directed I));

theorem :: SCMFSA8C:31
  for s being State of SCM+FSA, I being Program of SCM+FSA st s.intloc 0
= 1 & Directed I is_pseudo-closed_on s,P
 holds DataPart IExec(I ";" Stop SCM+FSA,P,s)
  = DataPart Comput(P +* I, (Initialize s),
pseudo-LifeSpan(s,P,Directed I));

theorem :: SCMFSA8C:32
  for I,J being MacroInstruction of SCM+FSA,a being Int-Location
   holds if=0
  (a,I,J). (card I + card J + 3) = halt SCM+FSA;

theorem :: SCMFSA8C:33
  for I,J being MacroInstruction of SCM+FSA,a being Int-Location holds if>0
  (a,I,J). (card I + card J + 3) = halt SCM+FSA;

theorem :: SCMFSA8C:34
  for I,J being MacroInstruction of SCM+FSA,a being Int-Location holds if=0
  (a,I,J). (card J + 2) = goto  (card I + card J + 3);

theorem :: SCMFSA8C:35
  for I,J being MacroInstruction of SCM+FSA,a being Int-Location holds if>0
  (a,I,J). (card J + 2) = goto  (card I + card J + 3);

::$CT

theorem :: SCMFSA8C:37
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
      a being read-write Int-Location st
  s.a = 0 & Directed I is_pseudo-closed_on s,P
    holds if=0(a,I,J) is_halting_on s,P &
    LifeSpan(P +* if=0(a,I,J),Initialize s)
   = LifeSpan(P +* (I ";" Stop SCM+FSA),
       Initialize s) + 1;

theorem :: SCMFSA8C:38
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
      a being
  read-write Int-Location st s.intloc 0 = 1 & s.a = 0 & Directed I
  is_pseudo-closed_on s,P holds DataPart IExec(if=0(a,I,J),P,s)
   = DataPart IExec(I ";" Stop SCM+FSA,P,s);

theorem :: SCMFSA8C:39
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
  being read-write Int-Location
   st s.a > 0 & Directed I is_pseudo-closed_on s,P
holds if>0(a,I,J) is_halting_on s,P &
 LifeSpan(P+* if>0(a,I,J),Initialize s)
   = LifeSpan(P +* (I ";" Stop SCM+FSA),Initialize s) + 1;

theorem :: SCMFSA8C:40
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
  being read-write Int-Location st s.intloc 0 = 1 & s.a > 0 & Directed I
  is_pseudo-closed_on s,P holds DataPart IExec(if>0(a,I,J),P,s)
   = DataPart IExec(I ";" Stop SCM+FSA,P,s);

theorem :: SCMFSA8C:41
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
  being read-write Int-Location st s.a <> 0 &
   Directed J is_pseudo-closed_on s,P
holds if=0(a,I,J) is_halting_on s,P &
    LifeSpan(P +* if=0(a,I,J),Initialize s)
    = LifeSpan(P +* (J ";" Stop SCM+FSA),
      Initialize s) + 3;

theorem :: SCMFSA8C:42
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
      a being
  read-write Int-Location st s.intloc 0 = 1 & s.a <> 0 & Directed J
  is_pseudo-closed_on s,P holds
   DataPart IExec(if=0(a,I,J),P,s) = DataPart IExec(J ";" Stop SCM+FSA,P,s);

theorem :: SCMFSA8C:43
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
  being read-write Int-Location st s.a <= 0 &
   Directed J is_pseudo-closed_on s,P
holds if>0(a,I,J) is_halting_on s,P &
  LifeSpan(P +* if>0(a,I,J),s +* (Start-At(0,SCM+FSA))) =
  LifeSpan(P +* (J ";" Stop SCM+FSA),
  Initialize s) + 3;

theorem :: SCMFSA8C:44
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
  being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 & Directed J
  is_pseudo-closed_on s,P holds
   DataPart IExec(if>0(a,I,J),P,s) = DataPart IExec(J
  ";" Stop SCM+FSA,P,s);

theorem :: SCMFSA8C:45
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
      a being
  read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J
  is_pseudo-closed_on s,P holds
if=0(a,I,J)
  is_halting_on s,P;

theorem :: SCMFSA8C:46
  for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a being
  read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J
  is_pseudo-closed_on s,P holds if>0(a,I,J) is_halting_on s,P;

theorem :: SCMFSA8C:47
  for I being Program of SCM+FSA, a being Int-Location holds I
  does not destroy a implies Directed I does not destroy a;

theorem :: SCMFSA8C:48
  for i being Instruction of SCM+FSA, a being Int-Location holds i
  does not destroy a implies Macro i does not destroy a;

theorem :: SCMFSA8C:49
  for a being Int-Location holds halt SCM+FSA does not refer a;

theorem :: SCMFSA8C:50
  for a,b,c being Int-Location holds a <> b implies AddTo(c,b)
  does not refer a;

theorem :: SCMFSA8C:51
  for i being Instruction of SCM+FSA, a being Int-Location holds
  i does not refer a implies Macro i does not refer a;

theorem :: SCMFSA8C:52
  for I,J being Program of SCM+FSA, a being Int-Location holds I
  does not destroy a & J does not destroy a implies I ";" J does not destroy a;

theorem :: SCMFSA8C:53
  for J being Program of SCM+FSA, i being Instruction of SCM+FSA,
a being Int-Location st i does not destroy a & J does not destroy a holds i ";"
  J does not destroy a;

theorem :: SCMFSA8C:54
  for I being Program of SCM+FSA, j being Instruction of SCM+FSA, a
being Int-Location st I does not destroy a & j does not destroy a holds I ";" j
  does not destroy a;

theorem :: SCMFSA8C:55
  for i,j being Instruction of SCM+FSA, a being Int-Location st i
  does not destroy a & j does not destroy a holds i ";" j does not destroy a;

theorem :: SCMFSA8C:56
  for a being Int-Location holds Stop SCM+FSA does not destroy a;

theorem :: SCMFSA8C:57
  for a being Int-Location, l being Nat
   holds Goto l does not destroy a;

theorem :: SCMFSA8C:58
  for s being State of SCM+FSA, I being Program of SCM+FSA st I
  is_halting_on Initialized s,P holds
   (for a being read-write Int-Location holds
IExec(I,P,s).a = Comput(P +* I,Initialize Initialized s,
 (LifeSpan(P +* I, Initialize Initialized s))).a) &
  for f being FinSeq-Location
  holds IExec(I,P,s).f = Comput(P +* I,Initialize Initialized s,
  LifeSpan(P +* I,Initialize Initialized s)).f;

theorem :: SCMFSA8C:59
  for s being State of SCM+FSA, I being parahalting Program of
  SCM+FSA, a being read-write Int-Location holds IExec(I,P,s).a = Comput(
P +* I,
  Initialize Initialized s,
  (LifeSpan(P +* I,Initialize Initialized s))).a;

theorem :: SCMFSA8C:60
  for s being State of SCM+FSA,
      I being really-closed Program of SCM+FSA, a
  being Int-Location,k being Element of NAT
   st I is_halting_on Initialized s,P & I does not destroy a
 holds IExec(I,P,s).a = Comput(P +* I, (Initialize Initialized s),k).a;

theorem :: SCMFSA8C:61
  for s being State of SCM+FSA,
      I being parahalting really-closed Program of
  SCM+FSA, a being Int-Location,k being Element of NAT st I does not destroy a
holds IExec(I,P,s).a = Comput(P +* I,(Initialize Initialized s),k).a;

theorem :: SCMFSA8C:62
  for s being State of SCM+FSA,
      I being parahalting really-closed Program of
  SCM+FSA, a being Int-Location st I does not destroy a
   holds IExec(I,P,s).a = (Initialized s).a;

theorem :: SCMFSA8C:63
  for s being State of SCM+FSA, I being keeping_0 Program of
  SCM+FSA st I is_halting_on Initialized s,P
   holds IExec(I,P,s).intloc 0 = 1 & for k
being Nat holds Comput(P +* I,
(Initialize Initialized s),k).intloc 0 = 1;

theorem :: SCMFSA8C:64
  for s being State of SCM+FSA, I being Program of SCM+FSA, a
being Int-Location st I does not destroy a holds for k being Element of NAT st
IC Comput(P +* I, (Initialize s),k) in dom I
holds Comput(P +* I,
  (Initialize s),k + 1).a =
   Comput(P +* I, (Initialize s),k).a;

theorem :: SCMFSA8C:65
  for s being State of SCM+FSA, I being Program of SCM+FSA, a
being Int-Location st I does not destroy a for m being Nat st
(for n being Nat st n < m
 holds IC Comput(P +* I, (Initialize s),n) in dom I)
 for n being Nat st n <= m holds
  Comput(P +* I, (Initialize s),n).a = s.a;

theorem :: SCMFSA8C:66
  for s being State of SCM+FSA, I being good Program of SCM+FSA
  for m being Nat st (for n being Nat st n < m holds IC
  Comput(P +* I, (Initialize s),n) in dom I) holds
  for n being Nat st n <= m
     holds Comput(P +* I, (Initialize s),n).intloc 0 = s.intloc 0;

registration
 cluster good keeping_0 really-closed parahalting
     for MacroInstruction of SCM+FSA;
end;

theorem :: SCMFSA8C:67
  for s being State of SCM+FSA,
      I being good really-closed Program of SCM+FSA st
  I is_halting_on Initialized s,P
   holds IExec(I,P,s).intloc 0 = 1 & for k being Nat
  holds Comput(P +* I, (Initialize Initialized s),k).intloc 0 = 1;

theorem :: SCMFSA8C:68
  for s being State of SCM+FSA,
      I being good really-closed Program of SCM+FSA
 for k being Nat
  holds Comput(P +* I, Initialize s,k).intloc 0 = s.intloc 0;

theorem :: SCMFSA8C:69
  for P
  for s being State of SCM+FSA,
      I being keeping_0 parahalting really-closed
  Program of SCM+FSA, a being read-write Int-Location st I does not destroy a
  holds Comput(P +* (I ";" SubFrom(a,intloc 0)),
   Initialize Initialized s,
   LifeSpan(P +* (I ";" SubFrom(a,intloc 0)),
  Initialize Initialized s)).a = s.a - 1;

theorem :: SCMFSA8C:70
  for i being Instruction of SCM+FSA st i does not destroy intloc
  0 holds Macro i is good;

theorem :: SCMFSA8C:71
  for s1,s2 being State of SCM+FSA,
      I being really-closed Program of SCM+FSA st
I is_halting_on s1,P1 & DataPart s1 = DataPart s2
  for k being Nat holds
    Comput(P1 +* I,Initialize s1,k)
   =  Comput(P2 +* I,Initialize s2,k)
   & CurInstr(P1 +* I,Comput(P1 +* I,Initialize s1,k))
    = CurInstr(P2 +* I,Comput(P2 +* I,Initialize s2,k));

theorem :: SCMFSA8C:72
  for s1,s2 being State of SCM+FSA,
      I being really-closed Program of SCM+FSA
    st I is_halting_on s1,P1 & DataPart s1 = DataPart s2
   holds
  LifeSpan(P1 +* I,Initialize s1) =
  LifeSpan(P2 +* I,Initialize s2) &
   Result(P1 +* I,Initialize s1)
  =  Result(P2 +* I,Initialize s2);

theorem :: SCMFSA8C:73
  for s1,s2 being 0-started State of SCM+FSA,
      I being really-closed Program of SCM+FSA st
I is_halting_on s1,P1 &
  I c= P1 & I c= P2 &
   ex k being Nat st  Comput(P1, s1,k) =  s2
  holds  Result(P1,s1) =  Result(P2,s2);

begin :: loop

::$CD

::$CT 8

begin :: Times

definition
  let a be Int-Location;
  let I be MacroInstruction of SCM+FSA;
  func Times(a,I) -> Program of SCM+FSA equals
:: SCMFSA8C:def 2
  while>0 (a,I ";" SubFrom(a, intloc 0));
end;

registration
  let a be Int-Location;
  let I be MacroInstruction of SCM+FSA;
  cluster Times(a,I) -> halt-ending unique-halt;
end;

::$CT 6

theorem :: SCMFSA8C:88
  for I,J being MacroInstruction of SCM+FSA, a,c being Int-Location st I
does not destroy c & J does not destroy c holds if=0(a,I,J) does not destroy c
  & if>0(a,I,J) does not destroy c;


::$CT 2

theorem :: SCMFSA8C:91
  for s being State of SCM+FSA,
      I being good parahalting really-closed Program
  of SCM+FSA, a being read-write Int-Location st I does not destroy a
holds IExec(I ";" SubFrom(a,intloc 0),P,s).a = s.a - 1;

begin :: Example

reserve aa,bb for Int-Location;

theorem :: SCMFSA8C:92
 for I being MacroInstruction of SCM+FSA holds
  I does not destroy aa implies while>0(bb, I) does not destroy aa;

theorem :: SCMFSA8C:93
  for I being MacroInstruction of SCM+FSA
  for a,b being Int-Location st
  I does not destroy b & a<>b holds Times(a,I) does not destroy b;

theorem :: SCMFSA8C:94
  for a being Int-Location,I being MacroInstruction of SCM+FSA holds
  card Times(a,I) = card I + 7;

reserve s for State of SCM+FSA,
  a for Int-Location,
  I for Program of SCM+FSA,
  p for Instruction-Sequence of SCM+FSA;

theorem :: SCMFSA8C:95
 for I being really-closed Program of SCM+FSA
  st I is_halting_on Initialized s,p & I does not destroy a
 holds IExec(I,p,s).a = (Initialized s).a;

theorem :: SCMFSA8C:96
 for I,J being MacroInstruction of SCM+FSA st
  I does not destroy aa & J does not destroy aa
 holds I ';' J does not destroy aa;

theorem :: SCMFSA8C:97
 for I being MacroInstruction of SCM+FSA st I does not destroy aa
  holds I ';' goto  0 does not destroy aa;

theorem :: SCMFSA8C:98
 for I being MacroInstruction of SCM+FSA holds
  I does not destroy aa implies
  if>0(bb, I ';' goto 0) does not destroy aa;

theorem :: SCMFSA8C:99
 for I being MacroInstruction of SCM+FSA holds
  I does not destroy aa implies
  if=0(bb, I ';' goto 0) does not destroy aa;