let s be State of SCM+FSA ; :: thesis: 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 (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),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 keepInt0_1 Program of SCM+FSA ; :: thesis: ( 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 (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),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 InitClosed Program of SCM+FSA st Initialized (I ';' J) c= s holds
for k being Element of NAT holds (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT
set ISA0 = Initialized I;
let J be InitClosed Program of SCM+FSA ; :: thesis: ( Initialized (I ';' J) c= s implies for k being Element of NAT holds (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT )
set sISA0 = s +* (Initialized I);
set RI = Result (s +* (Initialized I));
set JSA0 = Initialized J;
set RIJ = (Result (s +* (Initialized I))) +* (Initialized J);
set sIJSA0 = s +* (Initialized (I ';' J));
defpred S1[ Nat] means (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),$1) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),$1)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + $1) equal_outside NAT ;
assume Initialized (I ';' J) c= s ; :: thesis: for k being Element of NAT holds (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),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 +* (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 ; :: thesis: ( S1[k] implies S1[k + 1] )
set k1 = k + 1;
set CRk = Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k;
set CRSk = (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA );
set CIJk = Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k);
set CRk1 = Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1);
set CRSk1 = (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA );
set CIJk1 = Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1));
assume A7: (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k) equal_outside NAT ; :: thesis: S1[k + 1]
A8: IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(card I) = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))
proof
(Result (s +* (Initialized I))) +* (Initialized J) = (Result (s +* (Initialized I))) +* (J +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) by FUNCT_4:15
.= ((Result (s +* (Initialized I))) +* J) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15
.= ((Result (s +* (Initialized I))) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) +* J by Th19 ;
then A9: J c= Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (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 (s +* (Initialized I))) + 1) + k))) /. (IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))) = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) . (IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))) by AMI_1:150;
A11: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) . (IC ((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)),SCM+FSA ))) by A7, AMI_1:121, Y
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) . ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)) by AMI_1:111 ;
reconsider ii = IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),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 ;
Initialized J c= (Result (s +* (Initialized I))) +* (Initialized J) by FUNCT_4:26;
then A13: IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) in dom J by Def1;
then A14: ii 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 +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),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: (IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I) in dom (Shift (IncAddr J,(card I)),(card I)) by A14;
Y: (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) /. (IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) = (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) . (IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) by AMI_1:150;
pi J,ii = J . (IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) by A13, AMI_1:def 47
.= (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) . (IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) by A13, A9, GRFUNC_1:8 ;
hence IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(card I) = (s +* (Initialized (I ';' J))) . ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) + (card I)) by A15, A10, A12, A16, GRFUNC_1:8, Y
.= CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) by A11, AMI_1:54 ;
:: thesis: verum
end;
Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (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 (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)), Exec (IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(card I)),((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (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 (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)),(Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (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 (s +* (Initialized I))) + 1) + k)) by AMI_1:144;
Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1)) = Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((((LifeSpan (s +* (Initialized I))) + 1) + k) + 1) ;
then A18: Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1)) = Following (ProgramPart (s +* (Initialized (I ';' J)))),(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + k)) by AMI_1:14;
A19: now
let a be Int-Location ; :: thesis: ((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . a = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . a
S: ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J)) = ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) by AMI_1:144;
thus ((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . a = (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) . a by SCMFSA_3:11
.= (Following (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) . a by AMI_1:14
.= ((Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA )) . a by SCMFSA_3:11, S
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 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 +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . f
S: ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J)) = ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) by AMI_1:144;
thus ((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) . f by SCMFSA_3:12
.= (Following (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) . f by AMI_1:14
.= ((Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA )) . f by SCMFSA_3:12, S
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) . f by A18, A17, SCMFSA6A:31, T ; :: thesis: verum
end;
S: ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J)) = ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k) by AMI_1:144;
IC ((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) = (IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I) by AMI_1:111
.= (IC (Following (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I) by AMI_1:14 ;
then IC ((Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),(k + 1))) + (card I)),SCM+FSA )) = IC ((Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k)),(Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),k))) + (card I)),SCM+FSA )) by AMI_1:111, S
.= IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (k + 1))) by A18, A17, AMI_1:121, T ;
hence S1[k + 1] by A19, A20, SCMFSA6A:28; :: thesis: 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 (s +* (Initialized I))) + 1) + 0 );
set s1 = ((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA );
thus IC (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) = (IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I) by AMI_1:111
.= (IC (((Result (s +* (Initialized I))) +* (J +* ((intloc 0 ) .--> 1))) +* (Start-At 0 ,SCM+FSA ))) + (card I) by FUNCT_4:15
.= 0 + (card I) by AMI_1:111
.= IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) by A1, A2, A3, A24, A23, Th21, FUNCT_4:26 ; :: thesis: ( ( for a being Int-Location holds (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a ) & ( for f being FinSeq-Location holds (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f ) )
A27: DataPart (Comput (ProgramPart s),s,(LifeSpan (s +* (Initialized I)))) = DataPart (Comput (ProgramPart s),s,((LifeSpan (s +* (Initialized I))) + 1)) by A1, A2, A3, A24, A23, Th22, FUNCT_4:26;
hereby :: thesis: for f being FinSeq-Location holds (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f
let a be Int-Location ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . b1 = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . b1
not a in dom (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA ) by SCMFSA6B:9;
then A28: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a = ((Result (s +* (Initialized I))) +* (Initialized J)) . a by FUNCT_4:12;
A29: (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . a = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized I)))) . a by A1, A23, Th24, SCMFSA6A:30
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a by A2, A27, SCMFSA6A:38 ;
per cases ( a <> intloc 0 or a = intloc 0 ) ;
suppose a <> intloc 0 ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . b1 = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . b1
then not a in dom (Initialized J) by SCMFSA6A:48;
hence (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . a = (Result (s +* (Initialized I))) . a by A28, FUNCT_4:12
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . a by A1, A23, A29, AMI_1:122 ;
:: thesis: verum
end;
suppose A30: a = intloc 0 ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . b1 = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . b1
then a in dom (Initialized J) by SCMFSA6A:45;
hence (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (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 (s +* (Initialized I))) + 1) + 0 )) . a by A25, A29, A30, Def3 ;
:: thesis: verum
end;
end;
end;
let f be FinSeq-Location ; :: thesis: (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f
A31: not f in dom (Initialized J) by SCMFSA6A:49;
not f in dom (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA ) by SCMFSA6B:10;
hence (((Result (s +* (Initialized I))) +* (Initialized J)) +* (Start-At ((IC ((Result (s +* (Initialized I))) +* (Initialized J))) + (card I)),SCM+FSA )) . f = ((Result (s +* (Initialized I))) +* (Initialized J)) . f by FUNCT_4:12
.= (Result (s +* (Initialized I))) . f by A31, FUNCT_4:12
.= (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . f by A1, A23, AMI_1:122
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized I)))) . f by A1, A23, Th24, SCMFSA6A:31
.= (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + 0 )) . f by A2, A27, SCMFSA6A:38 ;
:: thesis: verum
end;
Comput (ProgramPart ((Result (s +* (Initialized I))) +* (Initialized J))),((Result (s +* (Initialized I))) +* (Initialized J)),0 = (Result (s +* (Initialized I))) +* (Initialized J) by AMI_1:13;
then A32: S1[ 0 ] by A26, SCMFSA6A:28;
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 (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (Initialized J))),((Result (s +* I)) +* (Initialized J)),k)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT by A23, A22; :: thesis: verum