:: Conditional branch macro instructions of SCM+FSA, Part I (preliminary)
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996 Association of Mizar Users

set A = NAT ;

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

theorem :: SCMFSA8A:1

canceled;

theorem :: SCMFSA8A:2

canceled;

theorem Th3: :: SCMFSA8A:3

for s being State of SCM+FSA holds dom (s | NAT ) = NAT

proof end;

theorem Th4: :: SCMFSA8A:4

for s being State of SCM+FSA st s is halting holds
for k being Element of NAT st LifeSpan s <= k holds
CurInstr (Computation s,k) = halt SCM+FSA

proof end;

theorem Th5: :: SCMFSA8A:5

for s being State of SCM+FSA st s is halting holds
for k being Element of NAT st LifeSpan s <= k holds
IC (Computation s,k) = IC (Computation s,(LifeSpan s))

proof end;

theorem Th6: :: SCMFSA8A:6

for s1, s2 being State of SCM+FSA holds
( s1,s2 equal_outside NAT iff ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) )

proof end;

theorem Th7: :: SCMFSA8A:7

for s being State of SCM+FSA
for I being Program of SCM+FSA holds IC (IExec I,s) = IC (Result (s +* (Initialized I)))

proof end;

theorem :: SCMFSA8A:8

for s being State of SCM+FSA
for I being Program of SCM+FSA holds (Initialize s) +* (Initialized I) = s +* (Initialized I)

proof end;

theorem Th9: :: SCMFSA8A:9

for I being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA holds I c= I +* (Start-At l)

proof end;

theorem Th10: :: SCMFSA8A:10

for s being State of SCM+FSA
for l being Instruction-Location of SCM+FSA holds DataPart s = DataPart (s +* (Start-At l))

proof end;

theorem :: SCMFSA8A:11

for s being State of SCM+FSA
for I being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA holds DataPart s = DataPart (s +* (I +* (Start-At l)))

proof end;

theorem Th12: :: SCMFSA8A:12

for s being State of SCM+FSA
for l being Instruction-Location of SCM+FSA holds dom (s | NAT ) misses dom (Start-At l)

proof end;

theorem Th13: :: SCMFSA8A:13

for s being State of SCM+FSA
for I being Program of SCM+FSA holds s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 )))

proof end;

theorem Th14: :: SCMFSA8A:14

for s being State of SCM+FSA
for I1, I2 being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA holds s +* (I1 +* (Start-At l)),s +* (I2 +* (Start-At l)) equal_outside NAT

proof end;

theorem Th16: :: SCMFSA8A:15

0 in dom (Stop SCM+FSA ) by SCMNORM:2;

theorem Th16A: :: SCMFSA8A:16

(Stop SCM+FSA ) . 0 = halt SCM+FSA by AFINSQ_1:38;

theorem Th17: :: SCMFSA8A:17

card (Stop SCM+FSA ) = 1 by SCMNORM:3;

theorem :: SCMFSA8A:18

canceled;

theorem :: SCMFSA8A:19

canceled;

theorem :: SCMFSA8A:20

canceled;

theorem :: SCMFSA8A:21

for P being preProgram of SCM+FSA
for l being Instruction-Location of SCM+FSA
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed P,l) . x = goto l ) & ( P . x <> halt SCM+FSA implies (Directed P,l) . x = P . x ) ) by FUNCT_4:111, FUNCT_4:112;

theorem Th22: :: SCMFSA8A:22

for i being Instruction of SCM+FSA
for a being Int-Location
for n being Element of NAT st i does_not_destroy a holds
IncAddr i,n does_not_destroy a

proof end;

theorem Th23: :: SCMFSA8A:23

for P being preProgram of SCM+FSA
for n being Element of NAT
for a being Int-Location st P does_not_destroy a holds
[(ProgramPart (Relocated P,n))] does_not_destroy a

proof end;

theorem Th24: :: SCMFSA8A:24

for P being good preProgram of SCM+FSA
for n being Element of NAT holds [(ProgramPart (Relocated P,n))] is good

proof end;

theorem Th25: :: SCMFSA8A:25

for I, J being preProgram of SCM+FSA
for a being Int-Location st I does_not_destroy a & J does_not_destroy a holds
I +* J does_not_destroy a

proof end;

theorem Th26: :: SCMFSA8A:26

for I, J being good preProgram of SCM+FSA holds I +* J is good

proof end;

theorem Th27: :: SCMFSA8A:27

for I being preProgram of SCM+FSA
for l being Instruction-Location of SCM+FSA
for a being Int-Location st I does_not_destroy a holds
Directed I,l does_not_destroy a

proof end;

registration

let I be good preProgram of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
cluster Directed I,l -> good ;
correctness
coherence
Directed I,l is good ;

proof end;

end;

registration

let I be good Program of SCM+FSA ;
cluster Directed I -> good ;
correctness
coherence
Directed I is good ;
;

end;

registration

let I be Program of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
cluster Directed I,l -> initial ;
correctness
coherence
Directed I,l is initial ;

proof end;

end;

registration

let I, J be good Program of SCM+FSA ;
cluster I ';' J -> good ;
coherence
I ';' J is good

proof end;

end;

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

proof end;

definition

canceled;
let l be Instruction-Location of SCM+FSA ;
func Goto l -> halt-free good Program of SCM+FSA equals :: SCMFSA8A:def 2
(insloc 0 ) .--> (goto l);
coherence
(insloc 0 ) .--> (goto l) is halt-free good Program of SCM+FSA

proof end;

end;

:: deftheorem SCMFSA8A:def 1 :

canceled;

:: deftheorem defines Goto SCMFSA8A:def 2 :

for l being Instruction-Location of SCM+FSA holds Goto l = (insloc 0 ) .--> (goto l);

definition

let s be State of SCM+FSA ;
let P be initial FinPartState of SCM+FSA ;
pred P is_pseudo-closed_on s means :Def3: :: SCMFSA8A:def 3
ex k being Element of NAT st
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st n < k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ) );

end;

:: deftheorem Def3 defines is_pseudo-closed_on SCMFSA8A:def 3 :

for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA holds
( P is_pseudo-closed_on s iff ex k being Element of NAT st
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st n < k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ) ) );

definition

let P be initial FinPartState of SCM+FSA ;
attr P is pseudo-paraclosed means :Def4: :: SCMFSA8A:def 4
for s being State of SCM+FSA holds P is_pseudo-closed_on s;

end;

:: deftheorem Def4 defines pseudo-paraclosed SCMFSA8A:def 4 :

for P being initial FinPartState of SCM+FSA holds
( P is pseudo-paraclosed iff for s being State of SCM+FSA holds P is_pseudo-closed_on s );

registration

cluster pseudo-paraclosed Element of sproduct the Object-Kind of SCM+FSA ;
existence
ex b₁ being Program of SCM+FSA st b₁ is pseudo-paraclosed

proof end;

end;

definition

let s be State of SCM+FSA ;
let P be initial FinPartState of SCM+FSA ;
assume A1: P is_pseudo-closed_on s ;
func pseudo-LifeSpan s,P -> Element of NAT means :Def5: :: SCMFSA8A:def 5
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),it) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
it <= n ) );
existence
ex b₁ being Element of NAT st
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),b₁) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
b₁ <= n ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st IC (Computation (s +* (P +* (Start-At (insloc 0 )))),b₁) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
b₁ <= n ) & IC (Computation (s +* (P +* (Start-At (insloc 0 )))),b₂) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
b₂ <= n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines pseudo-LifeSpan SCMFSA8A:def 5 :

for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for b₃ being Element of NAT holds
( b₃ = pseudo-LifeSpan s,P iff ( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),b₃) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
b₃ <= n ) ) );

theorem Th28: :: SCMFSA8A:28

for I, J being Program of SCM+FSA
for x being set st x in dom I holds
(I ';' J) . x = (Directed I) . x

proof end;

theorem :: SCMFSA8A:29

for l being Instruction-Location of SCM+FSA holds card (Goto l) = 1 by Lm1;

theorem :: SCMFSA8A:30

for P being preProgram of SCM+FSA
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed P) . x = goto (insloc (card P)) ) & ( P . x <> halt SCM+FSA implies (Directed P) . x = P . x ) ) by FUNCT_4:111, FUNCT_4:112;

theorem Th31: :: SCMFSA8A:31

for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for n being Element of NAT st n < pseudo-LifeSpan s,P holds
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P & CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA )

proof end;

theorem Th32: :: SCMFSA8A:32

for s being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s holds
for k being Element of NAT st k <= pseudo-LifeSpan s,I holds
Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k equal_outside NAT

proof end;

theorem Th33: :: SCMFSA8A:33

for I being preProgram of SCM+FSA
for l being Instruction-Location of SCM+FSA holds card (Directed I,l) = card I

proof end;

theorem :: SCMFSA8A:34

for I being Program of SCM+FSA holds card (Directed I) = card I by Th33;

theorem Th35: :: SCMFSA8A:35

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
( Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA )

proof end;

theorem Th36: :: SCMFSA8A:36

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) )

proof end;

Lm2: for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 )

proof end;

theorem :: SCMFSA8A:37

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
Directed I is_pseudo-closed_on s by Lm2;

theorem :: SCMFSA8A:38

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 by Lm2;

theorem :: SCMFSA8A:39

canceled;

theorem :: SCMFSA8A:40

canceled;

theorem Th41: :: SCMFSA8A:41

for I, J being Program of SCM+FSA holds (Directed I) ';' J = I ';' J

proof end;

theorem Th42: :: SCMFSA8A:42

for s being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k) ) ) & DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = DataPart (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) )

proof end;

theorem Th43: :: SCMFSA8A:43

for s being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
( IC (Computation (s +* (Initialized (Directed I))),k) = IC (Computation (s +* (Initialized (I ';' J))),k) & CurInstr (Computation (s +* (Initialized (Directed I))),k) = CurInstr (Computation (s +* (Initialized (I ';' J))),k) ) ) & DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = DataPart (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) & IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = IC (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) )

proof end;

theorem Th44: :: SCMFSA8A:44

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
( Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (Computation (s +* (Initialized (Directed I))),k) <> halt SCM+FSA )

proof end;

theorem Th45: :: SCMFSA8A:45

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) )

proof end;

Lm3: for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )

proof end;

theorem :: SCMFSA8A:46

for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s ) by Lm3;

theorem :: SCMFSA8A:47

for l being Instruction-Location of SCM+FSA holds
( insloc 0 in dom (Goto l) & (Goto l) . (insloc 0 ) = goto l ) by Lm1;

Lm4: for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) & s +* (Initialized (I ';' (Stop SCM+FSA ))) is halting & LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 1 )

proof end;

theorem :: SCMFSA8A:48

canceled;

theorem :: SCMFSA8A:49

canceled;

theorem :: SCMFSA8A:50

canceled;

theorem :: SCMFSA8A:51

canceled;

theorem :: SCMFSA8A:52

canceled;

theorem :: SCMFSA8A:53

for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IC (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) by Lm4;

theorem :: SCMFSA8A:54

for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) by Lm4;

theorem :: SCMFSA8A:55

for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
s +* (Initialized (I ';' (Stop SCM+FSA ))) is halting by Lm4;

theorem :: SCMFSA8A:56

for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 1 by Lm4;

theorem :: SCMFSA8A:57

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (I ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (insloc (card I)))

proof end;

Lm5: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )

proof end;

theorem :: SCMFSA8A:58

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( ((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ) is_closed_on s & ((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ) is_halting_on s )

proof end;

theorem :: SCMFSA8A:59

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting by Lm5;

Lm6: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (Initialized I))) + 2 holds
CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) = IC (Computation (s +* (Initialized I)),k) ) & IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))) is halting & LifeSpan (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 2 )

proof end;

theorem :: SCMFSA8A:60

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))) is halting by Lm6;

theorem :: SCMFSA8A:61

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IC (IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )),s) = insloc (((card I) + (card J)) + 1)

proof end;

theorem :: SCMFSA8A:62

for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 1)))

proof end;