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 COMPOS_1:116
.=
Reloc (
J,
(card I))
by RELAT_1:209
.=
Shift (
(IncAddr (J,(card I))),
(card I))
by COMPOS_1:121
;
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 COMPOS_1:def 40;
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 EXTPRO_1:4;
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 EXTPRO_1:4
.=
((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 EXTPRO_1:4
.=
((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 EXTPRO_1:4
;
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, EXTPRO_1:23
;
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, EXTPRO_1:23
.=
(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 EXTPRO_1:3;
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