let s be State of SCM+FSA ; :: thesis: for I being keeping_0 Program of SCM+FSA st s +* I is halting holds
for J being paraclosed Program of SCM+FSA 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 SCM+FSA ; :: thesis: ( s +* I is halting implies for J being paraclosed Program of SCM+FSA 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:
s +* I is halting
; :: thesis: for J being paraclosed Program of SCM+FSA 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
let J be paraclosed Program of SCM+FSA ; :: thesis: ( (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 )
assume A2:
(I ';' J) +* (Start-At (insloc 0 )) c= s
; :: thesis: 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 ));
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 )));
A3:
s = s +* ((I ';' J) +* (Start-At (insloc 0 )))
by A2, FUNCT_4:79;
A5:
Directed I c= I ';' J
by SCMFSA6A:55;
A6:
s +* ((I ';' J) +* (Start-At (insloc 0 ))) = (s +* (I ';' J)) +* (Start-At (insloc 0 ))
by FUNCT_4:15;
then
s +* ((I ';' J) +* (Start-At (insloc 0 ))) = (s +* (Start-At (insloc 0 ))) +* (I ';' J)
by Th14;
then A7:
I ';' J c= s
by A3, FUNCT_4:26;
then A8:
Directed I c= s
by A5, XBOOLE_1:1;
A9:
Start-At (insloc 0 ) c= s
by A3, A6, FUNCT_4:26;
A10: 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 A9, FUNCT_4:79
;
A11: 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 A9, FUNCT_4:79
;
A12:
now 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)));
set s2 =
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 );
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, A3, A6, A8, A10, Th37, FUNCT_4:26
;
:: thesis: ( ( 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 ) )A13:
DataPart (Computation s,(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation s,((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1))
by A1, A3, A6, A8, A10, Th38, FUNCT_4:26;
hereby :: thesis: 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 ;
:: thesis: (((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 )) . aA14:
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 A14, FUNCT_4:12
.=
(Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . a
by A1, A10, AMI_1:122
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . a
by A1, A10, Th40, SCMFSA6A:30
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . a
by A3, A13, SCMFSA6A:38
;
:: thesis: verum
end; let f be
FinSeq-Location ;
:: thesis: (((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 )) . fA15:
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 A15, FUNCT_4:12
.=
(Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . f
by A1, A10, AMI_1:122
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . f
by A1, A10, Th40, SCMFSA6A:31
.=
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 0 )) . f
by A3, A13, SCMFSA6A:38
;
:: thesis: verum end;
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 ;
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 A16:
S1[ 0 ]
by A12, SCMFSA6A:28;
A17:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A18:
(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
;
:: thesis: 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));
A19:
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
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;
J +* (Start-At (insloc 0 )) c= (Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))
by FUNCT_4:26;
then A21:
IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),k) in dom J
by Def2;
then A22:
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 A23:
(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 A21, SCMFSA_4:24
;
ProgramPart (Relocated J,(card I)) c= I ';' J
by FUNCT_4:26;
then A24:
ProgramPart (Relocated J,(card I)) c= s +* ((I ';' J) +* (Start-At (insloc 0 )))
by A3, A7, XBOOLE_1:1;
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 A26:
ii + (card I) in dom (Shift (IncAddr J,(card I)),(card I))
by A22;
pi J,
ii =
J . ii
by A21, 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 A21, A27, 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 A23, A24, A25, A26, GRFUNC_1:8
.=
CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + k))
by A20, AMI_1:54
;
:: thesis: 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 A18, 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 A19, SCMFSA6A:32;
then A29:
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;
A30:
now 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
;
hence 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 A28, A29, AMI_1:121
;
:: thesis: verum end;
A31:
now let a be
Int-Location ;
:: thesis: ((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 A28, A29, SCMFSA6A:30
;
:: thesis: verum end;
now let f be
FinSeq-Location ;
:: thesis: ((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 A28, A29, SCMFSA6A:31
;
:: thesis: verum end;
hence
(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))),
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + (k + 1)) equal_outside NAT
by A30, A31, SCMFSA6A:28;
:: thesis: verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A16, A17);
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 A10, A11; :: thesis: verum