:: by Noriko Asamoto

::

:: Received August 27, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

set A = NAT ;

set D = Data-Locations ;

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

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

theorem :: SCMFSA8A:7

theorem Th8: :: SCMFSA8A:8

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

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 Th9: :: SCMFSA8A:9

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

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 Th11: :: SCMFSA8A:11

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

for a being Int-Location st not I destroys a & not J destroys a holds

not I +* J destroys a

proof end;

theorem Th13: :: SCMFSA8A:13

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

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 ;

correctness

coherence

Directed (I,l) is good ;

end;
let l be Element of NAT ;

correctness

coherence

Directed (I,l) is good ;

proof end;

registration

let I be Program of SCM+FSA;

let l be Element of NAT ;

correctness

coherence

Directed (I,l) is initial ;

end;
let l be Element of NAT ;

correctness

coherence

Directed (I,l) is initial ;

proof end;

registration
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
end;

:: deftheorem defines Goto SCMFSA8A:def 1 :

for l being Element of NAT holds Goto l = 0 .--> (goto l);

for l being Element of NAT holds Goto l = 0 .--> (goto l);

registration
end;

registration

ex b_{1} being Program of SCM+FSA st

( b_{1} is halt-free & b_{1} is good )
end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free good for set ;

existence ex b

( b

proof end;

definition

let s be State of SCM+FSA;

let P be Instruction-Sequence of SCM+FSA;

let I be Program of SCM+FSA;

end;
let P be Instruction-Sequence of SCM+FSA;

let I be Program of SCM+FSA;

pred I is_pseudo-closed_on s,P means :Def2: :: SCMFSA8A:def 2

ex k being Element of NAT st

( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) );

ex k being Element of NAT st

( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) );

:: deftheorem Def2 defines is_pseudo-closed_on SCMFSA8A:def 2 :

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA holds

( I is_pseudo-closed_on s,P iff ex k being Element of NAT st

( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) );

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA holds

( I is_pseudo-closed_on s,P iff ex k being Element of NAT st

( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Element of NAT st n < k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) );

definition

canceled;

let s be State of SCM+FSA;

let P be Instruction-Sequence of SCM+FSA;

let I be Program of SCM+FSA;

assume X1: I is_pseudo-closed_on s,P ;

ex b_{1} being Element of NAT st

( IC (Comput ((P +* I),(Initialize s),b_{1})) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

b_{1} <= n ) )

for b_{1}, b_{2} being Element of NAT st IC (Comput ((P +* I),(Initialize s),b_{1})) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

b_{1} <= n ) & IC (Comput ((P +* I),(Initialize s),b_{2})) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

b_{2} <= n ) holds

b_{1} = b_{2}

end;
let s be State of SCM+FSA;

let P be Instruction-Sequence of SCM+FSA;

let I be Program of SCM+FSA;

assume X1: I is_pseudo-closed_on s,P ;

func pseudo-LifeSpan (s,P,I) -> Element of NAT means :Def4: :: SCMFSA8A:def 4

( IC (Comput ((P +* I),(Initialize s),it)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

it <= n ) );

existence ( IC (Comput ((P +* I),(Initialize s),it)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

it <= n ) );

ex b

( IC (Comput ((P +* I),(Initialize s),b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds

for b_{4} being Element of NAT holds

( b_{4} = pseudo-LifeSpan (s,P,I) iff ( IC (Comput ((P +* I),(Initialize s),b_{4})) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds

b_{4} <= n ) ) );

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds

for b

( b

b

theorem Th14: :: SCMFSA8A:14

for I, J being Program of SCM+FSA

for x being set st x in dom I holds

(I ";" J) . x = (Directed I) . x

for x being set st x in dom I holds

(I ";" J) . x = (Directed I) . x

proof end;

theorem :: SCMFSA8A:16

theorem Th17: :: SCMFSA8A:17

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being 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 +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )

for P being Instruction-Sequence of SCM+FSA

for I being 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 +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )

proof end;

theorem Th18: :: SCMFSA8A:18

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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

Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)

for P being Instruction-Sequence of SCM+FSA

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

Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)

proof end;

theorem Th21: :: SCMFSA8A:21

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

for P being Instruction-Sequence of SCM+FSA

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

( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )

proof end;

theorem Th22: :: SCMFSA8A:22

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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))) )

for P being Instruction-Sequence of SCM+FSA

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 Instruction-Sequence of SCM+FSA

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:23

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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;

for P being Instruction-Sequence of SCM+FSA

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:24

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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;

for P being Instruction-Sequence of SCM+FSA

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 Th26: :: SCMFSA8A:26

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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))) )

for P being Instruction-Sequence of SCM+FSA

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 Th27: :: SCMFSA8A:27

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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))) )

for P being Instruction-Sequence of SCM+FSA

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 Th28: :: SCMFSA8A:28

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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

( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = 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 )

for P being Instruction-Sequence of SCM+FSA

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

( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = 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 Th29: :: SCMFSA8A:29

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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))) )

for P being Instruction-Sequence of SCM+FSA

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 Instruction-Sequence 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 ";" (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:30

for I being Program of SCM+FSA

for P being Instruction-Sequence 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 ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P ) by Lm3;

for P being Instruction-Sequence 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 ";" (Stop SCM+FSA) is_closed_on s,P & I ";" (Stop SCM+FSA) is_halting_on s,P ) by Lm3;

theorem :: SCMFSA8A:31

Lm4: for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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:32

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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;

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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:33

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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;

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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:34

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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;

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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:35

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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;

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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:36

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

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))

for P being Instruction-Sequence of SCM+FSA

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 Instruction-Sequence of SCM+FSA

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:37

for P being Instruction-Sequence of SCM+FSA

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 )

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:38

for I, J being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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;

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA 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 Instruction-Sequence of SCM+FSA

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:39

for P being Instruction-Sequence of SCM+FSA

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;

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:40

for P being Instruction-Sequence of SCM+FSA

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

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:41

for P being Instruction-Sequence of SCM+FSA

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))

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;