let s be State of SCM+FSA; for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being keeping_0 Program of SCM+FSA st P +* I halts_on s holds
for J being paraclosed Program of SCM+FSA st I ';' J c= P & Start-At (0,SCM+FSA) c= s holds
for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for I being keeping_0 Program of SCM+FSA st P +* I halts_on s holds
for J being paraclosed Program of SCM+FSA st I ';' J c= P & Start-At (0,SCM+FSA) c= s holds
for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))
let I be keeping_0 Program of SCM+FSA; ( P +* I halts_on s implies for J being paraclosed Program of SCM+FSA st I ';' J c= P & Start-At (0,SCM+FSA) c= s holds
for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))) )
assume A1:
P +* I halts_on s
; for J being paraclosed Program of SCM+FSA st I ';' J c= P & Start-At (0,SCM+FSA) c= s holds
for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))
set ISA0 = Start-At (0,SCM+FSA);
let J be paraclosed Program of SCM+FSA; ( I ';' J c= P & Start-At (0,SCM+FSA) c= s implies for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))) )
set sISA0 = s +* (Start-At (0,SCM+FSA));
set RI = Result ((P +* I),(s +* (Start-At (0,SCM+FSA))));
set JSA0 = Start-At (0,SCM+FSA);
set RIJ = (Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA));
set sIJSA0 = s +* (Start-At (0,SCM+FSA));
defpred S1[ Nat] means NPP ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),$1)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),$1))) + (card I)),SCM+FSA))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + $1)));
assume A2:
I ';' J c= P
; ( not Start-At (0,SCM+FSA) c= s or for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))) )
then A3:
P +* (I ';' J) = P
by FUNCT_4:104;
assume Z:
Start-At (0,SCM+FSA) c= s
; for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))
then A4:
s = s +* (Start-At (0,SCM+FSA))
by FUNCT_4:104;
A7:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
set k1 =
k + 1;
set CRk =
Comput (
((P +* I) +* J),
((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),
k);
set CRSk =
IncIC (
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)),
(card I));
set CIJk =
Comput (
(P +* (I ';' J)),
(s +* (Start-At (0,SCM+FSA))),
(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k));
set CRk1 =
Comput (
((P +* I) +* J),
((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),
(k + 1));
set CRSk1 =
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA));
set CIJk1 =
Comput (
(P +* (I ';' J)),
(s +* (Start-At (0,SCM+FSA))),
(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)));
assume A8:
NPP ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))) + (card I)),SCM+FSA))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))
;
S1[k + 1]
A9:
IncAddr (
(CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),
(card I))
= CurInstr (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))))
proof
A10:
I ';' J c= P +* (I ';' J)
by FUNCT_4:26;
Reloc (
J,
(card I))
c= I ';' J
by FUNCT_4:26;
then A11:
Reloc (
J,
(card I))
c= P +* (I ';' J)
by A10, XBOOLE_1:1;
dom (P +* (I ';' J)) = NAT
by PARTFUN1:def 4;
then A12:
(P +* (I ';' J)) /. (IC (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))) = (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))))
by PARTFUN1:def 8;
A13:
CurInstr (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))) =
(P +* (I ';' J)) . (IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)),(card I))))
by A8, A12, COMPOS_1:230
.=
(P +* (I ';' J)) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))) + (card I))
by FUNCT_4:121
;
reconsider ii =
IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)) as
Element of
NAT ;
A14:
Reloc (
J,
(card I))
= Shift (
(IncAddr (J,(card I))),
(card I))
by COMPOS_1:121;
A15:
Start-At (
0,
SCM+FSA)
c= (Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))
by FUNCT_4:26;
J c= (P +* I) +* J
by FUNCT_4:26;
then A16:
IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)) in dom J
by Def2, A15;
then A17:
IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)) in dom (IncAddr (J,(card I)))
by COMPOS_1:def 40;
then A18:
(Shift ((IncAddr (J,(card I))),(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))) + (card I)) =
(IncAddr (J,(card I))) . ii
by VALUED_1:def 12
.=
IncAddr (
(J /. ii),
(card I))
by A16, 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 A19:
ii + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I)))
by A17;
A20:
J c= (P +* I) +* J
by FUNCT_4:26;
A21:
J /. ii = J . ii
by A16, PARTFUN1:def 8;
thus IncAddr (
(CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),
(card I)) =
IncAddr (
(((P +* I) +* J) . (IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),
(card I))
by PBOOLE:158
.=
(Reloc (J,(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))) + (card I))
by A18, A14, A20, A21, A16, GRFUNC_1:8
.=
CurInstr (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))))
by A13, A11, A14, A19, GRFUNC_1:8
;
verum
end;
A22:
NPP (Exec ((IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),(card I))),(IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)),(card I))))) = NPP (IncIC ((Exec ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),(card I)))
by AMISTD_5:4;
NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))) = NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)),(card I)))
by A8;
then A23:
NPP (Exec ((CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))))),(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))))) = NPP (IncIC ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))),(card I)))
by A22, A9, AMISTD_2:def 20;
Comput (
(P +* (I ';' J)),
(s +* (Start-At (0,SCM+FSA))),
(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)))
= Comput (
(P +* (I ';' J)),
(s +* (Start-At (0,SCM+FSA))),
((((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k) + 1))
;
then A24:
Comput (
(P +* (I ';' J)),
(s +* (Start-At (0,SCM+FSA))),
(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)))
= Following (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k))))
by EXTPRO_1:4;
A25:
now let a be
Int-Location ;
((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)))) . athus ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA))) . a =
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) . a
by SCMFSA_3:11
.=
(Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))) . a
by EXTPRO_1:4
.=
((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))) +* (Start-At (((IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))))) + (card I)),SCM+FSA))) . a
by SCMFSA_3:11
.=
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)))) . a
by A24, A23, SCMFSA10:92
;
verum end;
A26:
now let f be
FinSeq-Location ;
((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)))) . fthus ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA))) . f =
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) . f
by SCMFSA_3:12
.=
(Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))) . f
by EXTPRO_1:4
.=
((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))) +* (Start-At (((IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))))) + (card I)),SCM+FSA))) . f
by SCMFSA_3:12
.=
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1)))) . f
by A24, A23, SCMFSA10:93
;
verum end;
IC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA))) =
(IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)
by FUNCT_4:121
.=
(IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))))) + (card I)
by EXTPRO_1:4
;
then IC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I)),SCM+FSA))) =
IC ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k)))) +* (Start-At (((IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),k))))) + (card I)),SCM+FSA)))
by FUNCT_4:121
.=
IC (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + (k + 1))))
by A24, A23, COMPOS_1:230
;
hence
S1[
k + 1]
by A25, A26, SCMFSA10:91;
verum
end;
A27: s +* (Start-At (0,SCM+FSA)) =
s +* (Start-At (0,SCM+FSA))
.=
s
by Z, FUNCT_4:104
;
Directed I c= I ';' J
by SCMFSA6A:55;
then A29:
Directed I c= P
by A2, XBOOLE_1:1;
A31:
now set s2 =
Comput (
(P +* (I ';' J)),
(s +* (Start-At (0,SCM+FSA))),
(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0));
set s1 =
((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA));
thus IC (((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) =
(IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)
by FUNCT_4:121
.=
0 + (card I)
by FUNCT_4:121
.=
IC (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0)))
by A1, A4, A29, Th37, A3, FUNCT_4:26
;
( ( for a being Int-Location holds (((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . a = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . f = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . f ) )A32:
DataPart (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1)))
by A1, A4, A29, Th38, FUNCT_4:26;
set o =
LifeSpan (
(P +* I),
(s +* (Start-At (0,SCM+FSA))));
hereby for f being FinSeq-Location holds (((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . f = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . f
let a be
Int-Location ;
(((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . a = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . a
Start-At (
0,
SCM+FSA)
c= Initialize J
by FUNCT_4:26;
then
dom (Start-At (0,SCM+FSA)) c= dom (Initialize J)
by RELAT_1:25;
then A34:
not
a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:132;
XX:
NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))
by Th40, A1, A27;
not
a in dom (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))
by SCMFSA_2:130;
hence (((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . a =
((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) . a
by FUNCT_4:12
.=
(Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) . a
by A34, FUNCT_4:12
.=
(Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . a
by A1, A27, EXTPRO_1:23
.=
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . a
by XX, SCMFSA10:92
.=
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . a
by A4, A32, A3, SCMFSA6A:38
;
verum
end; let f be
FinSeq-Location ;
(((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . f = (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . f
Start-At (
0,
SCM+FSA)
c= Initialize J
by FUNCT_4:26;
then
dom (Start-At (0,SCM+FSA)) c= dom (Initialize J)
by RELAT_1:25;
then A35:
not
f in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:133;
XX:
NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))
by Th40, A1, A27;
not
f in dom (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))
by SCMFSA_2:131;
hence (((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA))) . f =
((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) . f
by FUNCT_4:12
.=
(Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) . f
by A35, FUNCT_4:12
.=
(Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . f
by A1, A27, EXTPRO_1:23
.=
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . f
by XX, SCMFSA10:93
.=
(Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + 0))) . f
by A4, A32, A3, SCMFSA6A:38
;
verum end;
Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),0) = (Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))
by EXTPRO_1:3;
then A37:
S1[ 0 ]
by A31, SCMFSA10:91;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A37, A7);
hence
for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))
by A27; verum