let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds
for J being InitClosed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds
for J being InitClosed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))
let I be keepInt0_1 Program of SCM+FSA; :: thesis: ( p +* I halts_on s implies for J being InitClosed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)) )
assume A1: p +* I halts_on s ; :: thesis: for J being InitClosed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))
let J be InitClosed Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p implies for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)) )
set sISA0 = s +* (Initialize ((intloc 0) .--> 1));
set pISA0 = p +* I;
A2: I c= p +* I by FUNCT_4:25;
A3: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
set RI = Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))));
set pRI = p +* I;
set RIJ = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1));
set pRIJ = (p +* I) +* J;
set sIJSA0 = Initialized s;
set pIJSA0 = p +* (I ";" J);
defpred S₁[ Nat] means (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),$1)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),$1))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + $1));
assume A4: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( not I ";" J c= p or for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)) )
then A5: s = Initialized s by FUNCT_4:98;
assume A6: I ";" J c= p ; :: thesis: for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))
then A7: p +* (I ";" J) = p by FUNCT_4:98;
A8: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
set CRk = Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k);
set CRSk = IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)),(card I));
set CIJk = Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k));
set CRk1 = Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1));
set CRSk1 = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA));
set CIJk1 = Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)));
assume A9: (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)) ; :: thesis: S₁[k + 1]
A10: IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I)) = CurInstr ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))

proof

A11: J c= (p +* I) +* J by FUNCT_4:25;
A12: Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A13: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
I ";" J c= p +* (I ";" J) by FUNCT_4:25;
then A14: Reloc (J,(card I)) c= p +* (I ";" J) by A13, XBOOLE_1:1;
A15: (p +* (I ";" J)) /. (IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) = (p +* (I ";" J)) . (IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) by PBOOLE:143;
A16: CurInstr ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) = (p +* (I ";" J)) . ((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)) by A9, A15, FUNCT_4:113;
reconsider ii = IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)) as Element of NAT ;
A17: IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)) in dom J by Def1, A11, A12;
then A18: ii in dom (IncAddr (J,(card I))) by COMPOS_1:def 21;
then A19: (Shift ((IncAddr (J,(card I))),(card I))) . ((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)) = (IncAddr (J,(card I))) . ii by VALUED_1:def 12
.= IncAddr ((J /. ii),(card I)) by A17, COMPOS_1:def 21 ;
dom (Shift ((IncAddr (J,(card I))),(card I))) = { (il + (card I)) where il is Element of NAT : il in dom (IncAddr (J,(card I))) } by VALUED_1:def 12;
then A20: (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I))) by A18;
A21: J /. ii = J . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) by A17, PARTFUN1:def 6
.= ((p +* I) +* J) . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) by A17, A11, GRFUNC_1:2 ;
CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) = ((p +* I) +* J) . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) by PBOOLE:143;
hence IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I)) = CurInstr ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) by A16, A19, A20, A21, A14, GRFUNC_1:2; :: thesis: verum

end;

A22: Exec ((CurInstr ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) = Exec ((IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I))),(IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)),(card I)))) by A9, A10;
then A23: Exec ((CurInstr ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) = IncIC ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I)) by AMISTD_5:4;
Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1))) = Comput ((p +* (I ";" J)),(Initialized s),((((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k) + 1)) ;
then A24: Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1))) = Following ((p +* (I ";" J)),(Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) by EXTPRO_1:3;

A25: now :: thesis: for a being Int-Location holds ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . a

let a be Int-Location; :: thesis: ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . a
thus ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) . a by SCMFSA_3:3
.= (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))) . a by EXTPRO_1:3
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . a by A24, A23, SCMFSA_3:3 ; :: thesis: verum

end;

A26: now :: thesis: for f being FinSeq-Location holds ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . f

let f be FinSeq-Location ; :: thesis: ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . f
thus ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) . f by SCMFSA_3:4
.= (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))) . f by EXTPRO_1:3
.= (IncIC ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I))) . f by SCMFSA_3:4
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . f by A24, A22, AMISTD_5:4 ; :: thesis: verum

end;

IC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) = (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I) by FUNCT_4:113
.= (IC (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))))) + (card I) by EXTPRO_1:3 ;
then IC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) + (card I)),SCM+FSA))) = IC (IncIC ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))),(card I))) by FUNCT_4:113
.= IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) by A24, A22, AMISTD_5:4 ;
hence S₁[k + 1] by A25, A26, SCMFSA_2:61; :: thesis: verum

end;

A27: s +* (Initialize ((intloc 0) .--> 1)) = s by A4, FUNCT_4:98;
A28: Directed I c= I ";" J by SCMFSA6A:16;
A29: Directed I c= p by A28, A6, XBOOLE_1:1;

A30: now :: thesis: ( IC (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) = IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) & ( for a being Int-Location holds (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . f = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f ) )

set s2 = Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0));
set s1 = IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I));
reconsider RIJ1 = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* ((intloc 0) .--> 1) as State of SCM+FSA ;
A31: (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) = Initialize RIJ1 by FUNCT_4:14;
thus IC (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) = (IC ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) + (card I) by FUNCT_4:113
.= 0 + (card I) by A31, FUNCT_4:113
.= IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) by A1, A27, Th11, A29, A7, FUNCT_4:25 ; :: thesis: ( ( for a being Int-Location holds (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . f = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f ) )
A32: DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, A5, Th12, A29, FUNCT_4:25;

hereby :: thesis: for f being FinSeq-Location holds (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . f = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f

let a be Int-Location; :: thesis: (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . b₁ = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . b₁
not a in dom (Start-At (((IC ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) + (card I)),SCM+FSA)) by SCMFSA_2:102;
then A33: (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) . a by FUNCT_4:11;
A34: (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . a = (Comput ((p +* (I ";" J)),(Initialized s),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . a by A1, A27, Th14
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A5, A32, A7, SCMFSA_M:2 ;

per cases ( a <> intloc 0 or a = intloc 0 ) ;

suppose A35: a <> intloc 0 ; :: thesis: (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . b₁ = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . b₁

a <> IC by SCMFSA_2:56;
then not a in dom (Initialize ((intloc 0) .--> 1)) by A35, SCMFSA_M:11, TARSKI:def 2;
hence (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . a by A33, FUNCT_4:11
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A1, A27, A34, EXTPRO_1:23 ;
:: thesis: verum

end;

suppose A36: a = intloc 0 ; :: thesis: (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . b₁ = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . b₁

then a in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
hence (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = 1 by A36, A33, FUNCT_4:13, SCMFSA_M:12
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A34, A36, Def3, A2, A3 ;
:: thesis: verum

end;

end;

end;

let f be FinSeq-Location ; :: thesis: (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . f = (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f
( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58;
then A37: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
not f in dom (Start-At (((IC ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) + (card I)),SCM+FSA)) by SCMFSA_2:103;
hence (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . f = ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) . f by FUNCT_4:11
.= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f by A37, FUNCT_4:11
.= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by A1, A27, EXTPRO_1:23
.= (Comput ((p +* (I ";" J)),(Initialized s),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by A1, A27, Th14
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f by A5, A32, A7, SCMFSA_M:2 ;
:: thesis: verum

end;

A38: S₁[ 0 ] by A30, SCMFSA_2:61;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A38, A8);
hence for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)) by A27; :: thesis: verum