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 B4: 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 A4: s = Initialized s by FUNCT_4:98;
assume A5: 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 A6: p +* (I ';' J) = p by FUNCT_4:98;
A10: 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 A11: (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]
A12: 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

A13: J c= (p +* I) +* J by FUNCT_4:25;
A14: Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
A15: Reloc (J,(card I)) c= I ';' J by FUNCT_4:25;
I ';' J c= p +* (I ';' J) by FUNCT_4:25;
then A16: Reloc (J,(card I)) c= p +* (I ';' J) by A15, XBOOLE_1:1;
A17: (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;
A18: 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 A11, A17, 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 ;
A19: Reloc (J,(card I)) = Shift ((IncAddr (J,(card I))),(card I)) by COMPOS_1:34;
A20: IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)) in dom J by Def1, A13, A14;
then A21: ii in dom (IncAddr (J,(card I))) by COMPOS_1:def 19;
then A22: (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 A20, COMPOS_1:def 19 ;
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 A23: (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 A21;
A24: J /. ii = J . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))) by A20, 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 A20, A13, 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 A18, A22, A19, A23, A24, A16, GRFUNC_1:2; :: thesis: verum

end;

B25: 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 A11, A12;
then A25: 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 A26: 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;

A27: now

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 A26, A25, SCMFSA_3:3 ; :: thesis: verum

end;

A28: now

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 A26, B25, 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 A26, B25, AMISTD_5:4 ;
hence S₁[k + 1] by A27, A28, SCMFSA_2:61; :: thesis: verum

end;

A31: s +* (Initialize ((intloc 0) .--> 1)) = s by B4, FUNCT_4:98;
A32: Directed I c= I ';' J by SCMFSA6A:16;
A34: Directed I c= p by A32, A5, XBOOLE_1:1;

A35: now

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 ;
A37: (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 A37, FUNCT_4:113
.= IC (Comput ((p +* (I ';' J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) by A1, A31, Th21, A34, A6, 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 ) )
A38: 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, A4, Th22, A34, 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 A39: (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;
A40: (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, A31, Th24
.= (Comput ((p +* (I ';' J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A4, A38, A6, SCMFSA6A:7 ;

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

suppose S: 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 S, SCMFSA6A:42, 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 A39, FUNCT_4:11
.= (Comput ((p +* (I ';' J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A1, A31, A40, EXTPRO_1:23 ;
:: thesis: verum

end;

suppose A41: 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 SCMFSA6A:42, TARSKI:def 2;
hence (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = 1 by A41, A39, FUNCT_4:13, SCMFSA6A:43
.= (Comput ((p +* (I ';' J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A40, A41, 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 A42: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:42, 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 A42, FUNCT_4:11
.= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by A1, A31, EXTPRO_1:23
.= (Comput ((p +* (I ';' J)),(Initialized s),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by A1, A31, Th24
.= (Comput ((p +* (I ';' J)),(Initialized s),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f by A4, A38, A6, SCMFSA6A:7 ;
:: thesis: verum

end;

Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),0) = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:2;
then A43: S₁[ 0 ] by A35, SCMFSA_2:61;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A43, A10);
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 A31; :: thesis: verum