let P be Instruction-Sequence of SCM+FSA; :: thesis: 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 )
let I, J be Program of SCM+FSA; :: thesis: 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 )
let s be State of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( 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 ) )
assume A1: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or ( 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 ) )
A2: card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= 1 + (card J) by Lm1 ;
A4: card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= (card J) + 1 by Lm1 ;
A5: ((card I) + (card J)) + 1 = ((card J) + 1) + (card I) ;
A6: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
set J2 = (Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA));
set s2 = Initialize s;
set P2 = P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA));
set s1 = Initialize s;
assume A7: I is_halting_on s,P ; :: thesis: ( 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 )
dom (Reloc ((Stop SCM+FSA),((card J) + 1))) = { (m + ((card J) + 1)) where m is Element of NAT : m in dom (Stop SCM+FSA) } by COMPOS_1:33;
then A8: 0 + ((card J) + 1) in dom (Reloc ((Stop SCM+FSA),((card J) + 1))) by A6;
A9: dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ';' J) by SCMFSA6A:17;
A10: 0 in dom (Goto ((card J) + 1)) by Lm1;
A11: ((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 A10, A9, Th28
.= ((Goto ((card J) + 1)) ';' (Directed J)) . 0 by SCMFSA6A:24
.= (Directed (Goto ((card J) + 1))) . 0 by A10, Th28
.= (Goto ((card J) + 1)) . 0 by SCMFSA6A:22
.= goto ((card J) + 1) by Lm1 ;
A12: ((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 A13: DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, A7, Th42;
A14: 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 A15: 0 + 1 <= card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) by NAT_1:11;
A16: 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 A15, XREAL_1:6;
then A17: card I in dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA)))) by AFINSQ_1:66;
A18: 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 A16, SCMFSA6A:25
.= (card I) + (((card J) + 1) + 1) by A4, A18, 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 A19: ((card I) + (card J)) + 1 in dom (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA)))) by AFINSQ_1:66;
A20: 0 in dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) by A15, AFINSQ_1:66;
then 0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) } ;
then A21: 0 + (card I) in dom (Reloc (((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))),(card I))) by COMPOS_1:33;
A22: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A23: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) = 1 + ((card J) + (card (Stop SCM+FSA))) by A14, SCMFSA6A:21
.= (card J) + (1 + (card (Stop SCM+FSA))) ;
then (card J) + 1 < card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) by A22, XREAL_1:6;
then A24: (card J) + 1 in dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) by AFINSQ_1:66;
A25: ((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 A2, A8, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),((card J) + 1)) by A6, A23, COMPOS_1:35
.= halt SCM+FSA by COMPOS_1:11 ;
dom (Reloc (((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))),(card I))) = { (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))) } by COMPOS_1:33;
then A26: ((card I) + (card J)) + 1 in dom (Reloc (((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))),(card I))) by A24, A5;
A28: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, A7, A12, Th42;
A29: CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = (P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by PBOOLE:143
.= (P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by A1, A7, A12, Th42
.= (P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) . (card I) by A1, A7, Th36
.= (I ';' ((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA)))) . (card I) by A12, A17, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))),(card I))) . (0 + (card I)) by A21, FUNCT_4:13
.= IncAddr ((goto ((card J) + 1)),(card I)) by A20, A11, COMPOS_1:35
.= goto (((card J) + 1) + (card I)) by SCMFSA_4:1
.= goto (((card I) + (card J)) + 1) ;

A30: now

let f be FinSeq-Location ; :: thesis: (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . f = (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f
thus (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . f = (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 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))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) . f by EXTPRO_1:3
.= (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f by A29, SCMFSA_2:69 ; :: thesis: verum

end;

thus IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 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))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 1 by A29, SCMFSA_2:69 ; :: thesis: ( 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 )
then A32: CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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 A12, A19, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ';' (J ';' (Stop SCM+FSA))),(card I))) . (((card J) + 1) + (card I)) by A26, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A24, A25, COMPOS_1:35
.= halt SCM+FSA by COMPOS_1:11 ;

now

let a be Int-Location ; :: thesis: (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . a = (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a
thus (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . a = (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 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))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) . a by EXTPRO_1:3
.= (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a by A29, SCMFSA_2:69 ; :: thesis: verum

end;

then DataPart (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) by A30, SCMFSA6A:7;
hence 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))) by A1, A7, A13, Th36; :: thesis: ( ( 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 )

hereby :: thesis: ( ( 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 )

let k be Element of NAT ; :: thesis: ( k < (LifeSpan ((P +* I),(Initialize s))) + 2 implies CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),b₁))) <> halt SCM+FSA )
assume A34: k < (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis: CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),b₁))) <> halt SCM+FSA

per cases ( k <= LifeSpan ((P +* I),(Initialize s)) or LifeSpan ((P +* I),(Initialize s)) < k ) ;

suppose A35: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),b₁))) <> halt SCM+FSA

then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA by A1, A7, Th35;
hence 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 by A1, A7, A12, A35, Th42; :: thesis: verum

end;

suppose A36: LifeSpan ((P +* I),(Initialize s)) < k ; :: thesis: CurInstr ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),b₁))) <> halt SCM+FSA

k < ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 by A34;
then A37: k <= (LifeSpan ((P +* I),(Initialize s))) + 1 by NAT_1:13;
(LifeSpan ((P +* I),(Initialize s))) + 1 <= k by A36, 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))),(Initialize s),k))) <> halt SCM+FSA by A29, A37, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hereby :: thesis: ( 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 )

let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* I),(Initialize s)) implies IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) )
assume A38: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k))
then Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) by A1, A7, Th35;
then IC (Comput ((P +* I),(Initialize s),k)) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) ;
hence IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A1, A7, A12, A38, Th42; :: thesis: verum

end;

thus IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I by A1, A7, A28, Th36; :: thesis: ( 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 )
thus A39: P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on Initialize s by A32, EXTPRO_1:29; :: thesis: LifeSpan ((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 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 holds
(LifeSpan ((P +* I),(Initialize s))) + 2 <= k by A33;
hence LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 by A32, A39, EXTPRO_1:def 15; :: thesis: verum