:: Initialization Halting Concepts and Their Basic Properties of SCM+FSA
::  by JingChao Chen and Yatsuka Nakamura
::
:: Received June 17, 1998
:: Copyright (c) 1998-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, AMI_1, SCMFSA_2, FSM_1, SCMFSA6A, TARSKI,
      CIRCUIT2, RELAT_1, FUNCT_1, CARD_1, FUNCOP_1, FUNCT_4, XBOOLE_0,
      SCMFSA6B, NAT_1, XXREAL_0, ARYTM_3, AMI_3, SF_MASTR, GRAPHSP, MSUALG_1,
      AMISTD_2, STRUCT_0, VALUED_1, SCMFSA6C, SCMFSA7B, SCMFSA8B, ARYTM_1,
      SCMFSA8C, SCM_HALT, PARTFUN1, EXTPRO_1, RELOC, COMPOS_1, AMISTD_1,
      SFMASTR2, SCMFSA_9, FRECHET;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, CARD_3,
      NUMBERS, XCMPLX_0, RELAT_1, FINSEQ_1, FUNCT_1, PARTFUN1, FUNCT_4,
      FUNCT_7, PBOOLE, FUNCT_2, VALUED_1, NAT_1, NAT_D, STRUCT_0, MEMSTR_0,
      COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, FUNCOP_1,
      SCMFSA6B, SCMFSA6A, SF_MASTR, SCMFSA8B, SFMASTR1, SCMFSA8C, SCMFSA7B,
      SCMFSA_3, SCMFSA6C, XXREAL_0, SCMFSA_M, SCMFSA_X, SCMFSA_9, SCMFSA9A;
 constructors SFMASTR1, DOMAIN_1, XXREAL_0, REAL_1, SCM_1, SCMFSA_3, SCMFSA6A,
      SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, AMISTD_1,
      AMISTD_2, NAT_D, RELSET_1, VALUED_1, SCMFSA7B, SCMFSA_9, AMISTD_5,
      PBOOLE, PRE_POLY, MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, SCMFSA_X,
      SCMFSA9A, CARD_3;
 registrations XBOOLE_0, FUNCT_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6A,
      SCMFSA6C, SCMFSA7B, SCMFSA_9, ORDINAL1, RELAT_1, COMPOS_1, SFMASTR1,
      EXTPRO_1, SCMFSA_4, FUNCT_4, STRUCT_0, FUNCOP_1, MEMSTR_0, AMI_3,
      COMPOS_0, SCMFSA_M, SCMFSA8C, CARD_3, AMISTD_1, SCMFSA10, SCMFSA_X;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve m,n for Nat,
  I for Program of SCM+FSA,
  s,s1,s2 for State of SCM+FSA,
  a for Int-Location,
  f for FinSeq-Location,
  p,p1,p2 for Instruction-Sequence of SCM+FSA;

::$CD

definition
  let I be Program of SCM+FSA;
  attr I is InitHalting means
:: SCM_HALT:def 2

  for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s
  for P being Instruction-Sequence of SCM+FSA
   st I c= P
  holds P halts_on s;
  attr I is keepInt0_1 means
:: SCM_HALT:def 3

  for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s
  for p st I c= p
  for k being Nat holds (Comput(p,s,k)).intloc 0 = 1;
end;

::$CT

theorem :: SCM_HALT:2
  Macro halt SCM+FSA is InitHalting;

registration
  cluster InitHalting for Program of SCM+FSA;
end;

registration
  cluster parahalting -> InitHalting for Program of SCM+FSA;
end;

registration
  cluster keeping_0 -> keepInt0_1 for Program of SCM+FSA;
end;

::$CT

theorem :: SCM_HALT:4
  for I being InitHalting really-closed Program of SCM+FSA,
      a being read-write
  Int-Location holds not a in UsedILoc I implies (IExec(I,p,s)).a = s.a;

theorem :: SCM_HALT:5
  for I being InitHalting really-closed Program of SCM+FSA,
      f being FinSeq-Location
  holds not f in UsedI*Loc I implies (IExec(I,p,s)).f = s.f;

registration
  cluster InitHalting -> non empty for Program of SCM+FSA;
end;

theorem :: SCM_HALT:6
  for J being InitHalting really-closed Program of SCM+FSA
   st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1
  for n being Nat st
  Reloc(J,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 :: SCM_HALT:7
  for I being InitHalting really-closed Program of SCM+FSA st
   Initialize ((intloc 0) .--> 1) c= s1 &
   Initialize ((intloc 0) .--> 1) c= s2 &
   I c= p1 & I c= p2 &
    s1 =  s2
 for k being Nat holds
   Comput(p1,s1,k) =  Comput(p2,s2,k) &
  CurInstr(p1,Comput(p1,s1,k)) = CurInstr(p2,Comput(p2,s2,k));

theorem :: SCM_HALT:8
  for I being InitHalting really-closed Program of SCM+FSA
   st Initialize ((intloc 0) .--> 1) c= s1 &
     Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 &
    s1 =  s2
 holds LifeSpan(p1,s1) = LifeSpan(p2,
  s2) &  Result(p1,s1) =  Result(p2,s2);

registration
  cluster keeping_0 InitHalting for Program of SCM+FSA;
end;

registration
  cluster keepInt0_1 InitHalting for really-closed Program of SCM+FSA;
end;

theorem :: SCM_HALT:9
  for I being keepInt0_1 InitHalting Program of SCM+FSA holds
  IExec(I,p,s).intloc 0 = 1;

theorem :: SCM_HALT:10
  for I being really-closed Program of SCM+FSA, J being Program of
  SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p &
   p halts_on s
   for m st m <= LifeSpan(p,s) holds
   Comput(p,s,m) =  Comput(p+*(I ";" J),s,m);

theorem :: SCM_HALT:11
  for I being really-closed Program of SCM+FSA
   st p+*I halts_on s &
   Directed I c= p &
   Initialize ((intloc 0) .--> 1) c= s
   holds IC Comput(p, s,LifeSpan(p +* I,s) + 1) =  card I;

theorem :: SCM_HALT:12
  for I being really-closed Program of SCM+FSA
   st p+*I halts_on s & Directed I c= p &
 Initialize ((intloc 0) .--> 1) c= s
 holds DataPart Comput(p, s,LifeSpan(p +* I,s))
  = DataPart Comput(p,s,LifeSpan(p +* I,s) + 1);

theorem :: SCM_HALT:13
  for I being InitHalting really-closed Program of SCM+FSA st
    Initialize ((intloc 0) .--> 1) c= s & I c= p
  for k being Nat st k <= LifeSpan(p,s)
   holds CurInstr(p +* Directed I,
    Comput(p +* Directed I, s,k)) <> halt SCM+FSA;

theorem :: SCM_HALT:14
  for I being really-closed Program of SCM+FSA
   st p+*I halts_on Initialized s
   for J being Program of SCM+FSA, k being Nat
    st k <= LifeSpan(p +* I,Initialized s )
   holds  Comput(p +* I, (Initialized s),k)
    =  Comput(p +* (I ";" J), (Initialized s),k);

theorem :: SCM_HALT:15
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      J being InitHalting really-closed Program of SCM+FSA,
      s being State of SCM+FSA st
 Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p
  holds IC Comput(p, s,LifeSpan(p +* I,s) + 1) =  card I &
   DataPart Comput(p, s,LifeSpan(p +* I,s) + 1) =
    DataPart(Comput(p +* I, s,LifeSpan(p +* I,s))
       +* Initialize ((intloc 0) .--> 1)) &
  Reloc(J,card I) c= p &
  Comput(p, s,LifeSpan(p +* I,s) + 1).intloc 0 = 1 & p halts_on s &
   LifeSpan(p,s) = LifeSpan(p +* I,s) + 1 +
 LifeSpan(p +* I +* J,
Result(p +* I,s) +*Initialize ((intloc 0) .--> 1)) & (J is keeping_0 implies
(Result(p,s)).intloc 0 = 1);

registration
  let I be keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      J be InitHalting really-closed Program of SCM+FSA;
  cluster I ";" J -> InitHalting;
end;

theorem :: SCM_HALT:16
  for I being keepInt0_1 really-closed Program of SCM+FSA st p+*I halts_on s
  for J being really-closed Program of SCM+FSA st
   Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p
for k being Element of NAT holds (Comput(p +* I +* J,
(Result(p +* I,s) +* Initialize ((intloc 0) .--> 1)),k) +*
  Start-At (IC Comput(p +* I +* J, (
  Result(p +* I,s) +* Initialize ((intloc 0) .--> 1)),k) + card I,SCM+FSA))
  =  Comput(p +* (I ";" J), s,LifeSpan(p +* I,s)+1+k);

theorem :: SCM_HALT:17
  for I being keepInt0_1 really-closed Program of SCM+FSA
   st not p+*I halts_on Initialized s
 for J being Program of SCM+FSA, k being Nat
  holds  Comput(p +* I, Initialized s,k)
   =  Comput(p +* (I ";" J), Initialized s,k);

theorem :: SCM_HALT:18
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      J being InitHalting really-closed Program of SCM+FSA holds
   LifeSpan(p +* (I ";" J),Initialized s)
     = LifeSpan(p+*I,Initialized s) + 1 +
       LifeSpan(p +* I +* J,
           Result(p+*I,Initialized s)
            +*Initialize ((intloc 0) .--> 1));

theorem :: SCM_HALT:19
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      J being InitHalting really-closed Program of SCM+FSA holds
 IExec(I ";" J,p,s) = IncIC(IExec(J,p,IExec(I,p,s)),card I);

registration
  let i be sequential Instruction of SCM+FSA;
  cluster Macro i -> InitHalting;
end;

registration
  let i be sequential Instruction of SCM+FSA,
      J be parahalting really-closed Program of SCM+FSA;
  cluster i ";" J -> InitHalting;
end;

registration
  let i be keeping_0 sequential Instruction of SCM+FSA,
      J be InitHalting really-closed Program of SCM+FSA;
  cluster i ";" J -> InitHalting;
end;

registration
  let I, J be keepInt0_1 really-closed Program of SCM+FSA;
  cluster I ";" J -> keepInt0_1;
end;

registration
  let j be keeping_0 sequential Instruction of SCM+FSA,
      I be keepInt0_1 InitHalting really-closed Program of SCM+FSA;
  cluster I ";" j -> InitHalting keepInt0_1;
end;

registration
  let i be keeping_0 sequential Instruction of SCM+FSA,
      J be keepInt0_1 InitHalting really-closed Program of SCM+FSA;
  cluster i ";" J -> InitHalting keepInt0_1;
end;

registration
  let j be sequential Instruction of SCM+FSA,
      I be parahalting really-closed Program of SCM+FSA;
  cluster I ";" j -> InitHalting;
end;

registration
  let i,j be sequential Instruction of SCM+FSA;
  cluster i ";" j -> InitHalting;
end;

theorem :: SCM_HALT:20
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      J being InitHalting really-closed Program of SCM+FSA
   holds IExec(I ";" J,p,s).a = IExec(J,p,IExec(I,p,s)).a;

theorem :: SCM_HALT:21
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      J being InitHalting really-closed Program of SCM+FSA
 holds IExec(I ";" J,p,s).f = IExec(J,p,IExec(I,p,s)).f;

theorem :: SCM_HALT:22
  for I be keepInt0_1 InitHalting Program of SCM+FSA, s be State
  of SCM+FSA holds DataPart(Initialized IExec(I,p,s)) = DataPart IExec(I,p,s);

theorem :: SCM_HALT:23
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      j being sequential Instruction of SCM+FSA
  holds IExec(I ";" j,p,s).a = Exec(j,IExec(I,p,s)).a;

theorem :: SCM_HALT:24
  for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
      j being sequential Instruction of SCM+FSA
  holds IExec(I ";" j,p,s).f = Exec(j,IExec(I,p,s)).f;

 definition
   let I be Program of SCM+FSA;
   let s be State of SCM+FSA;
   let p;
    pred I is_halting_onInit s,p means
:: SCM_HALT:def 4
   p+*I halts_on Initialized s;
 end;

::$CD

::$CT

theorem :: SCM_HALT:26
  for I being Program of SCM+FSA holds I is InitHalting iff for s
  being State of SCM+FSA,p holds I is_halting_onInit s,p;

theorem :: SCM_HALT:27
  for s being State of SCM+FSA, I being really-closed Program of SCM+FSA, a
being Int-Location st I does not destroy a &
:::I is_closed_onInit s,p &
 Initialize ((intloc 0) .--> 1) c= s & I c= p
   holds for k being Nat holds Comput(p,s,k).a = s.a;

registration
  cluster InitHalting good for Program of SCM+FSA;
end;

registration
  cluster really-closed good -> keepInt0_1 for Program of SCM+FSA;
end;

registration
  cluster Stop SCM+FSA -> InitHalting good;
end;

theorem :: SCM_HALT:28
  for s being State of SCM+FSA, i being keeping_0 sequential
  Instruction of SCM+FSA, J being InitHalting really-closed Program of SCM+FSA,
   a being
  Int-Location holds IExec(i ";" J,p,s).a
   = IExec(J,p,Exec(i,Initialized s)).a;

theorem :: SCM_HALT:29
  for s being State of SCM+FSA, i being keeping_0 sequential
  Instruction of SCM+FSA, J being InitHalting really-closed Program of SCM+FSA,
   f being
  FinSeq-Location holds IExec(i ";" J,p,s).f
   = IExec(J,p,Exec(i,Initialized s)).f;

::$CT

theorem :: SCM_HALT:31
  for s being State of SCM+FSA, I being Program of SCM+FSA holds I
  is_halting_onInit s,p iff I is_halting_on Initialized s,p;

theorem :: SCM_HALT:32
  for I be Program of SCM+FSA, s be State of SCM+FSA holds IExec(I,p,s) =
  IExec(I,p,Initialized s);

theorem :: SCM_HALT:33
  for s being State of SCM+FSA,
   I being really-closed MacroInstruction of SCM+FSA,
   J being MacroInstruction of SCM+FSA,
  a being read-write Int-Location st s.a = 0 &
:::I is_closed_onInit s,p &
  I is_halting_onInit s,p holds
:::if=0(a,I,J) is_closed_onInit s,p &
    if=0(a,I,J) is_halting_onInit s,p;

theorem :: SCM_HALT:34
  for s being State of SCM+FSA,
      I being really-closed MacroInstruction of SCM+FSA,
      J being MacroInstruction of SCM+FSA,
      a being read-write Int-Location st s.a = 0 &
   I is_halting_onInit s,p
  holds IExec(if=0(a,I,J),p,s)
     = IExec(I,p,s) +* Start-At( (card I + card J + 3),SCM+FSA);

theorem :: SCM_HALT:35
  for s being State of SCM+FSA,
      I,J being really-closed MacroInstruction of SCM+FSA,
      a being read-write Int-Location st s.a <> 0
:::& J is_closed_onInit s,p
   & J  is_halting_onInit s,p
 holds
:::if=0(a,I,J) is_closed_onInit s,p &
if=0(a,I,J)
  is_halting_onInit s,p;

theorem :: SCM_HALT:36
  for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write
  Int-Location holds for s being State of SCM+FSA st s.a <> 0 &
:::Jis_closed_onInit s,p &
  J is_halting_onInit s,p
 holds IExec(if=0(a,I,J),p,s)
  = IExec(J,p,s) +* Start-At((card I + card J + 3),SCM+FSA);

theorem :: SCM_HALT:37
  for s being State of SCM+FSA,
      I,J being really-closed InitHalting MacroInstruction of
SCM+FSA, a being read-write Int-Location holds if=0(a,I,J) is InitHalting & (s.
  a = 0 implies IExec(if=0(a,I,J),p,s) = IExec(I,p,s) +* Start-At((card I +
card J + 3),SCM+FSA)) &
 (s.a <> 0 implies IExec(if=0(a,I,J),p,s) = IExec(J,p,s) +* Start-At(
   (card I + card J + 3),SCM+FSA));

theorem :: SCM_HALT:38
  for s being State of SCM+FSA,
      I,J being InitHalting really-closed MacroInstruction of SCM+FSA,
 a being read-write Int-Location holds IC IExec(if=0(a,I,J),p,s) =  (card
I + card J + 3) & (s.a = 0 implies ((for d being Int-Location
 holds IExec(if=0(a,I,J),p,s).d = IExec(I,p,s).d) &
  for f being FinSeq-Location
 holds IExec(if=0(a,I,J),p,s).f = IExec(I,p,s).f)) & (s.a <> 0 implies
   ((for d being Int-Location holds
  IExec(if=0(a,I,J),p,s).d = IExec(J,p,s).d) &
  for f being FinSeq-Location holds
  IExec(if=0(a,I,J),p,s).f = IExec(J,p,s).f));

theorem :: SCM_HALT:39
  for s being State of SCM+FSA,
      I,J being really-closed MacroInstruction of SCM+FSA, a
  being read-write Int-Location st s.a > 0 &
:::I is_closed_onInit s,p &
I
  is_halting_onInit s,p holds
:::if>0(a,I,J) is_closed_onInit s,p &
if>0(a,I,J)
  is_halting_onInit s,p;

theorem :: SCM_HALT:40
  for s being State of SCM+FSA,
      I,J being really-closed MacroInstruction of SCM+FSA,
      a being read-write Int-Location st s.a > 0 &
:::I is_closed_onInit s,p &
  I
is_halting_onInit s,p holds IExec(if>0(a,I,J),p,s)
 = IExec(I,p,s) +* Start-At((card I + card J + 3),SCM+FSA);

theorem :: SCM_HALT:41
  for s being State of SCM+FSA,
      I,J being really-closed MacroInstruction of SCM+FSA,
      a being read-write Int-Location st s.a <= 0 &
:::J is_closed_onInit s,p &
J
  is_halting_onInit s,p holds
:::if>0(a,I,J) is_closed_onInit s,p &
if>0(a,I,J) is_halting_onInit s,p;

theorem :: SCM_HALT:42
  for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write
  Int-Location holds for s being State of SCM+FSA st s.a <= 0 &
:::Jis_closed_onInit s,p &
J is_halting_onInit s,p
 holds IExec(if>0(a,I,J),p,s)
  = IExec(J,p,s) +* Start-At((card I + card J + 3),SCM+FSA);

theorem :: SCM_HALT:43
  for s being State of SCM+FSA,
      I,J being InitHalting really-closed MacroInstruction of
SCM+FSA, a being read-write Int-Location holds if>0(a,I,J) is InitHalting & (s.
  a > 0 implies IExec(if>0(a,I,J),p,s) = IExec(I,p,s) +* Start-At((card I +
card J + 3),SCM+FSA)) &
 (s.a <= 0 implies IExec(if>0(a,I,J),p,s) = IExec(J,p,s) +* Start-At(
   (card I + card J + 3),SCM+FSA));

theorem :: SCM_HALT:44
  for s being State of SCM+FSA,
      I,J being InitHalting really-closed MacroInstruction of SCM+FSA
, a being read-write Int-Location holds IC IExec(if>0(a,I,J),p,s) =  (card
I + card J + 3) & (s.a > 0 implies ((for d being Int-Location
 holds IExec(if>0(a,I,J),p,s).d = IExec(I,p,s).d) &
  for f being FinSeq-Location
 holds IExec(if>0(a,I,J),p,s).f
  = IExec(I,p,s).f)) & (s.a <= 0 implies ((for d being Int-Location
   holds
  IExec(if>0(a,I,J),p,s).d = IExec(J,p,s).d) & for f being FinSeq-Location
   holds
  IExec(if>0(a,I,J),p,s).f = IExec(J,p,s).f));

::$CT 4

registration
  let I,J be InitHalting really-closed MacroInstruction of SCM+FSA;
  let a be read-write Int-Location;
  cluster if=0(a,I,J) -> InitHalting;
  cluster if>0(a,I,J) -> InitHalting;
::   cluster if<0(a,I,J) -> InitHalting;
::   correctness by Th46;
end;

theorem :: SCM_HALT:49
  for I being Program of SCM+FSA holds I is InitHalting iff for s
  being State of SCM+FSA,p holds I is_halting_on Initialized s,p;

::$CT

theorem :: SCM_HALT:51
  for s being State of SCM+FSA, I being InitHalting 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 :: SCM_HALT:52
  for s being State of SCM+FSA, I being InitHalting 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 :: SCM_HALT:53
  for s being State of SCM+FSA, I being InitHalting 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 :: SCM_HALT:54
  for s be State of SCM+FSA,
  I be keepInt0_1 InitHalting 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;

::$CT 7

theorem :: SCM_HALT:62
  for s being 0-started State of SCM+FSA,
      I being good InitHalting really-closed MacroInstruction of
SCM+FSA, a being read-write Int-Location
   st I does not destroy a & s.intloc 0 = 1
 holds Times(a,I) is_halting_on s,p;

registration
  let a be read-write Int-Location,I be good MacroInstruction of SCM+FSA;
  cluster Times(a,I) -> good;
end;

::$CT 2

theorem :: SCM_HALT:65
  for s being State of SCM+FSA,
      I being good InitHalting really-closed MacroInstruction
of SCM+FSA, a being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 holds
  DataPart IExec(Times(a,I),p,s) = DataPart s;

reserve P,P1,P2,Q for Instruction-Sequence of SCM+FSA;

theorem :: SCM_HALT:66
  for s being State of SCM+FSA,
      I being good InitHalting really-closed MacroInstruction
  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 &
 (s.a > 0 implies DataPart IExec(Times(a,I),p,s)
  = DataPart IExec(Times(a,I),p,IExec(I ";" SubFrom(a,intloc 0),p,s)));

theorem :: SCM_HALT:67
  for s be State of SCM+FSA,
      I be good InitHalting really-closed MacroInstruction of SCM+FSA,
      f be FinSeq-Location,a be read-write Int-Location st s.a <= 0
 holds IExec(Times(a,I),p,s).f=s.f;

theorem :: SCM_HALT:68
  for s be State of SCM+FSA,
      I be good InitHalting really-closed MacroInstruction of SCM+FSA,
      b be Int-Location,a be read-write Int-Location st s.a <= 0
 holds IExec(Times(a,I),p,s).b=(Initialized s).b;

theorem :: SCM_HALT:69
  for s be State of SCM+FSA,
      I be good InitHalting really-closed MacroInstruction of SCM+FSA,
      f be FinSeq-Location,a be read-write Int-Location
     st I does not destroy a & s.a > 0
 holds IExec(Times(a,I),p,s).f
   =IExec(Times(a,I),p,IExec(I ";" SubFrom(a,intloc 0),p,s)).f;

theorem :: SCM_HALT:70
  for s be State of SCM+FSA,
      I be good InitHalting really-closed MacroInstruction of SCM+FSA, b
be Int-Location,a be read-write Int-Location st I does not destroy a & s.a > 0
holds IExec(Times(a,I),p,s).b
 =IExec(Times(a,I),p,IExec(I ";" SubFrom(a,intloc 0),p,s)).b;

definition
  let i be Instruction of SCM+FSA;
  redefine attr i is good means
:: SCM_HALT:def 6
  i does not destroy intloc 0;
end;

theorem :: SCM_HALT:71
  for s be State of SCM+FSA,I be InitHalting really-closed Program of SCM+FSA
   st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2
 for k be Nat
  holds  Comput(P1, s,k) =  Comput(P2, s,k) &
   CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k));

theorem :: SCM_HALT:72
  for s be State of SCM+FSA,I be InitHalting really-closed Program of SCM+FSA
    st Initialize ((intloc 0) .--> 1) c= s &
    I c= P1 & I c= P2
  holds LifeSpan(P1,s) = LifeSpan(P2,s) &
    Result(P1,s) =  Result(P2,s);

theorem :: SCM_HALT:73
  for s being State of SCM+FSA,
      I being really-closed MacroInstruction of SCM+FSA,
      a being read-write Int-Location st s.a <= 0
 holds while>0(a,I) is_halting_onInit s,P;

theorem :: SCM_HALT:74
  for s being State of SCM+FSA,
      I be really-closed MacroInstruction of SCM+FSA,
      a be read-write Int-Location st
I is_halting_onInit s,P & s.a >
  0 holds IC Comput(P +* while>0(a,I), Initialized s,
     LifeSpan(P +* I,Initialized s) + 2) =  0 &
   DataPart Comput(P +* while>0(a,I), Initialized s,
    LifeSpan(P +* I,Initialized s) + 2)
     = DataPart Comput(P +* I, Initialized s,LifeSpan(P +* I,Initialized s));

theorem :: SCM_HALT:75
  for s be State of SCM+FSA,
     I be good InitHalting really-closed MacroInstruction of
SCM+FSA, a be read-write Int-Location st s.a > 0 & while>0(a,I) is InitHalting
holds DataPart IExec(while>0(a,I),P,s) =
 DataPart IExec(while>0(a,I),P,IExec(I,P,s));

theorem :: SCM_HALT:76
  for I be good InitHalting really-closed MacroInstruction of SCM+FSA,
      a be read-write
Int-Location st (for s be State of SCM+FSA,P holds (s.a > 0
 implies IExec(I,P,s).a < s.a )) holds while>0(a,I) is InitHalting;