:: SCMFSA8C semantic presentation

registration
cluster pseudo-paraclosed FinPartState of SCM+FSA ;
existence
ex b1 being Macro-Instruction st b1 is pseudo-paraclosed
proof end;
end;

theorem Th1: :: SCMFSA8C:1
canceled;

theorem Th2: :: SCMFSA8C:2
for b1 being State of SCM+FSA
for b2 being initial FinPartState of SCM+FSA st b2 is_pseudo-closed_on b1 holds
for b3 being Nat st ( for b4 being Nat st b4 <= b3 holds
IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) in dom b2 ) holds
b3 < pseudo-LifeSpan b1,b2
proof end;

theorem Th3: :: SCMFSA8C:3
canceled;

theorem Th4: :: SCMFSA8C:4
canceled;

theorem Th5: :: SCMFSA8C:5
canceled;

theorem Th6: :: SCMFSA8C:6
for b1 being Function
for b2 being set st b2 in dom b1 holds
b1 +* (b2 .--> (b1 . b2)) = b1
proof end;

theorem Th7: :: SCMFSA8C:7
for b1 being Instruction-Location of SCM+FSA holds b1 + 0 = b1
proof end;

theorem Th8: :: SCMFSA8C:8
for b1 being Instruction of SCM+FSA holds IncAddr b1,0 = b1
proof end;

theorem Th9: :: SCMFSA8C:9
for b1 being programmed FinPartState of SCM+FSA holds ProgramPart (Relocated b1,0) = b1
proof end;

theorem Th10: :: SCMFSA8C:10
for b1, b2 being FinPartState of SCM+FSA st b1 c= b2 holds
ProgramPart b1 c= ProgramPart b2
proof end;

theorem Th11: :: SCMFSA8C:11
for b1, b2 being programmed FinPartState of SCM+FSA
for b3 being Nat st b1 c= b2 holds
Shift b1,b3 c= Shift b2,b3
proof end;

theorem Th12: :: SCMFSA8C:12
for b1, b2 being FinPartState of SCM+FSA
for b3 being Nat st b1 c= b2 holds
ProgramPart (Relocated b1,b3) c= ProgramPart (Relocated b2,b3)
proof end;

theorem Th13: :: SCMFSA8C:13
for b1, b2 being Macro-Instruction
for b3 being Nat st card b1 <= b3 & b3 < (card b1) + (card b2) holds
for b4 being Instruction of SCM+FSA st b4 = b2 . (insloc (b3 -' (card b1))) holds
(b1 ';' b2) . (insloc b3) = IncAddr b4,(card b1)
proof end;

theorem Th14: :: SCMFSA8C:14
for b1 being State of SCM+FSA st b1 . (intloc 0) = 1 & IC b1 = insloc 0 holds
Initialize b1 = b1
proof end;

theorem Th15: :: SCMFSA8C:15
for b1 being State of SCM+FSA holds Initialize (Initialize b1) = Initialize b1
proof end;

theorem Th16: :: SCMFSA8C:16
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds b1 +* ((Initialized b2) +* (Start-At (insloc 0))) = (Initialize b1) +* (b2 +* (Start-At (insloc 0)))
proof end;

theorem Th17: :: SCMFSA8C:17
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds IExec b2,b1 = IExec b2,(Initialize b1)
proof end;

theorem Th18: :: SCMFSA8C:18
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b1 . (intloc 0) = 1 holds
b1 +* (b2 +* (Start-At (insloc 0))) = b1 +* (Initialized b2)
proof end;

theorem Th19: :: SCMFSA8C:19
for b1 being Macro-Instruction holds b1 +* (Start-At (insloc 0)) c= Initialized b1
proof end;

theorem Th20: :: SCMFSA8C:20
for b1 being Instruction-Location of SCM+FSA
for b2 being Macro-Instruction holds
( b1 in dom b2 iff b1 in dom (Initialized b2) )
proof end;

theorem Th21: :: SCMFSA8C:21
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds
( Initialized b2 is_closed_on b1 iff b2 is_closed_on Initialize b1 )
proof end;

theorem Th22: :: SCMFSA8C:22
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds
( Initialized b2 is_halting_on b1 iff b2 is_halting_on Initialize b1 )
proof end;

theorem Th23: :: SCMFSA8C:23
for b1 being Macro-Instruction st ( for b2 being State of SCM+FSA holds b1 is_halting_on Initialize b2 ) holds
Initialized b1 is halting
proof end;

theorem Th24: :: SCMFSA8C:24
for b1 being Macro-Instruction st ( for b2 being State of SCM+FSA holds Initialized b1 is_halting_on b2 ) holds
Initialized b1 is halting
proof end;

theorem Th25: :: SCMFSA8C:25
for b1 being Macro-Instruction holds ProgramPart (Initialized b1) = b1
proof end;

theorem Th26: :: SCMFSA8C:26
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Instruction-Location of SCM+FSA
for b4 being set st b4 in dom b2 holds
b2 . b4 = (b1 +* (b2 +* (Start-At b3))) . b4
proof end;

theorem Th27: :: SCMFSA8C:27
for b1 being State of SCM+FSA st b1 . (intloc 0) = 1 holds
(Initialize b1) | (Int-Locations \/ FinSeq-Locations ) = b1 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th28: :: SCMFSA8C:28
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Int-Location
for b4 being Instruction-Location of SCM+FSA holds (b1 +* (b2 +* (Start-At b4))) . b3 = b1 . b3
proof end;

theorem Th29: :: SCMFSA8C:29
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds IC SCM+FSA in dom (b1 +* (Start-At b2))
proof end;

theorem Th30: :: SCMFSA8C:30
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds (b1 +* (Start-At b2)) . (IC SCM+FSA ) = b2
proof end;

theorem Th31: :: SCMFSA8C:31
for b1 being State of SCM+FSA
for b2 being FinPartState of SCM+FSA
for b3 being Instruction-Location of SCM+FSA holds IC (b1 +* (b2 +* (Start-At b3))) = b3
proof end;

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

theorem Th33: :: SCMFSA8C:33
for b1, b2 being State of SCM+FSA st b1 . (intloc 0) = b2 . (intloc 0) & ( for b3 being read-write Int-Location holds b1 . b3 = b2 . b3 ) & ( for b3 being FinSeq-Location holds b1 . b3 = b2 . b3 ) holds
b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th34: :: SCMFSA8C:34
for b1 being State of SCM+FSA
for b2 being programmed FinPartState of SCM+FSA holds (b1 +* b2) | (Int-Locations \/ FinSeq-Locations ) = b1 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th35: :: SCMFSA8C:35
for b1, b2 being State of SCM+FSA holds (b1 +* (b2 | the Instruction-Locations of SCM+FSA )) | (Int-Locations \/ FinSeq-Locations ) = b1 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th36: :: SCMFSA8C:36
for b1 being State of SCM+FSA holds (Initialize b1) | the Instruction-Locations of SCM+FSA = b1 | the Instruction-Locations of SCM+FSA
proof end;

theorem Th37: :: SCMFSA8C:37
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction holds (b2 +* (b1 | the Instruction-Locations of SCM+FSA )) | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th38: :: SCMFSA8C:38
for b1 being State of SCM+FSA holds IExec SCM+FSA-Stop ,b1 = (Initialize b1) +* (Start-At (insloc 0))
proof end;

theorem Th39: :: SCMFSA8C:39
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 holds
insloc 0 in dom b2
proof end;

theorem Th40: :: SCMFSA8C:40
for b1 being State of SCM+FSA
for b2 being paraclosed Macro-Instruction holds insloc 0 in dom b2
proof end;

theorem Th41: :: SCMFSA8C:41
for b1 being Instruction of SCM+FSA holds rng (Macro b1) = {b1,(halt SCM+FSA )}
proof end;

theorem Th42: :: SCMFSA8C:42
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 is_closed_on b1 & b3 +* (Start-At (insloc 0)) c= b1 holds
for b4 being Nat st ProgramPart (Relocated b3,b4) c= b2 & IC b2 = insloc b4 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
for b5 being Nat holds
( (IC ((Computation b1) . b5)) + b4 = IC ((Computation b2) . b5) & IncAddr (CurInstr ((Computation b1) . b5)),b4 = CurInstr ((Computation b2) . b5) & ((Computation b1) . b5) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b2) . b5) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th43: :: SCMFSA8C:43
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 is_closed_on b1 & b3 +* (Start-At (insloc 0)) c= b1 & b3 +* (Start-At (insloc 0)) c= b2 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
for b4 being Nat holds
( IC ((Computation b1) . b4) = IC ((Computation b2) . b4) & CurInstr ((Computation b1) . b4) = CurInstr ((Computation b2) . b4) & ((Computation b1) . b4) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b2) . b4) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th44: :: SCMFSA8C:44
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 is_closed_on b1 & b3 is_halting_on b1 & b3 +* (Start-At (insloc 0)) c= b1 & b3 +* (Start-At (insloc 0)) c= b2 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
LifeSpan b1 = LifeSpan b2
proof end;

theorem Th45: :: SCMFSA8C:45
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b1 . (intloc 0) = 1 & b3 is_closed_on b1 & b3 is_halting_on b1 & ( for b4 being read-write Int-Location holds b1 . b4 = b2 . b4 ) & ( for b4 being FinSeq-Location holds b1 . b4 = b2 . b4 ) holds
(IExec b3,b1) | (Int-Locations \/ FinSeq-Locations ) = (IExec b3,b2) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th46: :: SCMFSA8C:46
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b1 . (intloc 0) = 1 & b3 is_closed_on b1 & b3 is_halting_on b1 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
(IExec b3,b1) | (Int-Locations \/ FinSeq-Locations ) = (IExec b3,b2) | (Int-Locations \/ FinSeq-Locations )
proof end;

registration
let c1 be Macro-Instruction;
cluster Initialized a1 -> initial ;
correctness
coherence
Initialized c1 is initial;
proof end;
end;

E37: now
let c1 be State of SCM+FSA ;
let c2 be Macro-Instruction;
E38: ProgramPart (Initialized c2) = c2 by Th25;
hereby
assume E39: Initialized c2 is_pseudo-closed_on c1 ;
set c3 = pseudo-LifeSpan c1,(Initialized c2);
( IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . (pseudo-LifeSpan c1,(Initialized c2))) = insloc (card (ProgramPart (Initialized c2))) & ( for b1 being Nat st b1 < pseudo-LifeSpan c1,(Initialized c2) holds
IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . b1) in dom (Initialized c2) ) ) by E39, SCMFSA8A:def 5;
then IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . (pseudo-LifeSpan c1,(Initialized c2))) = insloc (card (ProgramPart (Initialized c2))) by Th16;
then E40: IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . (pseudo-LifeSpan c1,(Initialized c2))) = insloc (card (ProgramPart c2)) by E38, AMI_5:72;
E41: now
let c4 be Nat;
assume c4 < pseudo-LifeSpan c1,(Initialized c2) ;
then IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . c4) in dom (Initialized c2) by E39, SCMFSA8A:def 5;
then IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . c4) in dom (Initialized c2) by Th16;
hence IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . c4) in dom c2 by Th20;
end;
then E42: for b1 being Nat st not IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . b1) in dom c2 holds
pseudo-LifeSpan c1,(Initialized c2) <= b1 ;
thus c2 is_pseudo-closed_on Initialize c1 by E40, E41, SCMFSA8A:def 3;
hence pseudo-LifeSpan c1,(Initialized c2) = pseudo-LifeSpan (Initialize c1),c2 by E40, E42, SCMFSA8A:def 5;
end;
assume E39: c2 is_pseudo-closed_on Initialize c1 ;
set c3 = pseudo-LifeSpan (Initialize c1),c2;
( IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . (pseudo-LifeSpan (Initialize c1),c2)) = insloc (card (ProgramPart c2)) & ( for b1 being Nat st b1 < pseudo-LifeSpan (Initialize c1),c2 holds
IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . b1) in dom c2 ) ) by E39, SCMFSA8A:def 5;
then IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . (pseudo-LifeSpan (Initialize c1),c2)) = insloc (card (ProgramPart c2)) by Th16;
then E40: IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . (pseudo-LifeSpan (Initialize c1),c2)) = insloc (card (ProgramPart (Initialized c2))) by E38, AMI_5:72;
E41: now
let c4 be Nat;
assume c4 < pseudo-LifeSpan (Initialize c1),c2 ;
then IC ((Computation ((Initialize c1) +* (c2 +* (Start-At (insloc 0))))) . c4) in dom c2 by E39, SCMFSA8A:def 5;
then IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . c4) in dom c2 by Th16;
hence IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . c4) in dom (Initialized c2) by Th20;
end;
then E42: for b1 being Nat st not IC ((Computation (c1 +* ((Initialized c2) +* (Start-At (insloc 0))))) . b1) in dom (Initialized c2) holds
pseudo-LifeSpan (Initialize c1),c2 <= b1 ;
thus Initialized c2 is_pseudo-closed_on c1 by E40, E41, SCMFSA8A:def 3;
hence pseudo-LifeSpan c1,(Initialized c2) = pseudo-LifeSpan (Initialize c1),c2 by E40, E42, SCMFSA8A:def 5;
end;

theorem Th47: :: SCMFSA8C:47
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds
( Initialized b2 is_pseudo-closed_on b1 iff b2 is_pseudo-closed_on Initialize b1 ) by Lemma37;

theorem Th48: :: SCMFSA8C:48
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_pseudo-closed_on Initialize b1 holds
pseudo-LifeSpan b1,(Initialized b2) = pseudo-LifeSpan (Initialize b1),b2 by Lemma37;

theorem Th49: :: SCMFSA8C:49
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st Initialized b2 is_pseudo-closed_on b1 holds
pseudo-LifeSpan b1,(Initialized b2) = pseudo-LifeSpan (Initialize b1),b2 by Lemma37;

theorem Th50: :: SCMFSA8C:50
for b1 being State of SCM+FSA
for b2 being initial FinPartState of SCM+FSA st b2 is_pseudo-closed_on b1 holds
( b2 is_pseudo-closed_on b1 +* (b2 +* (Start-At (insloc 0))) & pseudo-LifeSpan b1,b2 = pseudo-LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))),b2 )
proof end;

theorem Th51: :: SCMFSA8C:51
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 +* (Start-At (insloc 0)) c= b1 & b3 is_pseudo-closed_on b1 holds
for b4 being Nat st ProgramPart (Relocated b3,b4) c= b2 & IC b2 = insloc b4 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
( ( for b5 being Nat st b5 < pseudo-LifeSpan b1,b3 holds
IncAddr (CurInstr ((Computation b1) . b5)),b4 = CurInstr ((Computation b2) . b5) ) & ( for b5 being Nat st b5 <= pseudo-LifeSpan b1,b3 holds
( (IC ((Computation b1) . b5)) + b4 = IC ((Computation b2) . b5) & ((Computation b1) . b5) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b2) . b5) | (Int-Locations \/ FinSeq-Locations ) ) ) )
proof end;

theorem Th52: :: SCMFSA8C:52
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) & b3 is_pseudo-closed_on b1 holds
b3 is_pseudo-closed_on b2
proof end;

theorem Th53: :: SCMFSA8C:53
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b1 . (intloc 0) = 1 holds
( b2 is_pseudo-closed_on b1 iff b2 is_pseudo-closed_on Initialize b1 )
proof end;

Lemma42: for b1 being Instruction-Location of SCM+FSA holds goto b1 <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;

Lemma43: for b1 being Int-Location
for b2 being Instruction-Location of SCM+FSA holds b1 =0_goto b2 <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;

Lemma44: for b1 being Int-Location
for b2 being Instruction-Location of SCM+FSA holds b1 >0_goto b2 <> halt SCM+FSA
by SCMFSA_2:49, SCMFSA_2:124;

Lemma45: for b1, b2 being Macro-Instruction holds ProgramPart (Relocated b2,(card b1)) c= b1 ';' b2
proof end;

theorem Th54: :: SCMFSA8C:54
for b1 being Int-Location
for b2, b3 being Macro-Instruction holds
( insloc 0 in dom (if=0 b1,b2,b3) & insloc 1 in dom (if=0 b1,b2,b3) & insloc 0 in dom (if>0 b1,b2,b3) & insloc 1 in dom (if>0 b1,b2,b3) )
proof end;

theorem Th55: :: SCMFSA8C:55
for b1 being Int-Location
for b2, b3 being Macro-Instruction holds
( (if=0 b1,b2,b3) . (insloc 0) = b1 =0_goto (insloc ((card b3) + 3)) & (if=0 b1,b2,b3) . (insloc 1) = goto (insloc 2) & (if>0 b1,b2,b3) . (insloc 0) = b1 >0_goto (insloc ((card b3) + 3)) & (if>0 b1,b2,b3) . (insloc 1) = goto (insloc 2) )
proof end;

theorem Th56: :: SCMFSA8C:56
for b1 being Int-Location
for b2, b3 being Macro-Instruction
for b4 being Nat st b4 < ((card b2) + (card b3)) + 3 holds
( insloc b4 in dom (if=0 b1,b2,b3) & (if=0 b1,b2,b3) . (insloc b4) <> halt SCM+FSA )
proof end;

theorem Th57: :: SCMFSA8C:57
for b1 being Int-Location
for b2, b3 being Macro-Instruction
for b4 being Nat st b4 < ((card b2) + (card b3)) + 3 holds
( insloc b4 in dom (if>0 b1,b2,b3) & (if>0 b1,b2,b3) . (insloc b4) <> halt SCM+FSA )
proof end;

theorem Th58: :: SCMFSA8C:58
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st Directed b2 is_pseudo-closed_on b1 holds
( b2 ';' SCM+FSA-Stop is_closed_on b1 & b2 ';' SCM+FSA-Stop is_halting_on b1 & LifeSpan (b1 +* ((b2 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0)))) = pseudo-LifeSpan b1,(Directed b2) & ( for b3 being Nat st b3 < pseudo-LifeSpan b1,(Directed b2) holds
IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) = IC ((Computation (b1 +* ((b2 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . b3) ) & ( for b3 being Nat st b3 <= pseudo-LifeSpan b1,(Directed b2) holds
((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* ((b2 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . b3) | (Int-Locations \/ FinSeq-Locations ) ) )
proof end;

theorem Th59: :: SCMFSA8C:59
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st Directed b2 is_pseudo-closed_on b1 holds
(Result (b1 +* ((b2 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . (pseudo-LifeSpan b1,(Directed b2))) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th60: :: SCMFSA8C:60
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b1 . (intloc 0) = 1 & Directed b2 is_pseudo-closed_on b1 holds
(IExec (b2 ';' SCM+FSA-Stop ),b1) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . (pseudo-LifeSpan b1,(Directed b2))) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th61: :: SCMFSA8C:61
for b1, b2 being Macro-Instruction
for b3 being Int-Location holds (if=0 b3,b1,b2) . (insloc (((card b1) + (card b2)) + 3)) = halt SCM+FSA
proof end;

theorem Th62: :: SCMFSA8C:62
for b1, b2 being Macro-Instruction
for b3 being Int-Location holds (if>0 b3,b1,b2) . (insloc (((card b1) + (card b2)) + 3)) = halt SCM+FSA
proof end;

theorem Th63: :: SCMFSA8C:63
for b1, b2 being Macro-Instruction
for b3 being Int-Location holds (if=0 b3,b1,b2) . (insloc ((card b2) + 2)) = goto (insloc (((card b1) + (card b2)) + 3))
proof end;

theorem Th64: :: SCMFSA8C:64
for b1, b2 being Macro-Instruction
for b3 being Int-Location holds (if>0 b3,b1,b2) . (insloc ((card b2) + 2)) = goto (insloc (((card b1) + (card b2)) + 3))
proof end;

theorem Th65: :: SCMFSA8C:65
for b1 being Macro-Instruction
for b2 being Int-Location holds (if=0 b2,(Goto (insloc 2)),b1) . (insloc ((card b1) + 3)) = goto (insloc ((card b1) + 5))
proof end;

theorem Th66: :: SCMFSA8C:66
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . b4 = 0 & Directed b2 is_pseudo-closed_on b1 holds
( if=0 b4,b2,b3 is_halting_on b1 & if=0 b4,b2,b3 is_closed_on b1 & LifeSpan (b1 +* ((if=0 b4,b2,b3) +* (Start-At (insloc 0)))) = (LifeSpan (b1 +* ((b2 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 1 )
proof end;

theorem Th67: :: SCMFSA8C:67
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . (intloc 0) = 1 & b1 . b4 = 0 & Directed b2 is_pseudo-closed_on b1 holds
(IExec (if=0 b4,b2,b3),b1) | (Int-Locations \/ FinSeq-Locations ) = (IExec (b2 ';' SCM+FSA-Stop ),b1) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th68: :: SCMFSA8C:68
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . b4 > 0 & Directed b2 is_pseudo-closed_on b1 holds
( if>0 b4,b2,b3 is_halting_on b1 & if>0 b4,b2,b3 is_closed_on b1 & LifeSpan (b1 +* ((if>0 b4,b2,b3) +* (Start-At (insloc 0)))) = (LifeSpan (b1 +* ((b2 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 1 )
proof end;

theorem Th69: :: SCMFSA8C:69
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . (intloc 0) = 1 & b1 . b4 > 0 & Directed b2 is_pseudo-closed_on b1 holds
(IExec (if>0 b4,b2,b3),b1) | (Int-Locations \/ FinSeq-Locations ) = (IExec (b2 ';' SCM+FSA-Stop ),b1) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th70: :: SCMFSA8C:70
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . b4 <> 0 & Directed b3 is_pseudo-closed_on b1 holds
( if=0 b4,b2,b3 is_halting_on b1 & if=0 b4,b2,b3 is_closed_on b1 & LifeSpan (b1 +* ((if=0 b4,b2,b3) +* (Start-At (insloc 0)))) = (LifeSpan (b1 +* ((b3 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 3 )
proof end;

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

theorem Th72: :: SCMFSA8C:72
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . b4 <= 0 & Directed b3 is_pseudo-closed_on b1 holds
( if>0 b4,b2,b3 is_halting_on b1 & if>0 b4,b2,b3 is_closed_on b1 & LifeSpan (b1 +* ((if>0 b4,b2,b3) +* (Start-At (insloc 0)))) = (LifeSpan (b1 +* ((b3 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 3 )
proof end;

theorem Th73: :: SCMFSA8C:73
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st b1 . (intloc 0) = 1 & b1 . b4 <= 0 & Directed b3 is_pseudo-closed_on b1 holds
(IExec (if>0 b4,b2,b3),b1) | (Int-Locations \/ FinSeq-Locations ) = (IExec (b3 ';' SCM+FSA-Stop ),b1) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th74: :: SCMFSA8C:74
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st Directed b2 is_pseudo-closed_on b1 & Directed b3 is_pseudo-closed_on b1 holds
( if=0 b4,b2,b3 is_closed_on b1 & if=0 b4,b2,b3 is_halting_on b1 )
proof end;

theorem Th75: :: SCMFSA8C:75
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being read-write Int-Location st Directed b2 is_pseudo-closed_on b1 & Directed b3 is_pseudo-closed_on b1 holds
( if>0 b4,b2,b3 is_closed_on b1 & if>0 b4,b2,b3 is_halting_on b1 )
proof end;

theorem Th76: :: SCMFSA8C:76
for b1 being Macro-Instruction
for b2 being Int-Location st b1 does_not_destroy b2 holds
Directed b1 does_not_destroy b2
proof end;

theorem Th77: :: SCMFSA8C:77
for b1 being Instruction of SCM+FSA
for b2 being Int-Location st b1 does_not_destroy b2 holds
Macro b1 does_not_destroy b2
proof end;

theorem Th78: :: SCMFSA8C:78
for b1 being Int-Location holds halt SCM+FSA does_not_refer b1
proof end;

theorem Th79: :: SCMFSA8C:79
for b1, b2, b3 being Int-Location st b1 <> b2 holds
AddTo b3,b2 does_not_refer b1
proof end;

theorem Th80: :: SCMFSA8C:80
for b1 being Instruction of SCM+FSA
for b2 being Int-Location st b1 does_not_refer b2 holds
Macro b1 does_not_refer b2
proof end;

theorem Th81: :: SCMFSA8C:81
for b1, b2 being Macro-Instruction
for b3 being Int-Location st b1 does_not_destroy b3 & b2 does_not_destroy b3 holds
b1 ';' b2 does_not_destroy b3
proof end;

theorem Th82: :: SCMFSA8C:82
for b1 being Macro-Instruction
for b2 being Instruction of SCM+FSA
for b3 being Int-Location st b2 does_not_destroy b3 & b1 does_not_destroy b3 holds
b2 ';' b1 does_not_destroy b3
proof end;

theorem Th83: :: SCMFSA8C:83
for b1 being Macro-Instruction
for b2 being Instruction of SCM+FSA
for b3 being Int-Location st b1 does_not_destroy b3 & b2 does_not_destroy b3 holds
b1 ';' b2 does_not_destroy b3
proof end;

theorem Th84: :: SCMFSA8C:84
for b1, b2 being Instruction of SCM+FSA
for b3 being Int-Location st b1 does_not_destroy b3 & b2 does_not_destroy b3 holds
b1 ';' b2 does_not_destroy b3
proof end;

theorem Th85: :: SCMFSA8C:85
for b1 being Int-Location holds SCM+FSA-Stop does_not_destroy b1
proof end;

theorem Th86: :: SCMFSA8C:86
for b1 being Int-Location
for b2 being Instruction-Location of SCM+FSA holds Goto b2 does_not_destroy b1
proof end;

theorem Th87: :: SCMFSA8C:87
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_halting_on Initialize b1 holds
( ( for b3 being read-write Int-Location holds (IExec b2,b1) . b3 = ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize b1) +* (b2 +* (Start-At (insloc 0)))))) . b3 ) & ( for b3 being FinSeq-Location holds (IExec b2,b1) . b3 = ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize b1) +* (b2 +* (Start-At (insloc 0)))))) . b3 ) )
proof end;

theorem Th88: :: SCMFSA8C:88
for b1 being State of SCM+FSA
for b2 being parahalting Macro-Instruction
for b3 being read-write Int-Location holds (IExec b2,b1) . b3 = ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize b1) +* (b2 +* (Start-At (insloc 0)))))) . b3
proof end;

theorem Th89: :: SCMFSA8C:89
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Int-Location
for b4 being Nat st b2 is_closed_on Initialize b1 & b2 is_halting_on Initialize b1 & b2 does_not_destroy b3 holds
(IExec b2,b1) . b3 = ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . b4) . b3
proof end;

theorem Th90: :: SCMFSA8C:90
for b1 being State of SCM+FSA
for b2 being parahalting Macro-Instruction
for b3 being Int-Location
for b4 being Nat st b2 does_not_destroy b3 holds
(IExec b2,b1) . b3 = ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . b4) . b3
proof end;

theorem Th91: :: SCMFSA8C:91
for b1 being State of SCM+FSA
for b2 being parahalting Macro-Instruction
for b3 being Int-Location st b2 does_not_destroy b3 holds
(IExec b2,b1) . b3 = (Initialize b1) . b3
proof end;

theorem Th92: :: SCMFSA8C:92
for b1 being State of SCM+FSA
for b2 being keeping_0 Macro-Instruction st b2 is_halting_on Initialize b1 holds
( (IExec b2,b1) . (intloc 0) = 1 & ( for b3 being Nat holds ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . b3) . (intloc 0) = 1 ) )
proof end;

theorem Th93: :: SCMFSA8C:93
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Int-Location st b2 does_not_destroy b3 holds
for b4 being Nat st IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) in dom b2 holds
((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . (b4 + 1)) . b3 = ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) . b3
proof end;

theorem Th94: :: SCMFSA8C:94
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Int-Location st b2 does_not_destroy b3 holds
for b4 being Nat st ( for b5 being Nat st b5 < b4 holds
IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b5) in dom b2 ) holds
for b5 being Nat st b5 <= b4 holds
((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b5) . b3 = b1 . b3
proof end;

theorem Th95: :: SCMFSA8C:95
for b1 being State of SCM+FSA
for b2 being good Macro-Instruction
for b3 being Nat st ( for b4 being Nat st b4 < b3 holds
IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) in dom b2 ) holds
for b4 being Nat st b4 <= b3 holds
((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) . (intloc 0) = b1 . (intloc 0)
proof end;

theorem Th96: :: SCMFSA8C:96
for b1 being State of SCM+FSA
for b2 being good Macro-Instruction st b2 is_halting_on Initialize b1 & b2 is_closed_on Initialize b1 holds
( (IExec b2,b1) . (intloc 0) = 1 & ( for b3 being Nat holds ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . b3) . (intloc 0) = 1 ) )
proof end;

theorem Th97: :: SCMFSA8C:97
for b1 being State of SCM+FSA
for b2 being good Macro-Instruction st b2 is_closed_on b1 holds
for b3 being Nat holds ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) . (intloc 0) = b1 . (intloc 0)
proof end;

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

theorem Th99: :: SCMFSA8C:99
for b1 being Instruction of SCM+FSA st b1 does_not_destroy intloc 0 holds
Macro b1 is good
proof end;

theorem Th100: :: SCMFSA8C:100
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 is_closed_on b1 & b3 is_halting_on b1 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
for b4 being Nat holds
( (Computation (b1 +* (b3 +* (Start-At (insloc 0))))) . b4,(Computation (b2 +* (b3 +* (Start-At (insloc 0))))) . b4 equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation (b1 +* (b3 +* (Start-At (insloc 0))))) . b4) = CurInstr ((Computation (b2 +* (b3 +* (Start-At (insloc 0))))) . b4) )
proof end;

theorem Th101: :: SCMFSA8C:101
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 is_closed_on b1 & b3 is_halting_on b1 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) holds
( LifeSpan (b1 +* (b3 +* (Start-At (insloc 0)))) = LifeSpan (b2 +* (b3 +* (Start-At (insloc 0)))) & Result (b1 +* (b3 +* (Start-At (insloc 0)))), Result (b2 +* (b3 +* (Start-At (insloc 0)))) equal_outside the Instruction-Locations of SCM+FSA )
proof end;

theorem Th102: :: SCMFSA8C:102
canceled;

theorem Th103: :: SCMFSA8C:103
for b1, b2 being State of SCM+FSA
for b3 being Macro-Instruction st b3 is_closed_on b1 & b3 is_halting_on b1 & b3 +* (Start-At (insloc 0)) c= b1 & b3 +* (Start-At (insloc 0)) c= b2 & ex b4 being Nat st (Computation b1) . b4,b2 equal_outside the Instruction-Locations of SCM+FSA holds
Result b1, Result b2 equal_outside the Instruction-Locations of SCM+FSA
proof end;

registration
let c1 be Macro-Instruction;
let c2 be Nat;
cluster IncAddr a1,a2 -> initial ;
correctness
coherence
( IncAddr c1,c2 is initial & IncAddr c1,c2 is programmed );
proof end;
end;

definition
let c1 be Macro-Instruction;
canceled;
canceled;
canceled;
func loop c1 -> halt-free Macro-Instruction equals :: SCMFSA8C:def 4
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 0)))) * a1;
coherence
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 0)))) * c1 is halt-free Macro-Instruction
proof end;
end;

:: deftheorem Def1 SCMFSA8C:def 1 :
canceled;

:: deftheorem Def2 SCMFSA8C:def 2 :
canceled;

:: deftheorem Def3 SCMFSA8C:def 3 :
canceled;

:: deftheorem Def4 defines loop SCMFSA8C:def 4 :
for b1 being Macro-Instruction holds loop b1 = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 0)))) * b1;

theorem Th104: :: SCMFSA8C:104
for b1 being Macro-Instruction holds loop b1 = Directed b1,(insloc 0) by SCMFSA8A:def 1;

theorem Th105: :: SCMFSA8C:105
for b1 being Macro-Instruction
for b2 being Int-Location st b1 does_not_destroy b2 holds
loop b1 does_not_destroy b2
proof end;

registration
let c1 be good Macro-Instruction;
cluster loop a1 -> good halt-free ;
correctness
coherence
loop c1 is good;
proof end;
end;

theorem Th106: :: SCMFSA8C:106
for b1 being Macro-Instruction holds dom (loop b1) = dom b1
proof end;

theorem Th107: :: SCMFSA8C:107
for b1 being Macro-Instruction holds not halt SCM+FSA in rng (loop b1)
proof end;

theorem Th108: :: SCMFSA8C:108
for b1 being Macro-Instruction
for b2 being set st b1 . b2 <> halt SCM+FSA holds
(loop b1) . b2 = b1 . b2
proof end;

theorem Th109: :: SCMFSA8C:109
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
for b3 being Nat st b3 <= LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))) holds
(Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3,(Computation (b1 +* ((loop b2) +* (Start-At (insloc 0))))) . b3 equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem Th110: :: SCMFSA8C:110
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
for b3 being Nat st b3 < LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))) holds
CurInstr ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) = CurInstr ((Computation (b1 +* ((loop b2) +* (Start-At (insloc 0))))) . b3)
proof end;

Lemma91: for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( CurInstr ((Computation (b1 +* ((loop b2) +* (Start-At (insloc 0))))) . (LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))))) = goto (insloc 0) & ( for b3 being Nat st b3 <= LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))) holds
CurInstr ((Computation (b1 +* ((loop b2) +* (Start-At (insloc 0))))) . b3) <> halt SCM+FSA ) )
proof end;

theorem Th111: :: SCMFSA8C:111
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
for b3 being Nat st b3 <= LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))) holds
CurInstr ((Computation (b1 +* ((loop b2) +* (Start-At (insloc 0))))) . b3) <> halt SCM+FSA by Lemma91;

theorem Th112: :: SCMFSA8C:112
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
CurInstr ((Computation (b1 +* ((loop b2) +* (Start-At (insloc 0))))) . (LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))))) = goto (insloc 0) by Lemma91;

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

theorem Th114: :: SCMFSA8C:114
for b1 being State of SCM+FSA
for b2 being parahalting Macro-Instruction st Initialized b2 c= b1 holds
for b3 being Nat st b3 <= LifeSpan b1 holds
CurInstr ((Computation (b1 +* (loop b2))) . b3) <> halt SCM+FSA
proof end;

definition
let c1 be Int-Location ;
let c2 be Macro-Instruction;
func Times c1,c2 -> Macro-Instruction equals :: SCMFSA8C:def 5
 if>0 a1,(loop (if=0 a1,(Goto (insloc 2)),(a2 ';' (SubFrom a1,(intloc 0))))),SCM+FSA-Stop ;
correctness
coherence
if>0 c1,(loop (if=0 c1,(Goto (insloc 2)),(c2 ';' (SubFrom c1,(intloc 0))))),SCM+FSA-Stop is Macro-Instruction;
;
end;

:: deftheorem Def5 defines Times SCMFSA8C:def 5 :
for b1 being Int-Location
for b2 being Macro-Instruction holds Times b1,b2 = if>0 b1,(loop (if=0 b1,(Goto (insloc 2)),(b2 ';' (SubFrom b1,(intloc 0))))),SCM+FSA-Stop ;

theorem Th115: :: SCMFSA8C:115
for b1 being good Macro-Instruction
for b2 being read-write Int-Location holds if=0 b2,(Goto (insloc 2)),(b1 ';' (SubFrom b2,(intloc 0))) is good
proof end;

theorem Th116: :: SCMFSA8C:116
for b1, b2 being Macro-Instruction
for b3 being Int-Location holds (if=0 b3,(Goto (insloc 2)),(b1 ';' (SubFrom b3,(intloc 0)))) . (insloc ((card (b1 ';' (SubFrom b3,(intloc 0)))) + 3)) = goto (insloc ((card (b1 ';' (SubFrom b3,(intloc 0)))) + 5))
proof end;

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

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

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

theorem Th120: :: SCMFSA8C:120
for b1 being parahalting good Macro-Instruction
for b2 being read-write Int-Location st b1 does_not_destroy b2 holds
Initialized (Times b2,b1) is halting
proof end;

theorem Th121: :: SCMFSA8C:121
for b1, b2 being Macro-Instruction
for b3, b4 being Int-Location st b1 does_not_destroy b4 & b2 does_not_destroy b4 holds
( if=0 b3,b1,b2 does_not_destroy b4 & if>0 b3,b1,b2 does_not_destroy b4 )
proof end;

theorem Th122: :: SCMFSA8C:122
for b1 being State of SCM+FSA
for b2 being parahalting good Macro-Instruction
for b3 being read-write Int-Location st b2 does_not_destroy b3 & b1 . (intloc 0) = 1 & b1 . b3 > 0 holds
ex b4 being State of SCM+FSA ex b5 being Nat st
( b4 = b1 +* ((loop (if=0 b3,(Goto (insloc 2)),(b2 ';' (SubFrom b3,(intloc 0))))) +* (Start-At (insloc 0))) & b5 = (LifeSpan (b1 +* ((if=0 b3,(Goto (insloc 2)),(b2 ';' (SubFrom b3,(intloc 0)))) +* (Start-At (insloc 0))))) + 1 & ((Computation b4) . b5) . b3 = (b1 . b3) - 1 & ((Computation b4) . b5) . (intloc 0) = 1 & ( for b6 being read-write Int-Location st b6 <> b3 holds
((Computation b4) . b5) . b6 = (IExec b2,b1) . b6 ) & ( for b6 being FinSeq-Location holds ((Computation b4) . b5) . b6 = (IExec b2,b1) . b6 ) & IC ((Computation b4) . b5) = insloc 0 & ( for b6 being Nat st b6 <= b5 holds
IC ((Computation b4) . b6) in dom (loop (if=0 b3,(Goto (insloc 2)),(b2 ';' (SubFrom b3,(intloc 0))))) ) )
proof end;

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

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

theorem Th125: :: SCMFSA8C:125
for b1 being State of SCM+FSA
for b2, b3, b4 being read-write Int-Location st b2 <> b3 & b2 <> b4 & b3 <> b4 & b1 . b2 >= 0 holds
(IExec (Times b2,(Macro (AddTo b3,b4))),b1) . b3 = (b1 . b3) + ((b1 . b4) * (b1 . b2))
proof end;