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

begin

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 ProgramPart s halts_on s holds
for k being Element of NAT st LifeSpan s <= k holds
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA

proof end;

theorem Th5: :: SCMFSA8A:5

for s being State of SCM+FSA st ProgramPart s halts_on s holds
for k being Element of NAT st LifeSpan s <= k holds
IC (Comput (ProgramPart s),s,k) = IC (Comput (ProgramPart s),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 Element of NAT holds I c= I +* (Start-At l,SCM+FSA )

proof end;

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

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

proof end;

theorem Th12: :: SCMFSA8A:12

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

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 0 ,SCM+FSA ))

proof end;

theorem Th14: :: SCMFSA8A:14

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

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 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 Element of NAT
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 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 -> halt-free good Program of SCM+FSA equals :: SCMFSA8A:def 2
0 .--> (goto l);
coherence
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 Element of NAT holds Goto l = 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 (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),k) = card (ProgramPart P) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),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 (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),k) = card (ProgramPart P) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),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 Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V61() 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 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 (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),it) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),n) in dom P holds
it <= n ) );
existence
ex b₁ being Element of NAT st
( IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),b₁) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),n) in dom P holds
b₁ <= n ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),b₁) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),n) in dom P holds
b₁ <= n ) & IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),b₂) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),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 (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),b₃) = card (ProgramPart P) & ( for n being Element of NAT st not IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),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 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 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 (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),n) in dom P & CurInstr (ProgramPart (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),n)),(Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),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
Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k, Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k equal_outside NAT

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 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 0 ,SCM+FSA ))) holds
( Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k, Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),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 (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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 0 ,SCM+FSA )))) + 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 0 ,SCM+FSA )))) + 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 0 ,SCM+FSA ))) holds
( IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k) & CurInstr (ProgramPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k) = CurInstr (ProgramPart (Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k) ) ) & DataPart (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = DataPart (Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) & IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = IC (Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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 (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) = IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k) & CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k)),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k) = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k)),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),k) ) ) & DataPart (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = DataPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) & IC (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(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
( Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k, Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k)),(Comput (ProgramPart (s +* (Initialized (Directed I)))),(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 (Comput (ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Comput (ProgramPart (s +* (Initialized (Directed I)))),(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 (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) & ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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 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 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC (Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = card I & DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) & ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) & 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 (Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = 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 (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(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
ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) 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 (card I),SCM+FSA )

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 (Comput (ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
IC (Comput (ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) ) & IC (Comput (ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I & ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) & LifeSpan (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 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 ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ) is_closed_on s & ((I ';' (Goto ((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
ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) 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 (Comput (ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Comput (ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((I ';' (Goto ((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 (ProgramPart (Comput (ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))),k)),(Comput (ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((I ';' (Goto ((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 (Comput (ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))),k) = IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k) ) & IC (Comput (ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = card I & ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))) & LifeSpan (s +* (Initialized (((I ';' (Goto ((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
ProgramPart (s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))) 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 ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )),s) = ((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 ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 1),SCM+FSA )

proof end;