:: Conditional branch macro instructions of SCM+FSA, Part I (preliminary) :: 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:1 canceled; theorem :: SCMFSA8A:2 canceled; theorem :: SCMFSA8A:3 canceled; theorem :: SCMFSA8A:4 canceled; theorem :: SCMFSA8A:5 canceled; theorem :: SCMFSA8A:6 canceled; theorem :: SCMFSA8A:7 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:105, FUNCT_4:106; 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 proofend; 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 proofend; theorem Th10: :: SCMFSA8A:10 for P being good preProgram of SCM+FSA for n being Element of NAT holds Reloc (P,n) is good proofend; 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 proofend; theorem Th12: :: SCMFSA8A:12 for I, J being good preProgram of SCM+FSA holds I +* J is good proofend; 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 proofend; 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 ; proofend; 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 ; proofend; end; registration let I, J be good Program of SCM+FSA; clusterI ";" J -> good ; coherence I ";" J is good proofend; 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)) ) proofend; definition let l be Element of NAT ; func Goto l -> Program of SCM+FSA equals :: SCMFSA8A:def 1 0 .--> (goto l); coherence 0 .--> (goto l) is Program of SCM+FSA proofend; end; :: deftheorem defines Goto SCMFSA8A:def_1_:_ 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 ) proofend; end; registration 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 b1 being Program of SCM+FSA st ( b1 is halt-free & b1 is good ) proofend; end; definition let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; let I be Program of SCM+FSA; predI 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 ) ); end; :: 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 ) ) ); registration cluster with_explicit_jumps IC-relocable sequential for Element of the InstructionsF of SCM+FSA; existence ex b1 being Instruction of SCM+FSA st b1 is sequential proofend; end; 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 ; 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 ex b1 being Element of NAT st ( IC (Comput ((P +* I),(Initialize s),b1)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds b1 <= n ) ) proofend; uniqueness for b1, b2 being Element of NAT st IC (Comput ((P +* I),(Initialize s),b1)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds b1 <= n ) & IC (Comput ((P +* I),(Initialize s),b2)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds b2 <= n ) holds b1 = b2 proofend; end; :: deftheorem SCMFSA8A:def_3_:_ canceled; :: 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 b4 being Element of NAT holds ( b4 = pseudo-LifeSpan (s,P,I) iff ( IC (Comput ((P +* I),(Initialize s),b4)) = card I & ( for n being Element of NAT st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds b4 <= n ) ) ); 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 proofend; theorem :: SCMFSA8A:15 for l being Element of NAT holds card (Goto l) = 1 by Lm1; theorem :: SCMFSA8A:16 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:105, FUNCT_4:106; 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 ) proofend; 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) proofend; theorem Th19: :: SCMFSA8A:19 for I being preProgram of SCM+FSA for l being Element of NAT holds card (Directed (I,l)) = card I proofend; theorem :: SCMFSA8A:20 for I being Program of SCM+FSA holds card (Directed I) = card I by Th19; 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 ) proofend; 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))) ) proofend; 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 ) proofend; 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; 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; theorem Th25: :: SCMFSA8A:25 for I, J being Program of SCM+FSA holds (Directed I) ";" J = I ";" J proofend; 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))) ) proofend; 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))) ) proofend; 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 ) proofend; 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))) ) proofend; 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 ) proofend; 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; theorem :: SCMFSA8A:31 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 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 ) proofend; 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; 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; 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; 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; 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)) proofend; 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 ) proofend; 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 ) proofend; 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; 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 ) proofend; 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; 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 proofend; 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)) proofend;