The Mizar abstract of SCMFSA8C

Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users
The abstract of the Mizar article:: The \tt loop and \tt Times Macroinstruction for \SCMFSA
by
Noriko Asamoto
Received October 29, 1997
MML identifier: SCMFSA8C
[ Mizar article, MML identifier index ]
environ

 vocabulary AMI_1, SCMFSA_2, BOOLE, SCMFSA8A, SCMFSA6A, CAT_1, FUNCT_4, AMI_3,
      FUNCT_1, RELAT_1, CARD_1, AMI_5, UNIALG_2, SCMFSA7B, SCM_1, FUNCT_7,
      RELOC, ARYTM_1, SCMFSA6C, SCMFSA6B, SF_MASTR, SCMFSA_4, FUNCOP_1,
      SCMFSA8B, AMI_2, SCMFSA8C, CARD_3;
 notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, NAT_1, CQC_LANG,
      RELAT_1, FUNCT_1, FUNCT_4, FUNCT_7, CARD_1, STRUCT_0, AMI_1, AMI_3,
      AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCM_1, SF_MASTR, SCMFSA6A, SCMFSA6B,
      SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, BINARITH;
 constructors ENUMSET1, AMI_5, SCM_1, SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA6B,
      SCMFSA6C, SCMFSA8A, SCMFSA8B, BINARITH, MEMBERED;
 clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SCMFSA6A, SF_MASTR,
      SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, INT_1, CQC_LANG, NAT_1, FRAENKEL,
      XREAL_0, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve m for Nat;

definition
 cluster pseudo-paraclosed Macro-Instruction;
end;

canceled;

theorem :: SCMFSA8C:2  ::T4425 ** n.t
 for s being State of SCM+FSA,P being initial FinPartState of SCM+FSA
 st P is_pseudo-closed_on s
 for k being Nat st
 (for n being Nat st n <= k holds
     IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P)
 holds k < pseudo-LifeSpan(s,P);

canceled 3;

theorem :: SCMFSA8C:6  ::T210837
 for f be Function, x be set st x in dom f holds
     f +* (x .--> f.x) = f;

theorem :: SCMFSA8C:7  ::TMP12
 for l being Instruction-Location of SCM+FSA holds
     l + 0 = l;

theorem :: SCMFSA8C:8  ::TMP19
 for i being Instruction of SCM+FSA holds
     IncAddr(i,0) = i;

theorem :: SCMFSA8C:9  ::TMP13
 for P being programmed FinPartState of SCM+FSA holds
     ProgramPart Relocated(P,0) = P;

theorem :: SCMFSA8C:10  ::TMP15'
 for P,Q being FinPartState of SCM+FSA st P c= Q holds
     ProgramPart P c= ProgramPart Q;

theorem :: SCMFSA8C:11  ::TMP18
 for P,Q being programmed FinPartState of SCM+FSA, k being Nat st P c= Q holds
     Shift(P,k) c= Shift(Q,k);

theorem :: SCMFSA8C:12  ::TMP15
 for P,Q being FinPartState of SCM+FSA, k being Nat st P c= Q holds
     ProgramPart Relocated(P,k) c= ProgramPart Relocated(Q,k);

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

theorem :: SCMFSA8C:14  ::T22246 ---???
 for s being State of SCM+FSA st s.intloc 0 = 1 & IC s = insloc 0 holds
     Initialize s = s;

theorem :: SCMFSA8C:15  ::T200922
 for s being State of SCM+FSA holds
     Initialize Initialize s = Initialize s;

theorem :: SCMFSA8C:16  ::TMP6
 for s being State of SCM+FSA, I being Macro-Instruction holds
     s +* (Initialized I +* Start-At insloc 0) =
         Initialize s +* (I +* Start-At insloc 0);

theorem :: SCMFSA8C:17  ::T200938
 for s being State of SCM+FSA, I being Macro-Instruction holds
     IExec(I,s) = IExec(I,Initialize s);

theorem :: SCMFSA8C:18  ::T26401 --- ???
 for s being State of SCM+FSA, I being Macro-Instruction
 st s.intloc 0 = 1 holds
     s +* (I +* Start-At insloc 0) = s +* Initialized I;

theorem :: SCMFSA8C:19  ::T24634 --- ???
 for I being Macro-Instruction holds
     I +* Start-At insloc 0 c= Initialized I;

theorem :: SCMFSA8C:20  ::TMP10
 for l being Instruction-Location of SCM+FSA, I being Macro-Instruction holds
     l in dom I iff l in dom Initialized I;

theorem :: SCMFSA8C:21
   for s being State of SCM+FSA, I being Macro-Instruction holds
 Initialized I is_closed_on s iff I is_closed_on Initialize s;

theorem :: SCMFSA8C:22  ::TMP5
 for s being State of SCM+FSA, I being Macro-Instruction holds
 Initialized I is_halting_on s iff I is_halting_on Initialize s;

theorem :: SCMFSA8C:23
   for I being Macro-Instruction holds
 (for s being State of SCM+FSA holds I is_halting_on Initialize s) implies
     Initialized I is halting;

theorem :: SCMFSA8C:24  ::TMP3'
 for I being Macro-Instruction holds
 (for s being State of SCM+FSA holds Initialized I is_halting_on s) implies
     Initialized I is halting;

theorem :: SCMFSA8C:25  ::TMP9
 for I being Macro-Instruction holds
     ProgramPart Initialized I = I;

theorem :: SCMFSA8C:26  ::T18750
 for s being State of SCM+FSA, I being Macro-Instruction,
     l being Instruction-Location of SCM+FSA, x being set holds
 x in dom I implies I.x = (s +* (I +* Start-At l)).x;

theorem :: SCMFSA8C:27  ::T22246' ---???
 for s being State of SCM+FSA st s.intloc 0 = 1 holds
     (Initialize s) | (Int-Locations \/ FinSeq-Locations) =
         s | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:28  ::T210615
 for s being State of SCM+FSA, I being Macro-Instruction,
     a being Int-Location, l being Instruction-Location of SCM+FSA holds
 (s +* (I +* Start-At l)).a = s.a;

theorem :: SCMFSA8C:29
   for I being programmed FinPartState of SCM+FSA,
     l being Instruction-Location of SCM+FSA holds
 IC SCM+FSA in dom (I +* Start-At l);

theorem :: SCMFSA8C:30
   for I being programmed FinPartState of SCM+FSA,
     l being Instruction-Location of SCM+FSA holds
 (I +* Start-At l).IC SCM+FSA = l;

theorem :: SCMFSA8C:31  ::T4633 -- ??
 for s being State of SCM+FSA, P being FinPartState of SCM+FSA,
     l being Instruction-Location of SCM+FSA holds
 IC (s +* (P +* Start-At l)) = l;

theorem :: SCMFSA8C:32  ::T30408
 for s being State of SCM+FSA, i being Instruction of SCM+FSA st
     InsCode i in {0,6,7,8} holds
 Exec(i,s) | (Int-Locations \/ FinSeq-Locations) =
     s | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:33  ::T271245 --- ???
 for s1,s2 being State of SCM+FSA st
     s1.intloc 0 = s2.intloc 0 &
     ((for a being read-write Int-Location holds s1.a = s2.a) &
     for f being FinSeq-Location holds s1.f = s2.f) holds
 s1 | (Int-Locations \/ FinSeq-Locations) =
     s2 | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:34
   for s being State of SCM+FSA,P being programmed FinPartState of SCM+FSA
holds
     (s +* P) | (Int-Locations \/ FinSeq-Locations) =
         s | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:35  ::T1643 --- ??
 for s,ss being State of SCM+FSA holds
     (s +* ss | the Instruction-Locations of SCM+FSA) |
         (Int-Locations \/ FinSeq-Locations) =
     s | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:36  ::T27643 --- ???
 for s being State of SCM+FSA holds
 (Initialize s) | the Instruction-Locations of SCM+FSA =
     s | the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA8C:37  ::T26530 --- ???
 for s,ss being State of SCM+FSA, I being Macro-Instruction holds
     (ss +* (s | (the Instruction-Locations of SCM+FSA))) |
         (Int-Locations \/ FinSeq-Locations) =
             ss | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:38  ::T27500 ue
 for s being State of SCM+FSA holds
     IExec(SCM+FSA-Stop,s) = Initialize s +* Start-At insloc 0;

theorem :: SCMFSA8C:39  ::T9x
 for s being State of SCM+FSA,I being Macro-Instruction
 st I is_closed_on s holds insloc 0 in dom I;

theorem :: SCMFSA8C:40
   for s being State of SCM+FSA,I being paraclosed Macro-Instruction holds
     insloc 0 in dom I;

theorem :: SCMFSA8C:41  ::Tm1(@BBB8)
 for i being Instruction of SCM+FSA holds
     rng Macro i = {i,halt SCM+FSA};

theorem :: SCMFSA8C:42  ::T0x
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
     I is_closed_on s1 & I +* Start-At insloc 0 c= s1
 for n being Nat st ProgramPart Relocated(I,n) c= s2 &
     IC s2 = insloc n &
     s1 | (Int-Locations \/ FinSeq-Locations) =
         s2 | (Int-Locations \/ FinSeq-Locations)
 for i being Nat holds
     IC (Computation s1).i + n = IC (Computation s2).i &
     IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) &
     (Computation s1).i | (Int-Locations \/ FinSeq-Locations)
         = (Computation s2).i | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:43  ::T24441
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
     I is_closed_on s1 &
     I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
     s1 | (Int-Locations \/ FinSeq-Locations) =
         s2 | (Int-Locations \/ FinSeq-Locations)
 for i being Nat holds
     IC (Computation s1).i = IC (Computation s2).i &
     CurInstr (Computation s1).i = CurInstr (Computation s2).i &
     (Computation s1).i | (Int-Locations \/ FinSeq-Locations) =
         (Computation s2).i | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:44  ::T24441'
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
     I is_closed_on s1 & I is_halting_on s1 &
     I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
     s1 | (Int-Locations \/ FinSeq-Locations) =
         s2 | (Int-Locations \/ FinSeq-Locations) holds
 LifeSpan s1 = LifeSpan s2;

theorem :: SCMFSA8C:45  ::T27835
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
     s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 &
     ((for a being read-write Int-Location holds s1.a = s2.a) &
     for f being FinSeq-Location holds s1.f = s2.f) holds
 IExec(I,s1) | (Int-Locations \/ FinSeq-Locations) =
     IExec(I,s2) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:46  ::T27835'
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
     s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 &
     s1 | (Int-Locations \/ FinSeq-Locations) =
         s2 | (Int-Locations \/ FinSeq-Locations) holds
 IExec(I,s1) | (Int-Locations \/ FinSeq-Locations) =
     IExec(I,s2) | (Int-Locations \/ FinSeq-Locations);

definition
 let I be Macro-Instruction;
 cluster Initialized I -> initial;
end;

theorem :: SCMFSA8C:47  ::TMP8
  for s being State of SCM+FSA, I being Macro-Instruction holds
 Initialized I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s;

theorem :: SCMFSA8C:48
   for s being State of SCM+FSA, I being Macro-Instruction
 st I is_pseudo-closed_on Initialize s holds
      pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I);

theorem :: SCMFSA8C:49
   for s being State of SCM+FSA, I being Macro-Instruction
 st Initialized I is_pseudo-closed_on s holds
      pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I);

theorem :: SCMFSA8C:50  ::TMP14
 for s being State of SCM+FSA, I being initial FinPartState of SCM+FSA
 st I is_pseudo-closed_on s holds
      I is_pseudo-closed_on s +* (I +* Start-At insloc 0) &
      pseudo-LifeSpan(s,I) = pseudo-LifeSpan(s +* (I +* Start-At insloc 0),I);

theorem :: SCMFSA8C:51  ::P'115'
 for s1,s2 being State of SCM+FSA, I being Macro-Instruction
 st I +* Start-At insloc 0 c= s1 & I is_pseudo-closed_on s1
 for n being Nat st ProgramPart Relocated(I,n) c= s2 &
     IC s2 = insloc n &
     s1 | (Int-Locations \/ FinSeq-Locations)
     = s2 | (Int-Locations \/ FinSeq-Locations) holds
 ((for i being Nat st i < pseudo-LifeSpan(s1,I) holds
     IncAddr(CurInstr (Computation s1).i,n) = CurInstr (Computation s2).i) &
 for i being Nat st i <= pseudo-LifeSpan(s1,I) holds
     IC (Computation s1).i + n = IC (Computation s2).i &
     (Computation s1).i | (Int-Locations \/ FinSeq-Locations)
         = (Computation s2).i | (Int-Locations \/ FinSeq-Locations));

theorem :: SCMFSA8C:52  ::TMP11
 for s1,s2 being State of SCM+FSA, I being Macro-Instruction st
     s1 | (Int-Locations \/ FinSeq-Locations) =
         s2 | (Int-Locations \/ FinSeq-Locations) holds
     I is_pseudo-closed_on s1 implies I is_pseudo-closed_on s2;

theorem :: SCMFSA8C:53  ::T1702
 for s being State of SCM+FSA, I being Macro-Instruction
     st s.intloc 0 = 1 holds
 I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s;

theorem :: SCMFSA8C:54  ::TD2' ** n.t
 for a being Int-Location, I,J being Macro-Instruction holds
     insloc 0 in dom if=0(a,I,J) &
     insloc 1 in dom if=0(a,I,J) &
     insloc 0 in dom if>0(a,I,J) &
     insloc 1 in dom if>0(a,I,J);

theorem :: SCMFSA8C:55  ::TD2 ** n.t
 for a being Int-Location, I,J being Macro-Instruction holds
     if=0(a,I,J).insloc 0 = a =0_goto insloc (card J + 3) &
     if=0(a,I,J).insloc 1 = goto insloc 2 &
     if>0(a,I,J).insloc 0 = a >0_goto insloc (card J + 3) &
     if>0(a,I,J).insloc 1 = goto insloc 2;

theorem :: SCMFSA8C:56  ::T6327 ** n.t
 for a being Int-Location, I,J being Macro-Instruction, n being Nat st
 n < card I + card J + 3 holds insloc n in dom if=0(a,I,J) &
 if=0(a,I,J).insloc n <> halt SCM+FSA;

theorem :: SCMFSA8C:57  ::T6327' ** n.t
 for a being Int-Location, I,J being Macro-Instruction, n being Nat st
 n < card I + card J + 3 holds insloc n in dom if>0(a,I,J) &
 if>0(a,I,J).insloc n <> halt SCM+FSA;

theorem :: SCMFSA8C:58  ::T29502
 for s being State of SCM+FSA, I being Macro-Instruction st
     Directed I is_pseudo-closed_on s holds
 I ';' SCM+FSA-Stop is_closed_on s &
 I ';' SCM+FSA-Stop is_halting_on s &
 LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) =
     pseudo-LifeSpan(s,Directed I) &
 (for n being Nat st n < pseudo-LifeSpan(s,Directed I) holds
     IC (Computation (s +* (I +* Start-At insloc 0))).n =
         IC (Computation (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))).n) &
 for n being Nat st n <= pseudo-LifeSpan(s,Directed I) holds
     (Computation (s +* (I +* Start-At insloc 0))).n | D =
         (Computation (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))).n | D;

theorem :: SCMFSA8C:59  ::T29502'
 for s being State of SCM+FSA, I being Macro-Instruction st
     Directed I is_pseudo-closed_on s holds
 (Result (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))) | D =
     (Computation (s +* (I +* Start-At insloc 0))).
         pseudo-LifeSpan(s,Directed I) | D;

theorem :: SCMFSA8C:60
   for s being State of SCM+FSA, I being Macro-Instruction st
     s.intloc 0 = 1 & Directed I is_pseudo-closed_on s holds
 IExec(I ';' SCM+FSA-Stop,s) | D =
     (Computation (s +* (I +* Start-At insloc 0))).
         pseudo-LifeSpan(s,Directed I) | D;

theorem :: SCMFSA8C:61  ::TMP20 ** n.t
 for I,J being Macro-Instruction,a being Int-Location holds
     if=0(a,I,J).insloc (card I + card J + 3) = halt SCM+FSA;

theorem :: SCMFSA8C:62  ::TMP20' ** n.t
 for I,J being Macro-Instruction,a being Int-Location holds
     if>0(a,I,J).insloc (card I + card J + 3) = halt SCM+FSA;

theorem :: SCMFSA8C:63  ::TMP21 ** n.t
 for I,J being Macro-Instruction,a being Int-Location holds
     if=0(a,I,J).insloc (card J + 2) = goto insloc (card I + card J + 3);

theorem :: SCMFSA8C:64  ::TMP21' ** n.t
 for I,J being Macro-Instruction,a being Int-Location holds
     if>0(a,I,J).insloc (card J + 2) = goto insloc (card I + card J + 3);

theorem :: SCMFSA8C:65  ::T31139 ** n.t
 for J being Macro-Instruction,a being Int-Location holds
     if=0(a,Goto insloc 2,J).insloc (card J + 3) = goto insloc (card J + 5);

theorem :: SCMFSA8C:66  ::TMP71
 for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.a = 0 & Directed I is_pseudo-closed_on s holds
     if=0(a,I,J) is_halting_on s & if=0(a,I,J) is_closed_on s &
     LifeSpan (s +* (if=0(a,I,J) +* Start-At insloc 0)) =
         LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) + 1;

theorem :: SCMFSA8C:67
   for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.intloc 0 = 1 & s.a = 0 & Directed I is_pseudo-closed_on s holds
     IExec(if=0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) =
         IExec(I ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:68  ::TMP71'
 for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.a > 0 & Directed I is_pseudo-closed_on s holds
     if>0(a,I,J) is_halting_on s & if>0(a,I,J) is_closed_on s &
     LifeSpan (s +* (if>0(a,I,J) +* Start-At insloc 0)) =
         LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) + 1;

theorem :: SCMFSA8C:69  ::TMP7'
 for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.intloc 0 = 1 & s.a > 0 & Directed I is_pseudo-closed_on s holds
     IExec(if>0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) =
         IExec(I ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:70  ::TMP171
 for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.a <> 0 & Directed J is_pseudo-closed_on s holds
     if=0(a,I,J) is_halting_on s & if=0(a,I,J) is_closed_on s &
     LifeSpan (s +* (if=0(a,I,J) +* Start-At insloc 0)) =
         LifeSpan (s +* (J ';' SCM+FSA-Stop +* Start-At insloc 0)) + 3;

theorem :: SCMFSA8C:71
   for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.intloc 0 = 1 & s.a <> 0 & Directed J is_pseudo-closed_on s holds
     IExec(if=0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) =
         IExec(J ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:72  ::TMP171'
 for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.a <= 0 & Directed J is_pseudo-closed_on s holds
     if>0(a,I,J) is_halting_on s & if>0(a,I,J) is_closed_on s &
     LifeSpan (s +* (if>0(a,I,J) +* Start-At insloc 0)) =
         LifeSpan (s +* (J ';' SCM+FSA-Stop +* Start-At insloc 0)) + 3;

theorem :: SCMFSA8C:73  ::TMP17'
 for s being State of SCM+FSA, I,J being Macro-Instruction,
     a being read-write Int-Location
 st s.intloc 0 = 1 & s.a <= 0 & Directed J is_pseudo-closed_on s holds
     IExec(if>0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) =
         IExec(J ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations);

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

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

theorem :: SCMFSA8C:76  ::TG8'
 for I being Macro-Instruction, a being Int-Location holds
     I does_not_destroy a implies Directed I does_not_destroy a;

theorem :: SCMFSA8C:77  ::Td1(@BBB8)
 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:78  ::R0'
 for a being Int-Location holds
     halt SCM+FSA does_not_refer a;

theorem :: SCMFSA8C:79
   for a,b,c being Int-Location holds
     a <> b implies AddTo(c,b) does_not_refer a;

theorem :: SCMFSA8C:80
   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:81  ::TG9'
 for I,J being Macro-Instruction, a being Int-Location holds
     I does_not_destroy a & J does_not_destroy a implies
         I ';' J does_not_destroy a;

theorem :: SCMFSA8C:82  ::T281220
 for J being Macro-Instruction, 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:83
   for I being Macro-Instruction, 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:84
   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:85  ::TQ7'
 for a being Int-Location holds
     SCM+FSA-Stop does_not_destroy a;

theorem :: SCMFSA8C:86  ::T27749
 for a being Int-Location, l being Instruction-Location of SCM+FSA holds
     Goto l does_not_destroy a;

theorem :: SCMFSA8C:87  ::T200724'
 for s being State of SCM+FSA, I being Macro-Instruction
     st I is_halting_on Initialize s holds
 (for a being read-write Int-Location holds
     IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).
         (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).a) &
 for f being FinSeq-Location holds
     IExec(I,s).f = (Computation (Initialize s +* (I +* Start-At insloc 0))).
         (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).f;

theorem :: SCMFSA8C:88  ::T200724
 for s being State of SCM+FSA, I being parahalting Macro-Instruction,
     a being read-write Int-Location holds
 IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).
     (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).a;

theorem :: SCMFSA8C:89  ::TMP29'
 for s being State of SCM+FSA, I being Macro-Instruction,
     a being Int-Location,k being Nat st
     I is_closed_on Initialize s & I is_halting_on Initialize s &
     I does_not_destroy a holds
 IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).k.a;

theorem :: SCMFSA8C:90  ::TMP29
 for s being State of SCM+FSA, I being parahalting Macro-Instruction,
     a being Int-Location,k being Nat st I does_not_destroy a holds
 IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).k.a;

theorem :: SCMFSA8C:91  ::TMP29''
 for s being State of SCM+FSA, I being parahalting Macro-Instruction,
     a being Int-Location st I does_not_destroy a holds
 IExec(I,s).a = (Initialize s).a;

theorem :: SCMFSA8C:92  ::T200724''
 for s being State of SCM+FSA, I being keeping_0 Macro-Instruction st
     I is_halting_on Initialize s holds
 IExec(I,s).intloc 0 = 1 &
 for k being Nat holds
     (Computation (Initialize s +* (I +* Start-At insloc 0))).k.intloc 0 = 1;

theorem :: SCMFSA8C:93  ::TQ9
 for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location
     st I does_not_destroy a holds
 for k being Nat st IC (Computation (s +* (I +* Start-At insloc 0))).k in dom I
     holds (Computation (s +* (I +* Start-At insloc 0))).(k + 1).a =
         (Computation (s +* (I +* Start-At insloc 0))).k.a;

theorem :: SCMFSA8C:94  ::TQ9'
 for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location
     st I does_not_destroy a holds
 for m being Nat st (for n being Nat st n < m holds
     IC (Computation (s +* (I +* Start-At insloc 0))).n in dom I) holds
 for n being Nat st n <= m holds
     (Computation (s +* (I +* Start-At insloc 0))).n.a = s.a;

theorem :: SCMFSA8C:95  ::T210921
 for s being State of SCM+FSA, I being good Macro-Instruction
 for m being Nat st (for n being Nat st n < m holds
     IC (Computation (s +* (I +* Start-At insloc 0))).n in dom I) holds
 for n being Nat st n <= m holds
     (Computation (s +* (I +* Start-At insloc 0))).n.intloc 0 = s.intloc 0;

theorem :: SCMFSA8C:96  ::T22842
 for s being State of SCM+FSA, I being good Macro-Instruction st
     I is_halting_on Initialize s & I is_closed_on Initialize s holds
 IExec(I,s).intloc 0 = 1 &
 for k being Nat holds
     (Computation (Initialize s +* (I +* Start-At insloc 0))).k.intloc 0 = 1;

theorem :: SCMFSA8C:97
   for s being State of SCM+FSA, I being good Macro-Instruction
 st I is_closed_on s holds
     for k being Nat holds
         (Computation (s +* (I +* Start-At insloc 0))).k.intloc 0 = s.intloc 0;

theorem :: SCMFSA8C:98  ::TMP27
 for s being State of SCM+FSA, I being keeping_0 parahalting Macro-Instruction,
     a being read-write Int-Location st I does_not_destroy a holds
 (Computation (Initialize s +* (I ';' SubFrom(a,intloc 0) +*
     Start-At insloc 0))).(LifeSpan (Initialize s +*
     (I ';' SubFrom(a,intloc 0) +* Start-At insloc 0))).a = s.a - 1;

theorem :: SCMFSA8C:99  ::T211205
 for i being Instruction of SCM+FSA st i does_not_destroy intloc 0 holds
     Macro i is good;

theorem :: SCMFSA8C:100  ::T13'   6B
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction
     st I is_closed_on s1 & I is_halting_on s1 & s1 | D = s2 | D holds
 for k being Nat holds
     (Computation (s1 +* (I +* Start-At insloc 0))).k,
         (Computation (s2 +* (I +* Start-At insloc 0))).k
         equal_outside the Instruction-Locations of SCM+FSA &
     CurInstr (Computation (s1 +* (I +* Start-At insloc 0))).k =
         CurInstr (Computation (s2 +* (I +* Start-At insloc 0))).k;

theorem :: SCMFSA8C:101  ::T14'   6B
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction
     st I is_closed_on s1 & I is_halting_on s1 & s1 | D = s2 | D holds
 LifeSpan (s1 +* (I +* Start-At insloc 0)) =
     LifeSpan (s2 +* (I +* Start-At insloc 0)) &
 Result (s1 +* (I +* Start-At insloc 0)),
     Result (s2 +* (I +* Start-At insloc 0)) equal_outside
         the Instruction-Locations of SCM+FSA;

canceled;

theorem :: SCMFSA8C:103  ::T3829
 for s1,s2 being State of SCM+FSA,I being Macro-Instruction
     st I is_closed_on s1 & I is_halting_on s1 &
     I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
 ex k being Nat st (Computation s1).k,s2
     equal_outside the Instruction-Locations of SCM+FSA holds
 Result s1,Result s2 equal_outside the Instruction-Locations of SCM+FSA;

begin :: loop

definition
 let I be Macro-Instruction, k be Nat;
 cluster IncAddr(I,k) -> initial programmed;
end;

definition
 let I be Macro-Instruction;
 canceled 3;

 func loop I -> halt-free Macro-Instruction equals
:: SCMFSA8C:def 4
 ::D17
 ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc 0)) * I;
end;

theorem :: SCMFSA8C:104  ::T1
 for I being Macro-Instruction holds
     loop I = Directed(I,insloc 0);

theorem :: SCMFSA8C:105
   for I being Macro-Instruction, a being Int-Location holds
     I does_not_destroy a implies loop I does_not_destroy a;

definition
 let I be good Macro-Instruction;
 cluster loop I -> good;
end;

theorem :: SCMFSA8C:106  ::SCMFSA6A'14
 for I being Macro-Instruction holds
     dom loop I = dom I;

theorem :: SCMFSA8C:107  ::SCMFSA6A'18
 for I being Macro-Instruction holds
     not halt SCM+FSA in rng loop I;

theorem :: SCMFSA8C:108  ::SCMFSA6A'54
 for I being Macro-Instruction, x being set holds
     I.x <> halt SCM+FSA implies (loop I).x = I.x;

theorem :: SCMFSA8C:109  ::TMP24
 for s being State of SCM+FSA, I being Macro-Instruction
     st I is_closed_on s & I is_halting_on s
 for m being Nat st m <= LifeSpan (s +* (I +* Start-At insloc 0))
     holds (Computation (s +* (I +* Start-At insloc 0))).m,
         (Computation(s +* (loop I +* Start-At insloc 0))).m
         equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA8C:110  ::TMP25
 for s being State of SCM+FSA, I being Macro-Instruction
     st I is_closed_on s & I is_halting_on s
 for m being Nat st m < LifeSpan (s +* (I +* Start-At insloc 0)) holds
     CurInstr (Computation (s +* (I +* Start-At insloc 0))).m =
         CurInstr (Computation(s +* (loop I +* Start-At insloc 0))).m;

theorem :: SCMFSA8C:111
   for s being State of SCM+FSA, I being Macro-Instruction
     st I is_closed_on s & I is_halting_on s
 for m being Nat st m <= LifeSpan (s +* (I +* Start-At insloc 0)) holds
  CurInstr (Computation (s +* (loop I +* Start-At insloc 0))).m <> halt SCM+FSA
;

theorem :: SCMFSA8C:112  ::TMP26
  for s being State of SCM+FSA, I being Macro-Instruction
     st I is_closed_on s & I is_halting_on s holds
 CurInstr (Computation (s +* (loop I +* Start-At insloc 0))).
      LifeSpan (s +* (I +* Start-At insloc 0)) = goto insloc 0;

theorem :: SCMFSA8C:113  ::MAI1
 for s being State of SCM+FSA, I being paraclosed Macro-Instruction
     st I +* Start-At insloc 0 c= s & s is halting
 for m being Nat st m <= LifeSpan s
     holds (Computation s).m,(Computation (s +* loop I)).m
         equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA8C:114
   for s being State of SCM+FSA, I being parahalting Macro-Instruction
 st Initialized I c= s holds
     for k being Nat st k <= LifeSpan s holds
         CurInstr (Computation (s +* loop I)).k <> halt SCM+FSA;

begin :: Times

definition
 let a be Int-Location;
 let I be Macro-Instruction;
 func Times(a,I) -> Macro-Instruction equals
:: SCMFSA8C:def 5
 ::D13
  if>0(a,loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)),
     SCM+FSA-Stop);
end;

theorem :: SCMFSA8C:115  ::T211147 *** n.t
 for I being good Macro-Instruction, a being read-write Int-Location holds
     if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)) is good;

theorem :: SCMFSA8C:116  ::T21921 ** n.t
 for I,J being Macro-Instruction,a being Int-Location holds
     if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)).
         insloc (card (I ';' SubFrom(a,intloc 0)) + 3) =
         goto insloc (card (I ';' SubFrom(a,intloc 0)) + 5);

theorem :: SCMFSA8C:117  ::TMP22
 for s being State of SCM+FSA, I being good parahalting Macro-Instruction,
     a being read-write Int-Location st
     I does_not_destroy a & s.intloc 0 = 1 & s.a > 0 holds
 loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)) is_pseudo-closed_on s;

theorem :: SCMFSA8C:118
   for s being State of SCM+FSA, I being good parahalting Macro-Instruction,
     a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds
 Initialized loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0))
     is_pseudo-closed_on s;

theorem :: SCMFSA8C:119
   for s being State of SCM+FSA, I being good parahalting Macro-Instruction,
     a being read-write Int-Location
     st I does_not_destroy a & s.intloc 0 = 1 holds
 Times(a,I) is_closed_on s & Times(a,I) is_halting_on s;

theorem :: SCMFSA8C:120
   for I being good parahalting Macro-Instruction,
     a being read-write Int-Location st I does_not_destroy a holds
     Initialized Times(a,I) is halting;

theorem :: SCMFSA8C:121
   for I,J being Macro-Instruction, 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;

theorem :: SCMFSA8C:122  ::TMP22'
 for s being State of SCM+FSA, I being good parahalting Macro-Instruction,
     a being read-write Int-Location st I does_not_destroy a &
     s.intloc 0 = 1 & s.a > 0 holds
 ex s2 being State of SCM+FSA, k being Nat st
     s2 = s +* (loop if=0(a,Goto insloc 2,
     I ';' SubFrom(a,intloc 0)) +* Start-At insloc 0) &
     k = LifeSpan (s +* (if=0(a,Goto insloc 2,
         I ';' SubFrom(a,intloc 0)) +* Start-At insloc 0)) + 1 &
     (Computation s2).k.a = s.a - 1 &
     (Computation s2).k.intloc 0 = 1 &
   (for b being read-write Int-Location st b <> a holds
      (Computation s2).k.b = IExec(I,s).b) &
   (for f being FinSeq-Location holds (Computation s2).k.f = IExec(I,s).f) &
   IC (Computation s2).k = insloc 0 &
   for n being Nat st n <= k holds
       IC (Computation s2).n in
           dom loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0));

theorem :: SCMFSA8C:123  ::T1
 for s being State of SCM+FSA, I being good parahalting Macro-Instruction,
     a being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 holds
 IExec(Times(a,I),s) | (Int-Locations \/ FinSeq-Locations) =
     s | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8C:124  ::T2
 for s being State of SCM+FSA, I being good parahalting Macro-Instruction,
     a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds
 IExec(I ';' SubFrom(a,intloc 0),s).a = s.a - 1 &
 IExec(Times(a,I),s) | (Int-Locations \/ FinSeq-Locations) =
     IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)) |
         (Int-Locations \/ FinSeq-Locations);

begin ::example

theorem :: SCMFSA8C:125
   for s being State of SCM+FSA, a,b,c being read-write Int-Location
 st a <> b & a <> c & b <> c & s.a >= 0 holds
     IExec(Times(a,Macro AddTo(b,c)),s).b = s.b + s.c * s.a;
The abstract of the Mizar article:

The \tt loop and \tt Times Macroinstruction for \SCMFSA
