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

begin

set A = NAT ;

set D = Data-Locations SCM+FSA;

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

set T = (intloc 0) .--> 1;

theorem :: SCMFSA8A:1

canceled;

theorem :: SCMFSA8A:2

canceled;

theorem :: SCMFSA8A:3

canceled;

theorem Th4: :: SCMFSA8A:4

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt SCM+FSA

proof end;

theorem Th5: :: SCMFSA8A:5

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
IC (Comput (P,s,k)) = IC (Comput (P,s,(LifeSpan (P,s))))

proof end;

theorem Th6: :: SCMFSA8A:6

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

proof end;

theorem Th7: :: SCMFSA8A:7

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA holds IC (IExec (I,P,s)) = IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))

proof end;

theorem :: SCMFSA8A:8

canceled;

theorem :: SCMFSA8A:9

canceled;

theorem Th10: :: SCMFSA8A:10

for s being State of SCM+FSA
for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,SCM+FSA)))

proof end;

theorem :: SCMFSA8A:11

canceled;

theorem :: SCMFSA8A:12

canceled;

theorem Th13: :: SCMFSA8A:13

for s being State of SCM+FSA
for I being Program of SCM+FSA holds s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s)

proof end;

theorem :: SCMFSA8A:14

for s being State of SCM+FSA
for I1, I2 being Program of SCM+FSA
for l being Element of NAT holds NPP (s +* (NPP (I1 +* (Start-At (l,SCM+FSA))))) = NPP (s +* (NPP (I2 +* (Start-At (l,SCM+FSA)))))

proof end;

theorem :: SCMFSA8A:15

canceled;

theorem :: SCMFSA8A:16

canceled;

theorem :: SCMFSA8A:17

canceled;

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 Element of NAT
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 not i destroys a holds
not IncAddr (i,n) destroys 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 not P destroys a holds
not Reloc (P,n) destroys a

proof end;

theorem Th24: :: SCMFSA8A:24

for P being good preProgram of SCM+FSA
for n being Element of NAT holds Reloc (P,n) is good

proof end;

theorem Th25: :: SCMFSA8A:25

for I, J being preProgram 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 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 Element of NAT
for a being Int-Location st not I destroys a holds
not Directed (I,l) destroys a

proof end;

registration

let I be good preProgram of SCM+FSA;
let l be Element of NAT ;
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 Element of NAT ;
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 Element of NAT holds
( dom (0 .--> (goto l)) = {0} & 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )

proof end;

definition

canceled;
let l be Element of NAT ;
func Goto l -> Program of SCM+FSA equals :: SCMFSA8A:def 2
0 .--> (goto l);
coherence
0 .--> (goto l) is Program of SCM+FSA

proof end;

end;

:: deftheorem SCMFSA8A:def 1 :
canceled;

:: deftheorem defines Goto SCMFSA8A:def 2 :
for l being Element of NAT holds Goto l = 0 .--> (goto l);

registration

let l be Element of NAT ;
cluster Goto l -> halt-free good ;
coherence
( Goto l is halt-free & Goto l is good )

proof end;

end;

registration

cluster non empty Relation-like NAT -defined the U1 of SCM+FSA -defined the Instructions of SCM+FSA -valued Function-like the Object-Kind of SCM+FSA -compatible V21() V25() initial halt-free good set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is halt-free & b₁ is good )

proof end;

end;

definition

let s be State of SCM+FSA;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
let I be initial Program of SCM+FSA;
pred I is_pseudo-closed_on s,P means :Def3: :: SCMFSA8A:def 3
ex k being Element of NAT st
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),k)) = card (ProgramPart I) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) );

end;

:: deftheorem Def3 defines is_pseudo-closed_on SCMFSA8A:def 3 :
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being initial Program of SCM+FSA holds
( I is_pseudo-closed_on s,P iff ex k being Element of NAT st
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),k)) = card (ProgramPart I) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) ) );

definition

let I be initial Program of SCM+FSA;
attr I is pseudo-paraclosed means :: SCMFSA8A:def 4
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_pseudo-closed_on s,P;

end;

:: deftheorem defines pseudo-paraclosed SCMFSA8A:def 4 :
for I being initial Program of SCM+FSA holds
( I is pseudo-paraclosed iff for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_pseudo-closed_on s,P );

registration

cluster with_explicit_jumps IC-relocable Exec-preserving sequential Element of the Instructions of SCM+FSA;
existence
ex b₁ being Instruction of SCM+FSA st b₁ is sequential

proof end;

end;

registration

let i be sequential Instruction of SCM+FSA;
cluster <%i%> -> pseudo-paraclosed ;
coherence
<%i%> is pseudo-paraclosed

proof end;

end;

registration

cluster non empty Relation-like NAT -defined the U1 of SCM+FSA -defined the Instructions of SCM+FSA -valued Function-like the Object-Kind of SCM+FSA -compatible V21() V25() initial pseudo-paraclosed set ;
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
let I be initial Program of SCM+FSA;
assume A1: I is_pseudo-closed_on s,P ;
func pseudo-LifeSpan (s,P,I) -> Element of NAT means :Def5: :: SCMFSA8A:def 5
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),it)) = card (ProgramPart I) & ( for n being Element of NAT st not IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I holds
it <= n ) );
existence
ex b₁ being Element of NAT st
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),b₁)) = card (ProgramPart I) & ( for n being Element of NAT st not IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I holds
b₁ <= n ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st IC (Comput ((P +* (ProgramPart I)),(Initialize s),b₁)) = card (ProgramPart I) & ( for n being Element of NAT st not IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I holds
b₁ <= n ) & IC (Comput ((P +* (ProgramPart I)),(Initialize s),b₂)) = card (ProgramPart I) & ( for n being Element of NAT st not IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being initial Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for b₄ being Element of NAT holds
( b₄ = pseudo-LifeSpan (s,P,I) iff ( IC (Comput ((P +* (ProgramPart I)),(Initialize s),b₄)) = card (ProgramPart I) & ( for n being Element of NAT st not IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I 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 Element of NAT 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 (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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being initial Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) <> halt SCM+FSA )

proof end;

theorem Th32: :: SCMFSA8A:32

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
NPP (Comput ((P +* I),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))

proof end;

theorem Th33: :: SCMFSA8A:33

for I being preProgram of SCM+FSA
for l being Element of NAT 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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( NPP (Comput ((P +* I),(Initialize s),k)) = NPP (Comput ((P +* (Directed I)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

proof end;

theorem Th36: :: SCMFSA8A:36

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )

proof end;

Lm2: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )

proof end;

theorem :: SCMFSA8A:37

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
Directed I is_pseudo-closed_on s,P by Lm2;

theorem :: SCMFSA8A:38

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ';' J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ';' J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ';' J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )

proof end;

theorem Th43: :: SCMFSA8A:43

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )

proof end;

theorem Th44: :: SCMFSA8A:44

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( NPP (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) = NPP (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )

proof end;

theorem Th45: :: SCMFSA8A:45

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )

proof end;

Lm3: for I being Program of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )

proof end;

theorem :: SCMFSA8A:46

for I being Program of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P ) by Lm3;

theorem :: SCMFSA8A:47

for l being Element of NAT holds
( 0 in dom (Goto l) & (Goto l) . 0 = goto l ) by Lm1;

Lm4: for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 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
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by Lm4;

theorem :: SCMFSA8A:54

for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by Lm4;

theorem :: SCMFSA8A:55

for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by Lm4;

theorem :: SCMFSA8A:56

for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by Lm4;

theorem :: SCMFSA8A:57

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((I ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))

proof end;

Lm5: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(Initialize s))) + 2 holds
CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(Initialize s)) holds
IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) ) & IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on Initialize s & LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 )

proof end;

theorem :: SCMFSA8A:58

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P )

proof end;

theorem :: SCMFSA8A:59

for I, J being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I is_closed_on s,P & I is_halting_on s,P holds
P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on Initialize s by Lm5;

Lm6: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) & ( for k being Element of NAT st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 holds
CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) ) & IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )

proof end;

theorem :: SCMFSA8A:60

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by Lm6;

theorem :: SCMFSA8A:61

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IC (IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s)) = ((card I) + (card J)) + 1

proof end;

theorem :: SCMFSA8A:62

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))

proof end;