:: SCMFSA8A semantic presentation

set c1 = the Instruction-Locations of SCM+FSA ;

set c2 = Int-Locations \/ FinSeq-Locations ;

theorem Th1: :: SCMFSA8A:1
canceled;

theorem Th2: :: SCMFSA8A:2
for b1, b2 being Function
for b3 being set st dom b2 misses b3 holds
(b1 +* b2) | b3 = b1 | b3
proof end;

theorem Th3: :: SCMFSA8A:3
for b1 being State of SCM+FSA holds dom (b1 | the Instruction-Locations of SCM+FSA ) = the Instruction-Locations of SCM+FSA
proof end;

theorem Th4: :: SCMFSA8A:4
for b1 being State of SCM+FSA st b1 is halting holds
for b2 being Nat st LifeSpan b1 <= b2 holds
CurInstr ((Computation b1) . b2) = halt SCM+FSA
proof end;

theorem Th5: :: SCMFSA8A:5
for b1 being State of SCM+FSA st b1 is halting holds
for b2 being Nat st LifeSpan b1 <= b2 holds
IC ((Computation b1) . b2) = IC ((Computation b1) . (LifeSpan b1))
proof end;

theorem Th6: :: SCMFSA8A:6
for b1, b2 being State of SCM+FSA holds
( b1,b2 equal_outside the Instruction-Locations of SCM+FSA iff ( IC b1 = IC b2 & b1 | (Int-Locations \/ FinSeq-Locations ) = b2 | (Int-Locations \/ FinSeq-Locations ) ) )
proof end;

theorem Th7: :: SCMFSA8A:7
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds IC (IExec b2,b1) = IC (Result (b1 +* (Initialized b2)))
proof end;

theorem Th8: :: SCMFSA8A:8
for b1 being State of SCM+FSA
for b2 being Macro-Instruction holds (Initialize b1) +* (Initialized b2) = b1 +* (Initialized b2)
proof end;

theorem Th9: :: SCMFSA8A:9
for b1 being Macro-Instruction
for b2 being Instruction-Location of SCM+FSA holds b1 c= b1 +* (Start-At b2)
proof end;

theorem Th10: :: SCMFSA8A:10
for b1 being State of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds b1 | (Int-Locations \/ FinSeq-Locations ) = (b1 +* (Start-At b2)) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th11: :: SCMFSA8A:11
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Instruction-Location of SCM+FSA holds b1 | (Int-Locations \/ FinSeq-Locations ) = (b1 +* (b2 +* (Start-At b3))) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th12: :: SCMFSA8A:12
for b1 being State of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds dom (b1 | the Instruction-Locations of SCM+FSA ) misses dom (Start-At b2)
proof end;

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

theorem Th14: :: SCMFSA8A:14
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction
for b4 being Instruction-Location of SCM+FSA holds b1 +* (b2 +* (Start-At b4)),b1 +* (b3 +* (Start-At b4)) equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem Th15: :: SCMFSA8A:15
dom SCM+FSA-Stop = {(insloc 0)} by CQC_LANG:5, SCMFSA_4:def 5;

theorem Th16: :: SCMFSA8A:16
( insloc 0 in dom SCM+FSA-Stop & SCM+FSA-Stop . (insloc 0) = halt SCM+FSA ) by Th15, CQC_LANG:6, SCMFSA_4:def 5, TARSKI:def 1;

theorem Th17: :: SCMFSA8A:17
card SCM+FSA-Stop = 1
proof end;

definition
let c3 be programmed FinPartState of SCM+FSA ;
let c4 be Instruction-Location of SCM+FSA ;
func Directed c1,c2 -> programmed FinPartState of SCM+FSA equals :: SCMFSA8A:def 1
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto a2))) * a1;
coherence
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto c4))) * c3 is programmed FinPartState of SCM+FSA
proof end;
end;

:: deftheorem Def1 defines Directed SCMFSA8A:def 1 :
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds Directed b1,b2 = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto b2))) * b1;

theorem Th18: :: SCMFSA8A:18
for b1 being programmed FinPartState of SCM+FSA holds Directed b1 = Directed b1,(insloc (card b1)) by SCMFSA6A:def 1;

registration
let c3 be programmed FinPartState of SCM+FSA ;
let c4 be Instruction-Location of SCM+FSA ;
cluster Directed a1,a2 -> programmed halt-free ;
correctness
coherence
Directed c3,c4 is halt-free;
proof end;
end;

registration
let c3 be programmed FinPartState of SCM+FSA ;
cluster Directed a1 -> halt-free ;
correctness
coherence
Directed c3 is halt-free;
proof end;
end;

theorem Th19: :: SCMFSA8A:19
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds dom (Directed b1,b2) = dom b1
proof end;

theorem Th20: :: SCMFSA8A:20
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds Directed b1,b2 = b1 +* (((halt SCM+FSA ) .--> (goto b2)) * b1)
proof end;

theorem Th21: :: SCMFSA8A:21
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA
for b3 being set st b3 in dom b1 holds
( ( b1 . b3 = halt SCM+FSA implies (Directed b1,b2) . b3 = goto b2 ) & ( b1 . b3 <> halt SCM+FSA implies (Directed b1,b2) . b3 = b1 . b3 ) )
proof end;

theorem Th22: :: SCMFSA8A:22
for b1 being Instruction of SCM+FSA
for b2 being Int-Location
for b3 being Nat st b1 does_not_destroy b2 holds
IncAddr b1,b3 does_not_destroy b2
proof end;

theorem Th23: :: SCMFSA8A:23
for b1 being programmed FinPartState of SCM+FSA
for b2 being Nat
for b3 being Int-Location st b1 does_not_destroy b3 holds
ProgramPart (Relocated b1,b2) does_not_destroy b3
proof end;

theorem Th24: :: SCMFSA8A:24
for b1 being programmed good FinPartState of SCM+FSA
for b2 being Nat holds ProgramPart (Relocated b1,b2) is good
proof end;

theorem Th25: :: SCMFSA8A:25
for b1, b2 being programmed FinPartState 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 Th26: :: SCMFSA8A:26
for b1, b2 being programmed good FinPartState of SCM+FSA holds b1 +* b2 is good
proof end;

theorem Th27: :: SCMFSA8A:27
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA
for b3 being Int-Location st b1 does_not_destroy b3 holds
Directed b1,b2 does_not_destroy b3
proof end;

registration
let c3 be programmed good FinPartState of SCM+FSA ;
let c4 be Instruction-Location of SCM+FSA ;
cluster Directed a1,a2 -> programmed good halt-free ;
correctness
coherence
Directed c3,c4 is good;
proof end;
end;

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

registration
let c3 be Macro-Instruction;
let c4 be Instruction-Location of SCM+FSA ;
cluster Directed a1,a2 -> programmed initial halt-free ;
correctness
coherence
Directed c3,c4 is initial;
proof end;
end;

registration
let c3, c4 be good Macro-Instruction;
cluster a1 ';' a2 -> good ;
coherence
c3 ';' c4 is good
proof end;
end;

Lemma25: for b1 being Instruction-Location of SCM+FSA holds
( dom ((insloc 0) .--> (goto b1)) = {(insloc 0)} & insloc 0 in dom ((insloc 0) .--> (goto b1)) & ((insloc 0) .--> (goto b1)) . (insloc 0) = goto b1 & card ((insloc 0) .--> (goto b1)) = 1 & not halt SCM+FSA in rng ((insloc 0) .--> (goto b1)) )
proof end;

definition
let c3 be Instruction-Location of SCM+FSA ;
func Goto c1 -> good halt-free Macro-Instruction equals :: SCMFSA8A:def 2
(insloc 0) .--> (goto a1);
coherence
(insloc 0) .--> (goto c3) is good halt-free Macro-Instruction
proof end;
end;

:: deftheorem Def2 defines Goto SCMFSA8A:def 2 :
for b1 being Instruction-Location of SCM+FSA holds Goto b1 = (insloc 0) .--> (goto b1);

definition
let c3 be State of SCM+FSA ;
let c4 be initial FinPartState of SCM+FSA ;
pred c2 is_pseudo-closed_on c1 means :Def3: :: SCMFSA8A:def 3
ex b1 being Nat st
( IC ((Computation (a1 +* (a2 +* (Start-At (insloc 0))))) . b1) = insloc (card (ProgramPart a2)) & ( for b2 being Nat st b2 < b1 holds
IC ((Computation (a1 +* (a2 +* (Start-At (insloc 0))))) . b2) in dom a2 ) );
end;

:: deftheorem Def3 defines is_pseudo-closed_on SCMFSA8A:def 3 :
for b1 being State of SCM+FSA
for b2 being initial FinPartState of SCM+FSA holds
( b2 is_pseudo-closed_on b1 iff ex b3 being Nat st
( IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) = insloc (card (ProgramPart b2)) & ( for b4 being Nat st b4 < b3 holds
IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) in dom b2 ) ) );

definition
let c3 be initial FinPartState of SCM+FSA ;
attr a1 is pseudo-paraclosed means :Def4: :: SCMFSA8A:def 4
for b1 being State of SCM+FSA holds a1 is_pseudo-closed_on b1;
end;

:: deftheorem Def4 defines pseudo-paraclosed SCMFSA8A:def 4 :
for b1 being initial FinPartState of SCM+FSA holds
( b1 is pseudo-paraclosed iff for b2 being State of SCM+FSA holds b1 is_pseudo-closed_on b2 );

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

definition
let c3 be State of SCM+FSA ;
let c4 be initial FinPartState of SCM+FSA ;
assume E28: c4 is_pseudo-closed_on c3 ;
func pseudo-LifeSpan c1,c2 -> Nat means :Def5: :: SCMFSA8A:def 5
( IC ((Computation (a1 +* (a2 +* (Start-At (insloc 0))))) . a3) = insloc (card (ProgramPart a2)) & ( for b1 being Nat st not IC ((Computation (a1 +* (a2 +* (Start-At (insloc 0))))) . b1) in dom a2 holds
a3 <= b1 ) );
existence
ex b1 being Nat st
( IC ((Computation (c3 +* (c4 +* (Start-At (insloc 0))))) . b1) = insloc (card (ProgramPart c4)) & ( for b2 being Nat st not IC ((Computation (c3 +* (c4 +* (Start-At (insloc 0))))) . b2) in dom c4 holds
b1 <= b2 ) )
proof end;
uniqueness
for b1, b2 being Nat st IC ((Computation (c3 +* (c4 +* (Start-At (insloc 0))))) . b1) = insloc (card (ProgramPart c4)) & ( for b3 being Nat st not IC ((Computation (c3 +* (c4 +* (Start-At (insloc 0))))) . b3) in dom c4 holds
b1 <= b3 ) & IC ((Computation (c3 +* (c4 +* (Start-At (insloc 0))))) . b2) = insloc (card (ProgramPart c4)) & ( for b3 being Nat st not IC ((Computation (c3 +* (c4 +* (Start-At (insloc 0))))) . b3) in dom c4 holds
b2 <= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines pseudo-LifeSpan SCMFSA8A:def 5 :
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 holds
( b3 = pseudo-LifeSpan b1,b2 iff ( IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) = insloc (card (ProgramPart b2)) & ( for b4 being Nat st not IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4) in dom b2 holds
b3 <= b4 ) ) );

theorem Th28: :: SCMFSA8A:28
for b1, b2 being Macro-Instruction
for b3 being set st b3 in dom b1 holds
(b1 ';' b2) . b3 = (Directed b1) . b3
proof end;

theorem Th29: :: SCMFSA8A:29
for b1 being Instruction-Location of SCM+FSA holds card (Goto b1) = 1 by Lemma25;

theorem Th30: :: SCMFSA8A:30
for b1 being programmed FinPartState of SCM+FSA
for b2 being set st b2 in dom b1 holds
( ( b1 . b2 = halt SCM+FSA implies (Directed b1) . b2 = goto (insloc (card b1)) ) & ( b1 . b2 <> halt SCM+FSA implies (Directed b1) . b2 = b1 . b2 ) )
proof end;

theorem Th31: :: SCMFSA8A:31
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 b3 < pseudo-LifeSpan b1,b2 holds
( IC ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) in dom b2 & CurInstr ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b3) <> halt SCM+FSA )
proof end;

theorem Th32: :: SCMFSA8A:32
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction st b2 is_pseudo-closed_on b1 holds
for b4 being Nat st b4 <= pseudo-LifeSpan b1,b2 holds
(Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . b4,(Computation (b1 +* ((b2 ';' b3) +* (Start-At (insloc 0))))) . b4 equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem Th33: :: SCMFSA8A:33
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA holds card (Directed b1,b2) = card b1
proof end;

theorem Th34: :: SCMFSA8A:34
for b1 being Macro-Instruction holds card (Directed b1) = card b1
proof end;

theorem Th35: :: SCMFSA8A:35
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 +* ((Directed b2) +* (Start-At (insloc 0))))) . b3 equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . b3) <> halt SCM+FSA )
proof end;

theorem Th36: :: SCMFSA8A:36
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( IC ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . ((LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1)) = insloc (card b2) & ((Computation (b1 +* (b2 +* (Start-At (insloc 0))))) . (LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . ((LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

Lemma38: for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( Directed b2 is_pseudo-closed_on b1 & pseudo-LifeSpan b1,(Directed b2) = (LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1 )
proof end;

theorem Th37: :: SCMFSA8A:37
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
Directed b2 is_pseudo-closed_on b1 by Lemma38;

theorem Th38: :: SCMFSA8A:38
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
pseudo-LifeSpan b1,(Directed b2) = (LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1 by Lemma38;

theorem Th39: :: SCMFSA8A:39
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA st b1 is halt-free holds
Directed b1,b2 = b1
proof end;

theorem Th40: :: SCMFSA8A:40
for b1 being Macro-Instruction st b1 is halt-free holds
Directed b1 = b1
proof end;

theorem Th41: :: SCMFSA8A:41
for b1, b2 being Macro-Instruction holds (Directed b1) ';' b2 = b1 ';' b2
proof end;

theorem Th42: :: SCMFSA8A:42
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( ( for b4 being Nat st b4 <= LifeSpan (b1 +* (b2 +* (Start-At (insloc 0)))) holds
( IC ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . b4) = IC ((Computation (b1 +* ((b2 ';' b3) +* (Start-At (insloc 0))))) . b4) & CurInstr ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . b4) = CurInstr ((Computation (b1 +* ((b2 ';' b3) +* (Start-At (insloc 0))))) . b4) ) ) & ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . ((LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* ((b2 ';' b3) +* (Start-At (insloc 0))))) . ((LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & IC ((Computation (b1 +* ((Directed b2) +* (Start-At (insloc 0))))) . ((LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1)) = IC ((Computation (b1 +* ((b2 ';' b3) +* (Start-At (insloc 0))))) . ((LifeSpan (b1 +* (b2 +* (Start-At (insloc 0))))) + 1)) )
proof end;

theorem Th43: :: SCMFSA8A:43
for b1 being State of SCM+FSA
for b2, b3 being Macro-Instruction st b2 is_closed_on Initialize b1 & b2 is_halting_on Initialize b1 holds
( ( for b4 being Nat st b4 <= LifeSpan (b1 +* (Initialized b2)) holds
( IC ((Computation (b1 +* (Initialized (Directed b2)))) . b4) = IC ((Computation (b1 +* (Initialized (b2 ';' b3)))) . b4) & CurInstr ((Computation (b1 +* (Initialized (Directed b2)))) . b4) = CurInstr ((Computation (b1 +* (Initialized (b2 ';' b3)))) . b4) ) ) & ((Computation (b1 +* (Initialized (Directed b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* (Initialized (b2 ';' b3)))) . ((LifeSpan (b1 +* (Initialized b2))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & IC ((Computation (b1 +* (Initialized (Directed b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 1)) = IC ((Computation (b1 +* (Initialized (b2 ';' b3)))) . ((LifeSpan (b1 +* (Initialized b2))) + 1)) )
proof end;

theorem Th44: :: SCMFSA8A:44
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on Initialize b1 & b2 is_halting_on Initialize b1 holds
for b3 being Nat st b3 <= LifeSpan (b1 +* (Initialized b2)) holds
( (Computation (b1 +* (Initialized b2))) . b3,(Computation (b1 +* (Initialized (Directed b2)))) . b3 equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation (b1 +* (Initialized (Directed b2)))) . b3) <> halt SCM+FSA )
proof end;

theorem Th45: :: SCMFSA8A:45
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on Initialize b1 & b2 is_halting_on Initialize b1 holds
( IC ((Computation (b1 +* (Initialized (Directed b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 1)) = insloc (card b2) & ((Computation (b1 +* (Initialized b2))) . (LifeSpan (b1 +* (Initialized b2)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* (Initialized (Directed b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 1)) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

Lemma46: for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on b2 & b1 is_halting_on b2 holds
( IC ((Computation (b2 +* ((b1 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (b2 +* (b1 +* (Start-At (insloc 0))))) + 1)) = insloc (card b1) & ((Computation (b2 +* (b1 +* (Start-At (insloc 0))))) . (LifeSpan (b2 +* (b1 +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b2 +* ((b1 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (b2 +* (b1 +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & b2 +* ((b1 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))) is halting & LifeSpan (b2 +* ((b1 ';' SCM+FSA-Stop ) +* (Start-At (insloc 0)))) = (LifeSpan (b2 +* (b1 +* (Start-At (insloc 0))))) + 1 & b1 ';' SCM+FSA-Stop is_closed_on b2 & b1 ';' SCM+FSA-Stop is_halting_on b2 )
proof end;

theorem Th46: :: SCMFSA8A:46
for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on b2 & b1 is_halting_on b2 holds
( b1 ';' SCM+FSA-Stop is_closed_on b2 & b1 ';' SCM+FSA-Stop is_halting_on b2 ) by Lemma46;

theorem Th47: :: SCMFSA8A:47
for b1 being Instruction-Location of SCM+FSA holds
( insloc 0 in dom (Goto b1) & (Goto b1) . (insloc 0) = goto b1 ) by Lemma25;

theorem Th48: :: SCMFSA8A:48
for b1 being with_non-empty_elements set
for b2 being non empty non void definite AMI-Struct of b1
for b3 being programmed FinPartState of b2
for b4 being set st b4 in dom b3 holds
b3 . b4 is Instruction of b2
proof end;

theorem Th49: :: SCMFSA8A:49
for b1 being programmed FinPartState of SCM+FSA
for b2 being set
for b3 being Nat st b2 in dom (ProgramPart (Relocated b1,b3)) holds
(ProgramPart (Relocated b1,b3)) . b2 = (Relocated b1,b3) . b2
proof end;

theorem Th50: :: SCMFSA8A:50
for b1 being programmed FinPartState of SCM+FSA
for b2 being Nat holds ProgramPart (Relocated (Directed b1),b2) = Directed (ProgramPart (Relocated b1,b2)),(insloc ((card b1) + b2))
proof end;

theorem Th51: :: SCMFSA8A:51
for b1, b2 being programmed FinPartState of SCM+FSA
for b3 being Instruction-Location of SCM+FSA holds Directed (b1 +* b2),b3 = (Directed b1,b3) +* (Directed b2,b3)
proof end;

theorem Th52: :: SCMFSA8A:52
for b1, b2 being Macro-Instruction holds Directed (b1 ';' b2) = b1 ';' (Directed b2)
proof end;

Lemma53: for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on Initialize b2 & b1 is_halting_on Initialize b2 holds
( IC ((Computation (b2 +* (Initialized (b1 ';' SCM+FSA-Stop )))) . ((LifeSpan (b2 +* (Initialized b1))) + 1)) = insloc (card b1) & ((Computation (b2 +* (Initialized b1))) . (LifeSpan (b2 +* (Initialized b1)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b2 +* (Initialized (b1 ';' SCM+FSA-Stop )))) . ((LifeSpan (b2 +* (Initialized b1))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & b2 +* (Initialized (b1 ';' SCM+FSA-Stop )) is halting & LifeSpan (b2 +* (Initialized (b1 ';' SCM+FSA-Stop ))) = (LifeSpan (b2 +* (Initialized b1))) + 1 )
proof end;

theorem Th53: :: SCMFSA8A:53
for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on Initialize b2 & b1 is_halting_on Initialize b2 holds
IC ((Computation (b2 +* (Initialized (b1 ';' SCM+FSA-Stop )))) . ((LifeSpan (b2 +* (Initialized b1))) + 1)) = insloc (card b1) by Lemma53;

theorem Th54: :: SCMFSA8A:54
for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on Initialize b2 & b1 is_halting_on Initialize b2 holds
((Computation (b2 +* (Initialized b1))) . (LifeSpan (b2 +* (Initialized b1)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b2 +* (Initialized (b1 ';' SCM+FSA-Stop )))) . ((LifeSpan (b2 +* (Initialized b1))) + 1)) | (Int-Locations \/ FinSeq-Locations ) by Lemma53;

theorem Th55: :: SCMFSA8A:55
for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on Initialize b2 & b1 is_halting_on Initialize b2 holds
b2 +* (Initialized (b1 ';' SCM+FSA-Stop )) is halting by Lemma53;

theorem Th56: :: SCMFSA8A:56
for b1 being Macro-Instruction
for b2 being State of SCM+FSA st b1 is_closed_on Initialize b2 & b1 is_halting_on Initialize b2 holds
LifeSpan (b2 +* (Initialized (b1 ';' SCM+FSA-Stop ))) = (LifeSpan (b2 +* (Initialized b1))) + 1 by Lemma53;

theorem Th57: :: SCMFSA8A:57
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_closed_on Initialize b1 & b2 is_halting_on Initialize b1 holds
IExec (b2 ';' SCM+FSA-Stop ),b1 = (IExec b2,b1) +* (Start-At (insloc (card b2)))
proof end;

Lemma54: for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on b3 & b1 is_halting_on b3 holds
( IC ((Computation (b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (b3 +* (b1 +* (Start-At (insloc 0))))) + 2)) = insloc (((card b1) + (card b2)) + 1) & ((Computation (b3 +* (b1 +* (Start-At (insloc 0))))) . (LifeSpan (b3 +* (b1 +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (b3 +* (b1 +* (Start-At (insloc 0))))) + 2)) | (Int-Locations \/ FinSeq-Locations ) & ( for b4 being Nat st b4 < (LifeSpan (b3 +* (b1 +* (Start-At (insloc 0))))) + 2 holds
CurInstr ((Computation (b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . b4) <> halt SCM+FSA ) & ( for b4 being Nat st b4 <= LifeSpan (b3 +* (b1 +* (Start-At (insloc 0)))) holds
IC ((Computation (b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . b4) = IC ((Computation (b3 +* (b1 +* (Start-At (insloc 0))))) . b4) ) & IC ((Computation (b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (b3 +* (b1 +* (Start-At (insloc 0))))) + 1)) = insloc (card b1) & b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))) is halting & LifeSpan (b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0)))) = (LifeSpan (b3 +* (b1 +* (Start-At (insloc 0))))) + 2 )
proof end;

theorem Th58: :: SCMFSA8A:58
for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on b3 & b1 is_halting_on b3 holds
( ((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop is_closed_on b3 & ((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop is_halting_on b3 )
proof end;

theorem Th59: :: SCMFSA8A:59
for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on b3 & b1 is_halting_on b3 holds
b3 +* ((((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))) is halting by Lemma54;

Lemma55: for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on Initialize b3 & b1 is_halting_on Initialize b3 holds
( IC ((Computation (b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )))) . ((LifeSpan (b3 +* (Initialized b1))) + 2)) = insloc (((card b1) + (card b2)) + 1) & ((Computation (b3 +* (Initialized b1))) . (LifeSpan (b3 +* (Initialized b1)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )))) . ((LifeSpan (b3 +* (Initialized b1))) + 2)) | (Int-Locations \/ FinSeq-Locations ) & ( for b4 being Nat st b4 < (LifeSpan (b3 +* (Initialized b1))) + 2 holds
CurInstr ((Computation (b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )))) . b4) <> halt SCM+FSA ) & ( for b4 being Nat st b4 <= LifeSpan (b3 +* (Initialized b1)) holds
IC ((Computation (b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )))) . b4) = IC ((Computation (b3 +* (Initialized b1))) . b4) ) & IC ((Computation (b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )))) . ((LifeSpan (b3 +* (Initialized b1))) + 1)) = insloc (card b1) & b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )) is halting & LifeSpan (b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ))) = (LifeSpan (b3 +* (Initialized b1))) + 2 )
proof end;

theorem Th60: :: SCMFSA8A:60
for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on Initialize b3 & b1 is_halting_on Initialize b3 holds
b3 +* (Initialized (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop )) is halting by Lemma55;

theorem Th61: :: SCMFSA8A:61
for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on Initialize b3 & b1 is_halting_on Initialize b3 holds
IC (IExec (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ),b3) = insloc (((card b1) + (card b2)) + 1)
proof end;

theorem Th62: :: SCMFSA8A:62
for b1, b2 being Macro-Instruction
for b3 being State of SCM+FSA st b1 is_closed_on Initialize b3 & b1 is_halting_on Initialize b3 holds
IExec (((b1 ';' (Goto (insloc ((card b2) + 1)))) ';' b2) ';' SCM+FSA-Stop ),b3 = (IExec b1,b3) +* (Start-At (insloc (((card b1) + (card b2)) + 1)))
proof end;