:: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA}
:: by Noriko Asamoto
::
:: Received October 29, 1997
:: Copyright (c) 1997-2019 Association of Mizar Users

set SA0 = Start-At (0,SCM+FSA);

set Q = () .--> 1;

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

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

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

theorem :: SCMFSA8C:4
canceled;

::$CT theorem Th4: :: SCMFSA8C:5 for I being Program of SCM+FSA st ( for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds Initialize (() .--> 1) is I -halted proof end; theorem :: SCMFSA8C:6 for I being Program of SCM+FSA st ( for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds Initialize (() .--> 1) is I -halted by Th4; theorem :: SCMFSA8C:7 canceled; theorem :: SCMFSA8C:8 canceled; theorem :: SCMFSA8C:9 canceled; theorem :: SCMFSA8C:10 canceled; theorem :: SCMFSA8C:11 canceled; ::$CT 5
theorem Th6: :: SCMFSA8C:12
for s being State of SCM+FSA
for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds
DataPart (Exec (i,s)) = DataPart s
proof end;

theorem :: SCMFSA8C:13
canceled;

::$CT theorem :: SCMFSA8C:14 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA holds IExec ((),P,s) = Initialized s proof end; theorem :: SCMFSA8C:15 canceled; ::$CT
theorem Th8: :: SCMFSA8C:16
for P1, P2 being Instruction-Sequence of SCM+FSA
for s1 being 0 -started State of SCM+FSA
for s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st I c= P1 holds
for n being Nat st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
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)) )
proof end;

theorem Th9: :: SCMFSA8C:17
for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being 0 -started State of SCM+FSA
for I being really-closed Program of SCM+FSA st I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
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)) )
proof end;

theorem Th10: :: SCMFSA8C:18
for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being 0 -started State of SCM+FSA
for 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)
proof end;

theorem :: SCMFSA8C:19
for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st s1 . () = 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))
proof end;

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

theorem Th13: :: SCMFSA8C:21
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for 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 ((),(P +* I),I) )
proof end;

theorem Th14: :: SCMFSA8C:22
for P1, P2 being Instruction-Sequence of SCM+FSA
for s1 being 0 -started State of SCM+FSA
for s2 being State of SCM+FSA
for I being Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds
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)) ) ) )
proof end;

theorem Th15: :: SCMFSA8C:23
for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2
proof end;

theorem Th16: :: SCMFSA8C:24
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . () = 1 holds
( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )
proof end;

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

theorem Th18: :: SCMFSA8C:26
for a being Int-Location
for 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 )
proof end;

theorem Th19: :: SCMFSA8C:27
for a being Int-Location
for I, J being MacroInstruction of SCM+FSA
for 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 )
proof end;

theorem Th20: :: SCMFSA8C:28
for a being Int-Location
for I, J being MacroInstruction of SCM+FSA
for 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 )
proof end;

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

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

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

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

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

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

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

theorem :: SCMFSA8C:36
canceled;

::$CT theorem Th28: :: SCMFSA8C:37 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for 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))),()) = (LifeSpan ((P +* (I ";" ())),())) + 1 ) proof end; theorem :: SCMFSA8C:38 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for a being read-write Int-Location st s . () = 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 ";" ()),P,s)) proof end; theorem Th30: :: SCMFSA8C:39 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for 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))),()) = (LifeSpan ((P +* (I ";" ())),())) + 1 ) proof end; theorem :: SCMFSA8C:40 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for a being read-write Int-Location st s . () = 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 ";" ()),P,s)) proof end; theorem Th32: :: SCMFSA8C:41 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for 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))),()) = (LifeSpan ((P +* (J ";" ())),())) + 3 ) proof end; theorem :: SCMFSA8C:42 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for a being read-write Int-Location st s . () = 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 ";" ()),P,s)) proof end; theorem Th34: :: SCMFSA8C:43 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for 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 +* ())) = (LifeSpan ((P +* (J ";" ())),())) + 3 ) proof end; theorem :: SCMFSA8C:44 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for a being read-write Int-Location st s . () = 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 ";" ()),P,s)) proof end; theorem :: SCMFSA8C:45 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for 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 proof end; theorem :: SCMFSA8C:46 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I, J being MacroInstruction of SCM+FSA for 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 proof end; theorem :: SCMFSA8C:47 for I being Program of SCM+FSA for a being Int-Location st not I destroys a holds not Directed I destroys a by SCMFSA8A:13; theorem Th39: :: SCMFSA8C:48 for i being Instruction of SCM+FSA for a being Int-Location st not i destroys a holds not Macro i destroys a proof end; theorem :: SCMFSA8C:49 for a being Int-Location holds not halt SCM+FSA refers a ; theorem :: SCMFSA8C:50 for a, b, c being Int-Location st a <> b holds not AddTo (c,b) refers a proof end; theorem :: SCMFSA8C:51 for i being Instruction of SCM+FSA for a being Int-Location st not i refers a holds not Macro i refers a proof end; theorem Th43: :: SCMFSA8C:52 for I, J being Program of SCM+FSA for a being Int-Location st not I destroys a & not J destroys a holds not I ";" J destroys a proof end; theorem Th44: :: SCMFSA8C:53 for J being Program of SCM+FSA for i being Instruction of SCM+FSA for a being Int-Location st not i destroys a & not J destroys a holds not i ";" J destroys a proof end; theorem Th45: :: SCMFSA8C:54 for I being Program of SCM+FSA for j being Instruction of SCM+FSA for a being Int-Location st not I destroys a & not j destroys a holds not I ";" j destroys a proof end; theorem :: SCMFSA8C:55 for i, j being Instruction of SCM+FSA for a being Int-Location st not i destroys a & not j destroys a holds not i ";" j destroys a proof end; theorem Th47: :: SCMFSA8C:56 for a being Int-Location holds not Stop SCM+FSA destroys a proof end; theorem Th48: :: SCMFSA8C:57 for a being Int-Location for l being Nat holds not Goto l destroys a proof end; theorem Th49: :: SCMFSA8C:58 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for 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),(),(LifeSpan ((P +* I),())))) . a ) & ( for f being FinSeq-Location holds (IExec (I,P,s)) . f = (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) . f ) ) proof end; theorem Th50: :: SCMFSA8C:59 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being parahalting Program of SCM+FSA for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) . a proof end; theorem Th51: :: SCMFSA8C:60 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being really-closed Program of SCM+FSA for a being Int-Location for k being Element of NAT st I is_halting_on Initialized s,P & not I destroys a holds (IExec (I,P,s)) . a = (Comput ((P +* I),(),k)) . a proof end; theorem Th52: :: SCMFSA8C:61 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being really-closed parahalting Program of SCM+FSA for a being Int-Location for k being Element of NAT st not I destroys a holds (IExec (I,P,s)) . a = (Comput ((P +* I),(),k)) . a proof end; theorem Th53: :: SCMFSA8C:62 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being really-closed parahalting Program of SCM+FSA for a being Int-Location st not I destroys a holds (IExec (I,P,s)) . a = () . a proof end; theorem Th54: :: SCMFSA8C:63 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds ( (IExec (I,P,s)) . () = 1 & ( for k being Nat holds (Comput ((P +* I),(),k)) . () = 1 ) ) proof end; theorem Th55: :: SCMFSA8C:64 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA for a being Int-Location st not I destroys a holds for k being Element of NAT st IC (Comput ((P +* I),(),k)) in dom I holds (Comput ((P +* I),(),(k + 1))) . a = (Comput ((P +* I),(),k)) . a proof end; theorem Th56: :: SCMFSA8C:65 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA for a being Int-Location st not I destroys a holds for m being Nat st ( for n being Nat st n < m holds IC (Comput ((P +* I),(),n)) in dom I ) holds for n being Nat st n <= m holds (Comput ((P +* I),(),n)) . a = s . a proof end; theorem Th57: :: SCMFSA8C:66 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good Program of SCM+FSA for m being Nat st ( for n being Nat st n < m holds IC (Comput ((P +* I),(),n)) in dom I ) holds for n being Nat st n <= m holds (Comput ((P +* I),(),n)) . () = s . () by ; registration existence ex b1 being MacroInstruction of SCM+FSA st ( b1 is good & b1 is keeping_0 & b1 is really-closed & b1 is parahalting ) proof end; end; theorem :: SCMFSA8C:67 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds ( (IExec (I,P,s)) . () = 1 & ( for k being Nat holds (Comput ((P +* I),(),k)) . () = 1 ) ) proof end; theorem :: SCMFSA8C:68 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being good really-closed Program of SCM+FSA for k being Nat holds (Comput ((P +* I),(),k)) . () = s . () by ; theorem :: SCMFSA8C:69 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being keeping_0 really-closed parahalting Program of SCM+FSA for a being read-write Int-Location st not I destroys a holds (Comput ((P +* (I ";" (SubFrom (a,())))),(),(LifeSpan ((P +* (I ";" (SubFrom (a,())))),())))) . a = (s . a) - 1 proof end; theorem :: SCMFSA8C:70 for i being Instruction of SCM+FSA st not i destroys intloc 0 holds Macro i is good by Th39; theorem Th62: :: SCMFSA8C:71 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds for k being Nat holds ( Comput ((P1 +* I),(),k) = Comput ((P2 +* I),(),k) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(),k))) ) proof end; theorem Th63: :: SCMFSA8C:72 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being State of SCM+FSA for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds ( LifeSpan ((P1 +* I),()) = LifeSpan ((P2 +* I),()) & Result ((P1 +* I),()) = Result ((P2 +* I),()) ) proof end; theorem :: SCMFSA8C:73 for P1, P2 being Instruction-Sequence of SCM+FSA for s1, s2 being 0 -started State of SCM+FSA for 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) proof end; canceled; theorem :: SCMFSA8C:74 canceled; theorem :: SCMFSA8C:75 canceled; theorem :: SCMFSA8C:76 canceled; theorem :: SCMFSA8C:77 canceled; theorem :: SCMFSA8C:78 canceled; theorem :: SCMFSA8C:79 canceled; theorem :: SCMFSA8C:80 canceled; theorem :: SCMFSA8C:81 canceled; definition let a be Int-Location; let I be MacroInstruction of SCM+FSA ; func Times (a,I) -> Program of SCM+FSA equals :: SCMFSA8C:def 1 while>0 (a,(I ";" (SubFrom (a,())))); correctness coherence while>0 (a,(I ";" (SubFrom (a,())))) is Program of SCM+FSA ; ; end; :: deftheorem defines Times SCMFSA8C:def 1 : for a being Int-Location for I being MacroInstruction of SCM+FSA holds Times (a,I) = while>0 (a,(I ";" (SubFrom (a,())))); registration let a be Int-Location; let I be MacroInstruction of SCM+FSA ; coherence ( Times (a,I) is halt-ending & Times (a,I) is unique-halt ) proof end; end; theorem :: SCMFSA8C:82 canceled; theorem :: SCMFSA8C:83 canceled; theorem :: SCMFSA8C:84 canceled; theorem :: SCMFSA8C:85 canceled; theorem :: SCMFSA8C:86 canceled; theorem :: SCMFSA8C:87 canceled; ::$CT 6
theorem :: SCMFSA8C:88
for I, J being MacroInstruction of SCM+FSA
for a, c being Int-Location st not I destroys c & not J destroys c holds
( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c )
proof end;

theorem :: SCMFSA8C:89
canceled;

theorem :: SCMFSA8C:90
canceled;

::\$CT 2
theorem :: SCMFSA8C:91
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being good really-closed parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(IExec ((I ";" (SubFrom (a,()))),P,s)) . a = (s . a) - 1
proof end;

Lm1: for aa being Int-Location
for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds
not I ';' J destroys aa

proof end;

Lm2: for aa being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not I ';' () destroys aa

proof end;

Lm3: for aa, bb being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not if>0 (bb,(I ';' ())) destroys aa

proof end;

theorem Th67: :: SCMFSA8C:92
for aa, bb being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not while>0 (bb,I) destroys aa
proof end;

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

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

theorem :: SCMFSA8C:95
for s being State of SCM+FSA
for a being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,p & not I destroys a holds
(IExec (I,p,s)) . a = () . a
proof end;

theorem :: SCMFSA8C:96
for aa being Int-Location
for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds
not I ';' J destroys aa by Lm1;

theorem :: SCMFSA8C:97
for aa being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not I ';' () destroys aa by Lm2;

theorem :: SCMFSA8C:98
for aa, bb being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not if>0 (bb,(I ';' ())) destroys aa by Lm3;

theorem :: SCMFSA8C:99
for aa, bb being Int-Location
for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not if=0 (bb,(I ';' ())) destroys aa
proof end;