let s be State of SCM+FSA ; for I being keepInt0_1 Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I holds
for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),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 keepInt0_1 Program of SCM+FSA ; ( ProgramPart (s +* I) halts_on s +* I implies for J being InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),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 InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),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 = Initialized I;
let J be InitClosed Program of SCM+FSA ; ( Initialized (I ';' J) c= s implies for k being Element of NAT holds (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),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 +* (Initialized I);
set RI = Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I));
set JSA0 = Initialized J;
set RIJ = (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J);
set sIJSA0 = s +* (Initialized (I ';' J));
defpred S1[ Nat] means (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),$1) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),$1)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + $1) equal_outside NAT ;
assume
Initialized (I ';' J) c= s
; for k being Element of NAT holds (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),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 +* (Initialized (I ';' J))
by FUNCT_4:79;
A3: s +* (Initialized (I ';' J)) =
s +* ((I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )))
by FUNCT_4:15
.=
(s +* (I ';' J)) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:15
;
then A4:
s +* (Initialized (I ';' J)) = (s +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) +* (I ';' J)
by Th19;
then A5:
I ';' J c= s
by A2, FUNCT_4:26;
A6:
for k being Element of NAT st S1[k] holds
S1[k + 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 +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),
k;
set CRSk =
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA );
set CIJk =
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k);
set CRk1 =
Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),
(k + 1);
set CRSk1 =
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA );
set CIJk1 =
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1));
assume A7:
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA ),
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k) equal_outside NAT
;
S1[k + 1]
A8:
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),
(card I) = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))
proof
(Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J) =
(Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (J +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )))
by FUNCT_4:15
.=
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* J) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:15
.=
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) +* J
by Th19
;
then A9:
J c= Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),
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 +* (Initialized (I ';' J))
by A2, A5, XBOOLE_1:1;
Y:
(ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))) /. (IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))) = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)) . (IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)))
by COMPOS_1:38;
A11:
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)) =
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)) . (IC ((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA )))
by A7, Y, COMPOS_1:24
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)) . ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I))
by FUNCT_4:121
;
reconsider ii =
IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) as
Element of
NAT ;
A12:
ProgramPart (Relocated J,(card I)) =
Reloc (ProgramPart J),
(card I)
by AMISTD_2:69
.=
Reloc J,
(card I)
by RELAT_1:209
.=
Shift (IncAddr J,(card I)),
(card I)
by AMISTD_2:75
;
Initialized J c= (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)
by FUNCT_4:26;
then A13:
IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) in dom J
by Def1;
then A14:
ii in dom (IncAddr J,(card I))
by AMISTD_2:def 15;
then A15:
(Shift (IncAddr J,(card I)),(card I)) . ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized 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 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:
(IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I) in dom (Shift (IncAddr J,(card I)),(card I))
by A14;
Y:
(ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) /. (IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) = (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) . (IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))
by COMPOS_1:38;
J /. ii =
J . (IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))
by A13, PARTFUN1:def 8
.=
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) . (IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))
by A13, A9, GRFUNC_1:8
;
hence IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),
(card I) =
(s +* (Initialized (I ';' J))) . ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I))
by A15, A10, A12, A16, Y, GRFUNC_1:8
.=
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))
by A11, AMI_1:54
;
verum
end;
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k),
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA ) equal_outside NAT
by A7, FUNCT_7:28;
then
Exec (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)),
Exec (IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(card I)),
((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA )) equal_outside NAT
by A8, SCMFSA6A:32;
then A17:
Exec (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))),
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k)),
(Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA ) equal_outside NAT
by SCMFSA_4:28;
T:
ProgramPart (s +* (Initialized (I ';' J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))
by AMI_1:123;
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1)) = Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
((((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k) + 1)
;
then A18:
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1)) = Following (ProgramPart (s +* (Initialized (I ';' J)))),
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + k))
by AMI_1:14;
A19:
now let a be
Int-Location ;
((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . a = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1))) . aS:
ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) = ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)
by AMI_1:123;
thus ((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . a =
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) . a
by SCMFSA_3:11
.=
(Following (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) . a
by AMI_1:14
.=
((Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA )) . a
by S, SCMFSA_3:11
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1))) . a
by A18, A17, T, SCMFSA10:92
;
verum end;
A20:
now let f be
FinSeq-Location ;
((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1))) . fS:
ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) = ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)
by AMI_1:123;
thus ((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . f =
(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) . f
by SCMFSA_3:12
.=
(Following (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) . f
by AMI_1:14
.=
((Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA )) . f
by S, SCMFSA_3:12
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1))) . f
by A18, A17, T, SCMFSA10:93
;
verum end;
S:
ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) = ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)
by AMI_1:123;
IC ((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) =
(IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)
by FUNCT_4:121
.=
(IC (Following (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))) + (card I)
by AMI_1:14
;
then IC ((Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) =
IC ((Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA ))
by S, FUNCT_4:121
.=
IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + (k + 1)))
by A18, A17, T, COMPOS_1:24
;
hence
S1[
k + 1]
by A19, A20, SCMFSA10:91;
verum
end;
A21:
((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ) c= s
by A2, A3, FUNCT_4:26;
then A22:
s +* (Initialized (I ';' J)) = s +* (I ';' J)
by A4, FUNCT_4:79;
A23: s +* (Initialized I) =
s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )))
by FUNCT_4:15
.=
(s +* I) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:15
.=
(s +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) +* I
by Th19
.=
s +* I
by A21, FUNCT_4:79
;
Directed I c= I ';' J
by SCMFSA6A:55;
then A24:
Directed I c= s
by A5, XBOOLE_1:1;
A25:
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
A26:
now set s2 =
Comput (ProgramPart (s +* (Initialized (I ';' J)))),
(s +* (Initialized (I ';' J))),
(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 );
set s1 =
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA );
thus IC (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) =
(IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)
by FUNCT_4:121
.=
(IC (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (J +* ((intloc 0 ) .--> 1))) +* (Start-At 0 ,SCM+FSA ))) + (card I)
by FUNCT_4:15
.=
0 + (card I)
by FUNCT_4:121
.=
IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 ))
by A1, A2, A3, A24, A23, Th21, FUNCT_4:26
;
( ( for a being Int-Location holds (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . a ) & ( for f being FinSeq-Location holds (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . f ) )A27:
DataPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) = DataPart (Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1))
by A1, A2, A3, A24, A23, Th22, FUNCT_4:26;
hereby for f being FinSeq-Location holds (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . f
let a be
Int-Location ;
(((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . b1 = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . b1
not
a in dom (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )
by SCMFSA6B:9;
then A28:
(((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a = ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) . a
by FUNCT_4:12;
A29:
(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . a =
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . a
by A1, A23, Th24, SCMFSA10:92
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . a
by A2, A27, SCMFSA6A:38
;
per cases
( a <> intloc 0 or a = intloc 0 )
;
suppose
a <> intloc 0
;
(((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . b1 = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . b1then
not
a in dom (Initialized J)
by SCMFSA6A:48;
hence (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a =
(Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . a
by A28, FUNCT_4:12
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . a
by A1, A23, A29, AMI_1:122
;
verum end; suppose A30:
a = intloc 0
;
(((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . b1 = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . b1then
a in dom (Initialized J)
by SCMFSA6A:45;
hence (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a =
(Initialized J) . a
by A28, FUNCT_4:14
.=
1
by A30, SCMFSA6A:46
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . a
by A25, A29, A30, Def3
;
verum end;
end; let f be
FinSeq-Location ;
(((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . fA31:
not
f in dom (Initialized J)
by SCMFSA6A:49;
not
f in dom (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )
by SCMFSA6B:10;
hence (((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f =
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)) . f
by FUNCT_4:12
.=
(Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . f
by A31, FUNCT_4:12
.=
(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . f
by A1, A23, AMI_1:122
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . f
by A1, A23, Th24, SCMFSA10:93
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) + 0 )) . f
by A2, A27, SCMFSA6A:38
;
verum end;
Comput (ProgramPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J))),((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)),0 = (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J)
by AMI_1:13;
then A32:
S1[ 0 ]
by A26, SCMFSA10:91;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A32, A6);
hence
for k being Element of NAT holds (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),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 A23, A22; verum