let s be State of SCM+FSA; for I being keeping_0 Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I holds
for J being paraclosed Program of SCM+FSA st (I ';' J) +* (Start-At (0,SCM+FSA)) c= s holds
for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT
set SA0 = Start-At (0,SCM+FSA);
let I be keeping_0 Program of SCM+FSA; ( ProgramPart (s +* I) halts_on s +* I implies for J being paraclosed Program of SCM+FSA st (I ';' J) +* (Start-At (0,SCM+FSA)) c= s holds
for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT )
assume A1:
ProgramPart (s +* I) halts_on s +* I
; for J being paraclosed Program of SCM+FSA st (I ';' J) +* (Start-At (0,SCM+FSA)) c= s holds
for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT
set ISA0 = I +* (Start-At (0,SCM+FSA));
let J be paraclosed Program of SCM+FSA; ( (I ';' J) +* (Start-At (0,SCM+FSA)) c= s implies for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT )
set sISA0 = s +* (I +* (Start-At (0,SCM+FSA)));
set RI = Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))));
set JSA0 = J +* (Start-At (0,SCM+FSA));
set RIJ = (Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)));
set sIJSA0 = s +* ((I ';' J) +* (Start-At (0,SCM+FSA)));
defpred S1[ Nat] means (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),$1)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),$1))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + $1)) equal_outside NAT ;
assume
(I ';' J) +* (Start-At (0,SCM+FSA)) c= s
; for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT
then A2:
s = s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))
by FUNCT_4:79;
A3:
s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) = Initialize (s +* (I ';' J))
by FUNCT_4:15;
then A4:
Start-At (0,SCM+FSA) c= s
by A2, FUNCT_4:26;
s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) = (Initialize s) +* (I ';' J)
by A3, COMPOS_1:83;
then A5:
I ';' J c= s
by A2, FUNCT_4:26;
A6:
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 (
(ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),
((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),
k);
set CRSk =
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA));
set CIJk =
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k));
set CRk1 =
Comput (
(ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),
((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),
(k + 1));
set CRSk1 =
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA));
set CIJk1 =
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)));
assume A7:
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)),
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))
equal_outside NAT
;
S1[k + 1]
A8:
IncAddr (
(CurInstr ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))),
(card I))
= CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))))
proof
(Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))) =
Initialize ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* J)
by FUNCT_4:15
.=
(Initialize (Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) +* J
by COMPOS_1:83
;
then A9:
J c= Comput (
(ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),
((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),
k)
by AMI_1:81, FUNCT_4:26;
ProgramPart (Relocated (J,(card I))) c= I ';' J
by FUNCT_4:26;
then A10:
ProgramPart (Relocated (J,(card I))) c= s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))
by A2, A5, XBOOLE_1:1;
Y:
(ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))) /. (IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))) = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))) . (IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))))
by COMPOS_1:38;
A11:
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))) =
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))) . (IC ((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA))))
by A7, Y, COMPOS_1:24
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))) . ((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I))
by FUNCT_4:121
;
reconsider ii =
IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) as
Element of
NAT ;
A12:
ProgramPart (Relocated (J,(card I))) =
Reloc (
(ProgramPart J),
(card I))
by COMPOS_1:116
.=
Reloc (
J,
(card I))
by RELAT_1:209
.=
Shift (
(IncAddr (J,(card I))),
(card I))
by COMPOS_1:121
;
J +* (Start-At (0,SCM+FSA)) c= (Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))
by FUNCT_4:26;
then A13:
IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) in dom J
by Def2;
then A14:
IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) in dom (IncAddr (J,(card I)))
by COMPOS_1:def 40;
then A15:
(Shift ((IncAddr (J,(card I))),(card I))) . ((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)) =
(IncAddr (J,(card I))) . ii
by VALUED_1:def 12
.=
IncAddr (
(J /. ii),
(card I))
by A13, SCMFSA_4:24
;
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 A16:
ii + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I)))
by A14;
Y:
(ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))
by COMPOS_1:38;
J /. ii =
J . ii
by A13, PARTFUN1:def 8
.=
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))
by A13, A9, GRFUNC_1:8
;
hence IncAddr (
(CurInstr ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))),
(card I)) =
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) . ((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I))
by A15, A10, A12, Y, A16, GRFUNC_1:8
.=
CurInstr (
(ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))))
by A11, AMI_1:54
;
verum
end;
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)),
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)) equal_outside NAT
by A7, FUNCT_7:28;
then
Exec (
(CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),
Exec (
(IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))),(card I))),
((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA))))
equal_outside NAT
by A8, SCMFSA6A:32;
then A17:
Exec (
(CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))),
(Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))) +* (Start-At (((IC (Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))))) + (card I)),SCM+FSA)) equal_outside NAT
by SCMFSA_4:28;
T:
ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k)))
by AMI_1:123;
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)))
= Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
((((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k) + 1))
;
then A18:
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)))
= Following (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + k))))
by EXTPRO_1:4;
A19:
now let a be
Int-Location ;
((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)))) . aS:
ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))
by AMI_1:123;
thus ((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA))) . a =
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) . a
by SCMFSA_3:11
.=
(Following ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))) . a
by EXTPRO_1:4
.=
((Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))) +* (Start-At (((IC (Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))))) + (card I)),SCM+FSA))) . a
by S, SCMFSA_3:11
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)))) . a
by A18, A17, T, SCMFSA10:92
;
verum end;
A20:
now let f be
FinSeq-Location ;
((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)))) . fS:
ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))
by AMI_1:123;
thus ((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA))) . f =
(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) . f
by SCMFSA_3:12
.=
(Following ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))) . f
by EXTPRO_1:4
.=
((Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))) +* (Start-At (((IC (Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))))) + (card I)),SCM+FSA))) . f
by S, SCMFSA_3:12
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1)))) . f
by A18, A17, T, SCMFSA10:93
;
verum end;
S:
ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))
by AMI_1:123;
IC ((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA))) =
(IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)
by FUNCT_4:121
.=
(IC (Following ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))))) + (card I)
by EXTPRO_1:4
;
then IC ((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1))) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),(k + 1)))) + (card I)),SCM+FSA))) =
IC ((Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k)))) +* (Start-At (((IC (Following ((ProgramPart (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),k))))) + (card I)),SCM+FSA)))
by S, FUNCT_4:121
.=
IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + (k + 1))))
by A18, A17, T, COMPOS_1:24
;
hence
S1[
k + 1]
by A19, A20, SCMFSA10:91;
verum
end;
A21: s +* (I +* (Start-At (0,SCM+FSA))) =
Initialize (s +* I)
by FUNCT_4:15
.=
(Initialize s) +* I
by COMPOS_1:83
.=
s +* I
by A4, FUNCT_4:79
;
Directed I c= I ';' J
by SCMFSA6A:55;
then A22:
Directed I c= s
by A5, XBOOLE_1:1;
A23:
now set s2 =
Comput (
(ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),
(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),
(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0));
set s1 =
((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA));
thus IC (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) =
(IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)
by FUNCT_4:121
.=
(IC (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* J) +* (Start-At (0,SCM+FSA)))) + (card I)
by FUNCT_4:15
.=
0 + (card I)
by FUNCT_4:121
.=
IC (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0)))
by A1, A2, A3, A22, A21, Th37, FUNCT_4:26
;
( ( for a being Int-Location holds (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . a = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . f = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . f ) )A24:
DataPart (Comput ((ProgramPart s),s,(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1)))
by A1, A2, A3, A22, A21, Th38, FUNCT_4:26;
hereby for f being FinSeq-Location holds (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . f = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . f
let a be
Int-Location ;
(((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . a = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . aA25:
not
a in dom (J +* (Start-At (0,SCM+FSA)))
by Th12;
not
a in dom (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))
by Th9;
hence (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . a =
((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) . a
by FUNCT_4:12
.=
(Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) . a
by A25, FUNCT_4:12
.=
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . a
by A1, A21, EXTPRO_1:23
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . a
by A1, A21, Th40, SCMFSA10:92
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . a
by A2, A24, SCMFSA6A:38
;
verum
end; let f be
FinSeq-Location ;
(((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . f = (Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . fA26:
not
f in dom (J +* (Start-At (0,SCM+FSA)))
by Th13;
not
f in dom (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))
by Th10;
hence (((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) +* (Start-At (((IC ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))) + (card I)),SCM+FSA))) . f =
((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) . f
by FUNCT_4:12
.=
(Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) . f
by A26, FUNCT_4:12
.=
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . f
by A1, A21, EXTPRO_1:23
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . f
by A1, A21, Th40, SCMFSA10:93
.=
(Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 0))) . f
by A2, A24, SCMFSA6A:38
;
verum end;
A27: s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) =
Initialize (s +* (I ';' J))
by FUNCT_4:15
.=
(Initialize s) +* (I ';' J)
by COMPOS_1:83
.=
s +* (I ';' J)
by A4, FUNCT_4:79
;
Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),0) = (Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))
by EXTPRO_1:3;
then A28:
S1[ 0 ]
by A23, SCMFSA10:91;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A28, A6);
hence
for k being Element of NAT holds (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) equal_outside NAT
by A21, A27; verum