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