let s be State of ; for I being keeping_0 Program of st ProgramPart (s +* I) halts_on s +* I holds
for J being paraclosed Program of st (I ';' J) +* (Start-At (insloc 0 )) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
set SA0 = Start-At (insloc 0 );
let I be keeping_0 Program of ; ( ProgramPart (s +* I) halts_on s +* I implies for J being paraclosed Program of st (I ';' J) +* (Start-At (insloc 0 )) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT )
assume A1:
ProgramPart (s +* I) halts_on s +* I
; for J being paraclosed Program of st (I ';' J) +* (Start-At (insloc 0 )) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
set ISA0 = I +* (Start-At (insloc 0 ));
let J be paraclosed Program of ; ( (I ';' J) +* (Start-At (insloc 0 )) c= s implies for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT )
set sISA0 = s +* (I +* (Start-At (insloc 0 )));
set RI = Result (s +* (I +* (Start-At (insloc 0 ))));
set JSA0 = J +* (Start-At (insloc 0 ));
set RIJ = (Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )));
set sIJSA0 = s +* ((I ';' J) +* (Start-At (insloc 0 )));
defpred S1[ Element of NAT ] means (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),$1) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),$1)) + (card I))), Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + $1) equal_outside NAT ;
assume
(I ';' J) +* (Start-At (insloc 0 )) c= s
; for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
then A2:
s = s +* ((I ';' J) +* (Start-At (insloc 0 )))
by FUNCT_4:79;
A3:
s +* ((I ';' J) +* (Start-At (insloc 0 ))) = (s +* (I ';' J)) +* (Start-At (insloc 0 ))
by FUNCT_4:15;
then A4:
Start-At (insloc 0 ) c= s
by A2, FUNCT_4:26;
s +* ((I ';' J) +* (Start-At (insloc 0 ))) = (s +* (Start-At (insloc 0 ))) +* (I ';' J)
by A3, Th14;
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 =
Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),
k;
set CRSk =
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I)));
set CIJk =
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k);
set CRk1 =
Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),
(k + 1);
set CRSk1 =
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)));
set CIJk1 =
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1));
assume A7:
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))),
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k) equal_outside NAT
;
S1[k + 1]
A8:
IncAddr (CurInstr (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)),
(card I) = CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k))
proof
(Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))) =
((Result (s +* (I +* (Start-At (insloc 0 ))))) +* J) +* (Start-At (insloc 0 ))
by FUNCT_4:15
.=
((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (Start-At (insloc 0 ))) +* J
by Th14
;
then A9:
J c= Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),
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 (insloc 0 )))
by A2, A5, XBOOLE_1:1;
A11:
CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k)) =
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k)) . (IC ((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I)))))
by A7, AMI_1:121
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k)) . ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))
by AMI_1:111
;
reconsider ii =
IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) as
Element of
NAT by ORDINAL1:def 13;
A12:
ProgramPart (Relocated J,(card I)) =
IncAddr [(Shift (ProgramPart J),(card I))],
(card I)
by SCMFSA_5:2
.=
IncAddr (Shift J,(card I)),
(card I)
by AMI_1:105
.=
Shift (IncAddr J,(card I)),
(card I)
by SCMFSA_4:35
;
J +* (Start-At (insloc 0 )) c= (Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))
by FUNCT_4:26;
then A13:
IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) in dom J
by Def2;
then A14:
IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) in dom (IncAddr J,(card I))
by SCMFSA_4:def 6;
then A15:
(Shift (IncAddr J,(card I)),(card I)) . ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I)) =
(IncAddr J,(card I)) . ii
by VALUED_1:def 12
.=
IncAddr (pi 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;
pi J,
ii =
J . ii
by A13, AMI_1:def 47
.=
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) . (IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k))
by A13, A9, GRFUNC_1:8
;
hence IncAddr (CurInstr (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)),
(card I) =
(s +* ((I ';' J) +* (Start-At (insloc 0 )))) . ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))
by A15, A10, A12, A16, GRFUNC_1:8
.=
CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k))
by A11, AMI_1:54
;
verum
end;
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k),
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))) equal_outside NAT
by A7, FUNCT_7:28;
then
Exec (CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k))),
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k)),
Exec (IncAddr (CurInstr (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)),(card I)),
((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) + (card I)))) equal_outside NAT
by A8, SCMFSA6A:32;
then A17:
Exec (CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k))),
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k)),
(Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k))) + (card I))) equal_outside NAT
by SCMFSA_4:28;
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1)) = Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
((((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k) + 1)
;
then A18:
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1)) = Following (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k))
by AMI_1:14;
A19:
now let a be
Int-Location ;
((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)))) . a = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1))) . athus ((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)))) . a =
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) . a
by SCMFSA_3:11
.=
(Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) . a
by AMI_1:14
.=
((Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k))) + (card I)))) . a
by SCMFSA_3:11
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1))) . a
by A18, A17, SCMFSA6A:30
;
verum end;
A20:
now let f be
FinSeq-Location ;
((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)))) . f = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1))) . fthus ((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)))) . f =
(Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) . f
by SCMFSA_3:12
.=
(Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) . f
by AMI_1:14
.=
((Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k))) + (card I)))) . f
by SCMFSA_3:12
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1))) . f
by A18, A17, SCMFSA6A:31
;
verum end;
IC ((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)))) =
(IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)
by AMI_1:111
.=
(IC (Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k))) + (card I)
by AMI_1:14
;
then IC ((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1)) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),(k + 1))) + (card I)))) =
IC ((Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k)) +* (Start-At ((IC (Following (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k))) + (card I))))
by AMI_1:111
.=
IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1)))
by A18, A17, AMI_1:121
;
hence
S1[
k + 1]
by A19, A20, SCMFSA6A:28;
verum
end;
A21: s +* (I +* (Start-At (insloc 0 ))) =
(s +* I) +* (Start-At (insloc 0 ))
by FUNCT_4:15
.=
(s +* (Start-At (insloc 0 ))) +* I
by Th14
.=
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 =
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 );
set s1 =
((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)));
thus IC (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) =
(IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)
by AMI_1:111
.=
(IC (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* J) +* (Start-At (insloc 0 )))) + (card I)
by FUNCT_4:15
.=
insloc (0 + (card I))
by AMI_1:111
.=
IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 ))
by A1, A2, A3, A22, A21, Th37, FUNCT_4:26
;
( ( for a being Int-Location holds (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . a = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . a ) & ( for f being FinSeq-Location holds (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . f = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . f ) )A24:
DataPart (Computation s,(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation s,((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1))
by A1, A2, A3, A22, A21, Th38, FUNCT_4:26;
hereby for f being FinSeq-Location holds (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . f = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . f
let a be
Int-Location ;
(((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . a = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . aA25:
not
a in dom (J +* (Start-At (insloc 0 )))
by Th12;
not
a in dom (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))
by Th9;
hence (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . a =
((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) . a
by FUNCT_4:12
.=
(Result (s +* (I +* (Start-At (insloc 0 ))))) . a
by A25, FUNCT_4:12
.=
(Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . a
by A1, A21, AMI_1:122
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . a
by A1, A21, Th40, SCMFSA6A:30
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . a
by A2, A24, SCMFSA6A:38
;
verum
end; let f be
FinSeq-Location ;
(((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . f = (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . fA26:
not
f in dom (J +* (Start-At (insloc 0 )))
by Th13;
not
f in dom (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))
by Th10;
hence (((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) +* (Start-At ((IC ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))))) + (card I)))) . f =
((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) . f
by FUNCT_4:12
.=
(Result (s +* (I +* (Start-At (insloc 0 ))))) . f
by A26, FUNCT_4:12
.=
(Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . f
by A1, A21, AMI_1:122
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . f
by A1, A21, Th40, SCMFSA6A:31
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . f
by A2, A24, SCMFSA6A:38
;
verum end;
A27: s +* ((I ';' J) +* (Start-At (insloc 0 ))) =
(s +* (I ';' J)) +* (Start-At (insloc 0 ))
by FUNCT_4:15
.=
(s +* (Start-At (insloc 0 ))) +* (I ';' J)
by Th14
.=
s +* (I ';' J)
by A4, FUNCT_4:79
;
Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),0 = (Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))
by AMI_1:13;
then A28:
S1[ 0 ]
by A23, SCMFSA6A:28;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A28, A6);
hence
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
by A21, A27; verum