let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 NPP ((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))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)))
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 NPP ((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))) = NPP (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 NPP ((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))) = NPP (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 NPP ((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))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)))
set ISA0 = Initialized I;
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 NPP ((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))) = NPP (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:26;
A3: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
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 = s +* (Initialize ((intloc 0) .--> 1));
set pIJSA0 = p +* (I ';' J);
defpred S₁[ Nat] means NPP ((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))) = NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + $1)));
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: ( not I ';' J c= p or for k being Element of NAT holds NPP ((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))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))) )
then A4: s = s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:103, FUNCT_4:104;
assume A5: I ';' J c= p ; :: thesis: for k being Element of NAT holds NPP ((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))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)))
then A6: p +* (I ';' J) = p by FUNCT_4:103, FUNCT_4:104;
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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)));
assume A11: NPP ((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))) = NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))

proof

A13: J c= (p +* I) +* J by FUNCT_4:26;
A14: Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
A15: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
I ';' J c= p +* (I ';' J) by FUNCT_4:26;
then A16: Reloc (J,(card I)) c= p +* (I ';' J) by A15, XBOOLE_1:1;
A17: (p +* (I ';' J)) /. (IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) = (p +* (I ';' J)) . (IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) by PBOOLE:158;
IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))) = IC (IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)),(card I))) by A11, COMPOS_1:230;
then A18: CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((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 A17, FUNCT_4:121;
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:121;
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 40;
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 40 ;
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 8
.= ((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:8 ;
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:158;
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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) by A18, A22, A19, A23, A24, A16, GRFUNC_1:8; :: thesis: verum

end;

NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))) = NPP (IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)),(card I))) by A11;
then NPP (Exec ((CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))) = NPP (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 A12, AMISTD_2:def 20;
then A25: NPP (Exec ((CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k))))) = NPP (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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1))) = Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k) + 1)) ;
then A26: Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1))) = Following ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + k)))) by EXTPRO_1:4;

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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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:11
.= (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:4
.= ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k)))) +* (Start-At (((IC (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),k))))) + (card I)),SCM+FSA))) . a by SCMFSA_3:11
.= (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . a by A26, A25, SCMFSA10:92 ; :: 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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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:12
.= (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:4
.= (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:12
.= (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) . f by A26, A25, SCMFSA10:93 ; :: 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:121
.= (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:4 ;
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:121
.= IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (k + 1)))) by A26, A25, COMPOS_1:230 ;
hence S₁[k + 1] by A27, A28, SCMFSA10:91; :: thesis: verum

end;

A29: Initialize ((intloc 0) .--> 1) c= s by A4, FUNCT_4:26;
A31: s +* (Initialize ((intloc 0) .--> 1)) = s +* (Initialize ((intloc 0) .--> 1))
.= s by A29, FUNCT_4:103, FUNCT_4:104 ;
A32: Directed I c= I ';' J by SCMFSA6A:55;
A34: Directed I c= p by A32, A5, XBOOLE_1:1;

A35: now

set s2 = Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((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));
A37: (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) = Initialize ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* ((intloc 0) .--> 1)) by FUNCT_4:15;
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:121
.= 0 + (card I) by A37, FUNCT_4:121
.= IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) by A1, A31, Th21, A34, A6, FUNCT_4:26 ; :: 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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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:26;

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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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)),(s +* (Initialize ((intloc 0) .--> 1))),(((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 SCMFSA6B:9;
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:12;
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A1, A31, Th24;
then A40: (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . a = (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . a by SCMFSA10:92
.= (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . a by A4, A38, A6, SCMFSA6A:38 ;

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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . b₁

a <> IC by SCMFSA_2:81;
then not a in dom (Initialize ((intloc 0) .--> 1)) by S, ddiS, 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:12
.= (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . b₁

then a in dom (Initialize ((intloc 0) .--> 1)) by ddiS, TARSKI:def 2;
hence (IncIC (((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))),(card I))) . a = 1 by A41, iSint, A39, FUNCT_4:14
.= (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((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)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f
( f <> intloc 0 & f <> IC ) by SCMFSA_2:82, SCMFSA_2:83;
then A42: not f in dom (Initialize ((intloc 0) .--> 1)) by ddiS, TARSKI:def 2;
XX: NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A1, A31, Th24;
not f in dom (Start-At (((IC ((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) + (card I)),SCM+FSA)) by SCMFSA6B:10;
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:12
.= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) . f by A42, FUNCT_4:12
.= (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)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by XX, SCMFSA10:93
.= (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 0))) . f by A4, A38, A6, SCMFSA6A:38 ;
:: 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:3;
then A43: S₁[ 0 ] by A35, SCMFSA10:91;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A43, A10);
hence for k being Element of NAT holds NPP ((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))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))) by A31; :: thesis: verum