let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st 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 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 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 )
let I be really-closed Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st 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 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 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 )
let J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st 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 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 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 )
let s be State of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P implies ( 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 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 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 ) )
A1: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= 1 + (card J) by Lm1 ;
A2: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= (card J) + 1 by Lm1 ;
A3: ((card I) + (card J)) + 1 = ((card J) + 1) + (card I) ;
A4: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
set J2 = (Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA));
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A5: I is_halting_on Initialized s,P ; :: thesis: ( 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 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 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 )
dom (Reloc ((Stop SCM+FSA),((card J) + 1))) = { (m + ((card J) + 1)) where m is Nat : m in dom (Stop SCM+FSA) } by COMPOS_1:33;
then A6: 0 + ((card J) + 1) in dom (Reloc ((Stop SCM+FSA),((card J) + 1))) by A4;
A7: dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ";" J) by SCMFSA6A:17;
A8: 0 in dom (Goto ((card J) + 1)) by Lm1;
A9: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . 0 = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . 0 by SCMFSA6A:25
.= (Directed ((Goto ((card J) + 1)) ";" J)) . 0 by A8, A7, Th7
.= ((Goto ((card J) + 1)) ";" (Directed J)) . 0 by SCMFSA6A:24
.= (Directed (Goto ((card J) + 1))) . 0 by A8, Th7
.= (Goto ((card J) + 1)) . 0 by SCMFSA6A:22
.= goto ((card J) + 1) ;
A10: ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) = (I ";" (Goto ((card J) + 1))) ";" (J ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by SCMFSA6A:25 ;
then A11: DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 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))))) + 1))) by A5, Th18;
A12: card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = (card (Goto ((card J) + 1))) + (card (J ";" (Stop SCM+FSA))) by SCMFSA6A:21
.= 1 + (card (J ";" (Stop SCM+FSA))) by Lm1 ;
then A13: 0 + 1 <= card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by NAT_1:11;
A14: card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by SCMFSA6A:21;
then (card I) + 0 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by A13, XREAL_1:6;
then A15: card I in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A16: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA))) by A14, SCMFSA6A:25
.= (card I) + (((card J) + 1) + 1) by A2, A16, SCMFSA6A:21
.= (((card I) + (card J)) + 1) + 1 ;
then ((card I) + (card J)) + 1 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by NAT_1:13;
then A17: ((card I) + (card J)) + 1 in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A18: 0 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A13, AFINSQ_1:66;
then 0 + (card I) in { (m + (card I)) where m is Nat : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) } ;
then A19: 0 + (card I) in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by COMPOS_1:33;
A20: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A21: (Stop SCM+FSA) . 0 = halt SCM+FSA ;
card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = 1 + ((card J) + (card (Stop SCM+FSA))) by A12, SCMFSA6A:21
.= (card J) + (1 + (card (Stop SCM+FSA))) ;
then (card J) + 1 < card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A20, XREAL_1:6;
then A22: (card J) + 1 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by AFINSQ_1:66;
A23: (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) /. (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)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (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)))) by PBOOLE:143;
A24: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . ((card J) + 1) = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . ((card J) + 1) by SCMFSA6A:25
.= (Reloc ((Stop SCM+FSA),((card J) + 1))) . (0 + ((card J) + 1)) by A1, A6, SCMFSA6A:40
.= IncAddr ((halt SCM+FSA),((card J) + 1)) by A4, A21, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) = { (m + (card I)) where m is Nat : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) } by COMPOS_1:33;
then A25: ((card I) + (card J)) + 1 in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by A22, A3;
A26: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = 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))) by A5, A10, Th18;
then A27: 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))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (card I) by A5, Th20, A23
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (card I) by A10, A15, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (0 + (card I)) by A19, SCMFSA6A:40
.= IncAddr ((goto ((card J) + 1)),(card I)) by A18, A9, COMPOS_1:35
.= goto (((card J) + 1) + (card I)) by SCMFSA_4:1
.= goto (((card I) + (card J)) + 1) ;
A28: now :: thesis: for f being FinSeq-Location holds (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 + 1)))) . f = (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))) . f
let f be FinSeq-Location ; :: thesis: (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 + 1)))) . f = (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))) . f
thus (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 + 1)))) . f = (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) + 1))) . f
.= (Following ((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))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))))) . f by EXTPRO_1:3
.= (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))) . f by A27, SCMFSA_2:69 ; :: thesis: verum
end;
thus 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))) = 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) + 1)))
.= IC (Following ((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))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 1 by A27, SCMFSA_2:69 ; :: thesis: ( 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 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 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 )
then A29: 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))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (((card I) + (card J)) + 1) by PBOOLE:143
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (((card I) + (card J)) + 1) by A10, A17, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (((card J) + 1) + (card I)) by A25, SCMFSA6A:40
.= IncAddr ((halt SCM+FSA),(card I)) by A22, A24, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
now :: thesis: for a being Int-Location holds (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 + 1)))) . a = (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))) . a
let a be Int-Location; :: thesis: (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 + 1)))) . a = (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))) . a
thus (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 + 1)))) . a = (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) + 1))) . a
.= (Following ((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))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))))) . a by EXTPRO_1:3
.= (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))) . a by A27, SCMFSA_2:69 ; :: thesis: verum
end;
then 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))))) + 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))) by A28, SCMFSA_M:2;
hence 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))) by A5, A11, Th20; :: thesis: ( ( for k being 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 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 )
hereby :: thesis: ( ( for k being 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 )
let k be Nat; :: thesis: ( k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 implies 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))),b1))) <> halt SCM+FSA )
assume A31: k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 ; :: thesis: 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))),b1))) <> halt SCM+FSA
per cases ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) or LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) < k ) ;
suppose A32: k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: 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))),b1))) <> halt SCM+FSA
then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A5, Th19;
hence 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 by A5, A10, A32, Th18; :: thesis: verum
end;
suppose A33: LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) < k ; :: thesis: 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))),b1))) <> halt SCM+FSA
k < ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 1 by A31;
then A34: k <= (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by NAT_1:13;
(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 <= k by A33, NAT_1:13;
hence 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 by A27, A34, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( 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 )
let k be Nat; :: thesis: ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies 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)) )
assume A35: k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: 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))
then Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) by A5, Th19;
then IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) ;
hence 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)) by A5, A10, A35, Th18; :: thesis: verum
end;
thus 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 by A5, A26, Th20; :: thesis: ( 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 )
thus A36: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by A29, EXTPRO_1:29; :: thesis: 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
for k being Nat st 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 holds
(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 <= k by A30;
hence 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 by A29, A36, EXTPRO_1:def 15; :: thesis: verum