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 +* I holds
for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s & I ';' J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT
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 +* I holds
for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s & I ';' J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT
let I be keepInt0_1 Program of SCM+FSA; :: thesis: ( p +* I halts_on s +* I implies for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s & I ';' J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT )
assume A1: p +* I halts_on s +* I ; :: thesis: for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s & I ';' J c= p holds
for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT
set ISA0 = Initialized I;
let J be InitClosed Program of SCM+FSA; :: thesis: ( Initialized (I ';' J) c= s & I ';' J c= p implies for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT )
set sISA0 = s +* (Initialized I);
set pISA0 = p +* I;
A2: I c= p +* I by FUNCT_4:26;
A3: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
set RI = Result ((p +* I),(s +* (Initialized I)));
set pRI = p +* I;
set JSA0 = Initialized J;
set RIJ = (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J);
set pRIJ = (p +* I) +* J;
set sIJSA0 = s +* (Initialized (I ';' J));
set pIJSA0 = p +* (I ';' J);
defpred S1[ Nat] means (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),$1)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),$1))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + $1)) equal_outside NAT ;
assume Initialized (I ';' J) c= s ; :: thesis: ( not I ';' J c= p or for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT )
then A4: s = s +* (Initialized (I ';' J)) by FUNCT_4:79;
assume A5: I ';' J c= p ; :: thesis: for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT
then A6: p +* (I ';' J) = p by FUNCT_4:79;
A7: s +* (Initialized (I ';' J)) = s +* ((I ';' J) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= (s +* (I ';' J)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15 ;
then A8: s +* (Initialized (I ';' J)) = (s +* (Initialize ((intloc 0) .--> 1))) +* (I ';' J) by Th19;
then A9: I ';' J c= s by A4, FUNCT_4:26;
A10: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
set k1 = k + 1;
set CRk = Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k);
set CRSk = IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)),(card I));
set CIJk = Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k));
set CRk1 = Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1));
set CRSk1 = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA));
set CIJk1 = Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1)));
assume A11: (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)) equal_outside NAT ; :: thesis: S1[k + 1]
A12: IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))),(card I)) = CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k))))
proof
A13: J c= (p +* I) +* J by FUNCT_4:26;
A14: Initialized J c= (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) 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 +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))) = (p +* (I ';' J)) . (IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))) by PBOOLE:158;
IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k))) = IC (IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)),(card I))) by A11, COMPOS_1:24;
then A18: CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))) = (p +* (I ';' J)) . (IC (IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)),(card I)))) by A17
.= (p +* (I ';' J)) . ((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))) + (card I)) by FUNCT_4:121 ;
reconsider ii = IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),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 +* (Initialized I)))) +* (Initialized J)),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 +* (Initialized I)))) +* (Initialized J)),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 +* (Initialized I)))) +* (Initialized J)),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 +* (Initialized I)))) +* (Initialized J)),k))) by A20, PARTFUN1:def 8
.= ((p +* I) +* J) . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))) by A20, GRFUNC_1:8, A13 ;
CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))) = ((p +* I) +* J) . (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))) by PBOOLE:158;
hence IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))),(card I)) = (p +* (I ';' J)) . ((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))) + (card I)) by A22, A19, A23, GRFUNC_1:8, A24, A16
.= CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))) by A18 ;
:: thesis: verum
end;
Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)), IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)),(card I)) equal_outside NAT by A11, FUNCT_7:28;
then Exec ((CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k))))),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))), Exec ((IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))),(card I))),(IncIC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)),(card I)))) equal_outside NAT by A12, AMISTD_2:def 20;
then A25: Exec ((CurInstr ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k))))),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))), IncIC ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))),(card I)) equal_outside NAT by AMISTD_5:4;
Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1))) = Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),((((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k) + 1)) ;
then A26: Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1))) = Following ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + k)))) by EXTPRO_1:4;
A27: now
let a be Int-Location ; :: thesis: ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1)))) . a
thus ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) . a by SCMFSA_3:11
.= (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))) . a by EXTPRO_1:4
.= ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))) +* (Start-At (((IC (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))))) + (card I)),SCM+FSA))) . a by SCMFSA_3:11
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 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 +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1)))) . f
thus ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) . f by SCMFSA_3:12
.= (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))) . f by EXTPRO_1:4
.= ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))) +* (Start-At (((IC (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))))) + (card I)),SCM+FSA))) . f by SCMFSA_3:12
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1)))) . f by A26, A25, SCMFSA10:93 ; :: thesis: verum
end;
IC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA))) = (IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I) by FUNCT_4:121
.= (IC (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))))) + (card I) by EXTPRO_1:4 ;
then IC ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1))) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),(k + 1)))) + (card I)),SCM+FSA))) = IC ((Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k)))) +* (Start-At (((IC (Following (((p +* I) +* J),(Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),k))))) + (card I)),SCM+FSA))) by FUNCT_4:121
.= IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (k + 1)))) by A26, A25, COMPOS_1:24 ;
hence S1[k + 1] by A27, A28, SCMFSA10:91; :: thesis: verum
end;
A29: Initialize ((intloc 0) .--> 1) c= s by A4, A7, FUNCT_4:26;
then A30: s +* (Initialized (I ';' J)) = s +* (I ';' J) by A8, FUNCT_4:79;
A31: s +* (Initialized I) = s +* (I +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= (s +* I) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= (s +* (Initialize ((intloc 0) .--> 1))) +* I by Th19
.= s +* I by A29, FUNCT_4:79 ;
A32: Directed I c= I ';' J by SCMFSA6A:55;
then A33: Directed I c= s by A9, XBOOLE_1:1;
A34: Directed I c= p by A32, A5, XBOOLE_1:1;
A35: now
set s2 = Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0));
set s1 = ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA));
A36: Initialized J = Initialize (J +* ((intloc 0) .--> 1)) by FUNCT_4:15;
A37: (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) = Initialize ((Result ((p +* I),(s +* (Initialized I)))) +* (J +* ((intloc 0) .--> 1))) by FUNCT_4:15, A36;
thus IC (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) = (IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I) by FUNCT_4:121
.= (IC (Initialize ((Result ((p +* I),(s +* (Initialized I)))) +* (J +* ((intloc 0) .--> 1))))) + (card I) by A37
.= 0 + (card I) by FUNCT_4:121
.= IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) by A1, A4, A7, A33, A31, Th21, FUNCT_4:26, A34, A6 ; :: thesis: ( ( for a being Int-Location holds (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . a = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . f = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . f ) )
A38: DataPart (Comput (p,s,(LifeSpan ((p +* I),(s +* (Initialized I)))))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1))) by A1, A4, A7, A33, A31, Th22, FUNCT_4:26, A34;
hereby :: thesis: for f being FinSeq-Location holds (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . f = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . f
let a be Int-Location ; :: thesis: (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . b1 = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . b1
not a in dom (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA)) by SCMFSA6B:9;
then A39: (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . a = ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) . a by FUNCT_4:12;
A40: (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) . a = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((p +* I),(s +* (Initialized I)))))) . a by A1, A31, Th24, SCMFSA10:92
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . a by A4, A38, SCMFSA6A:38, A6 ;
per cases ( a <> intloc 0 or a = intloc 0 ) ;
suppose a <> intloc 0 ; :: thesis: (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . b1 = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . b1
then not a in dom (Initialized J) by SCMFSA6A:48;
hence (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . a = (Result ((p +* I),(s +* (Initialized I)))) . a by A39, FUNCT_4:12
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . a by A1, A31, A40, EXTPRO_1:23 ;
:: thesis: verum
end;
suppose A41: a = intloc 0 ; :: thesis: (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . b1 = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . b1
then a in dom (Initialized J) by SCMFSA6A:45;
hence (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . a = (Initialized J) . a by A39, FUNCT_4:14
.= 1 by A41, SCMFSA6A:46
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . a by A40, A41, Def3, A2, A3 ;
:: thesis: verum
end;
end;
end;
let f be FinSeq-Location ; :: thesis: (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . f = (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . f
A42: not f in dom (Initialized J) by SCMFSA6A:49;
not f in dom (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA)) by SCMFSA6B:10;
hence (((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) +* (Start-At (((IC ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J))) + (card I)),SCM+FSA))) . f = ((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)) . f by FUNCT_4:12
.= (Result ((p +* I),(s +* (Initialized I)))) . f by A42, FUNCT_4:12
.= (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) . f by A1, A31, EXTPRO_1:23
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((p +* I),(s +* (Initialized I)))))) . f by A1, A31, Th24, SCMFSA10:93
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + 0))) . f by A4, A38, SCMFSA6A:38, A6 ;
:: thesis: verum
end;
Comput (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)),0) = (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) by EXTPRO_1:3;
then A43: S1[ 0 ] by A35, SCMFSA10:91;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A43, A10);
 hence for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),k))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* I))) + 1) + k)) equal_outside NAT by A31, A30; :: thesis: verum