let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being really-closed keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds
for J being really-closed 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 really-closed keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds
for J being really-closed 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 really-closed keepInt0_1 Program of SCM+FSA; :: thesis: ( p +* I halts_on s implies for J being really-closed 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 really-closed 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 really-closed 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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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: Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
I ";" J c= p +* (I ";" J) by FUNCT_4:25;
then A13: Reloc (J,(card I)) c= p +* (I ";" J) by A12, XBOOLE_1:1;
A14: (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;
A15: 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, A14, 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 ;
IC ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) = 0 by MEMSTR_0:def 11;
then IC ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))) in dom J by AFINSQ_1:65;
then A16: IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)) in dom J by AMISTD_1:21, A11;
then A17: ii in dom (IncAddr (J,(card I))) by COMPOS_1:def 21;
then A18: (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 A16, COMPOS_1:def 21 ;
dom (Shift ((IncAddr (J,(card I))),(card I))) = { (il + (card I)) where il is Nat : il in dom (IncAddr (J,(card I))) } by VALUED_1:def 12;
then A19: (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 A17;
A20: J /. ii = J . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) by A16, 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 A16, 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 A15, A18, A19, A20, A13, GRFUNC_1:2; :: thesis: verum

end;

A21: 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 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)))) = 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 A23: 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;

A24: 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 A23, A22, SCMFSA_3:3 ; :: thesis: verum

end;

A25: 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 A23, A21, 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 A23, A21, AMISTD_5:4 ;
hence S₁[k + 1] by A24, A25, SCMFSA_2:61; :: thesis: verum

end;

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

A29: 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 ;
A30: (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 A30, FUNCT_4:113
.= IC (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) by A1, A26, Th9, A28, 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 ) )
A31: 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, Th10, A28, 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 A32: (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;
A33: (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, A26, Th12
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A5, A31, A7, SCMFSA_M:2 ;

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

suppose A34: 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 A34, 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 A32, FUNCT_4:11
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A1, A26, A33, EXTPRO_1:23 ;
:: thesis: verum

end;

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₁

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 A35, A32, FUNCT_4:13, SCMFSA_M:12
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A33, A35, Def2, 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 A36: 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 A36, FUNCT_4:11
.= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by A1, A26, EXTPRO_1:23
.= (Comput ((p +* (I ";" J)),(Initialized s),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by A1, A26, Th12
.= (Comput ((p +* (I ";" J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f by A5, A31, A7, SCMFSA_M:2 ;
:: thesis: verum

end;

A37: S₁[ 0 ] by A29, SCMFSA_2:61;
for k being Nat holds S₁[k] from NAT_1:sch 2(A37, 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 A26; :: thesis: verum