let s be State of SCMPDS ; :: thesis: for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st Initialize (stop (I ';' J)) c= s holds
(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT
set SA0 = Start-At 0 ,SCMPDS ;
let I be halt-free parahalting Program of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st Initialize (stop (I ';' J)) c= s holds
(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT
let J be parahalting shiftable Program of SCMPDS ; :: thesis: for k being Element of NAT st Initialize (stop (I ';' J)) c= s holds
(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT
let k be Element of NAT ; :: thesis: ( Initialize (stop (I ';' J)) c= s implies (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT )
set sIsI = (Initialize s) +* (stop I);
set RI = Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));
set pJ = stop J;
set RIJ = (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J);
set pIJ = stop (I ';' J);
set sIsIJ = (Initialize s) +* (stop (I ';' J));
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by SCMPDS_4:5;
I2: s +* (Initialize (stop (I ';' J))) = (Initialize s) +* (stop (I ';' J)) by SCMPDS_4:5;
I3: (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Initialize (stop J)) = (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J) by SCMPDS_4:5;
Initialize (stop I) c= (Initialize s) +* (stop I) by I1, FUNCT_4:26;
then B1: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by SCMPDS_4:63;
set s2 = Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 0 );
set s1 = ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) +* (Start-At ((IC ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) + (card I)),SCMPDS );
set m1 = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));
A2: Initialize I c= Initialize (stop (I ';' J)) by Th15;
assume A3: Initialize (stop (I ';' J)) c= s ; :: thesis: (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT
then A4: s = (Initialize s) +* (stop (I ';' J)) by I2, FUNCT_4:79;
A5: now
thus IC (((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) +* (Start-At ((IC ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) + (card I)),SCMPDS )) = (IC ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* ((stop J) +* (Start-At 0 ,SCMPDS )))) + (card I) by I3, FUNCT_4:121
.= (IC (((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (stop J)) +* (Start-At 0 ,SCMPDS ))) + (card I) by FUNCT_4:15
.= 0 + (card I) by FUNCT_4:121
.= IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 0 )) by A3, A4, A2, Th30, XBOOLE_1:1 ; :: thesis: for a being Int_position holds (((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) +* (Start-At ((IC ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) + (card I)),SCMPDS )) . a = (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 0 )) . a
hereby :: thesis: verum
let a be Int_position ; :: thesis: (((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) +* (Start-At ((IC ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) + (card I)),SCMPDS )) . a = (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 0 )) . a
A6: not a in dom ((stop J) +* (Start-At 0 ,SCMPDS )) by SCMPDS_4:61;
not a in dom (Start-At ((IC ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) + (card I)),SCMPDS ) by SCMPDS_4:59;
hence (((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) +* (Start-At ((IC ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))) + (card I)),SCMPDS )) . a = ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) . a by FUNCT_4:12
.= (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) . a by A6, I3, FUNCT_4:12
.= (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . a by B1, AMI_1:122
.= (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 0 )) . a by Th34, SCMPDS_4:13 ;
:: thesis: verum
end;
end;
defpred S1[ Element of NAT ] means (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),$1) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),$1)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + $1) equal_outside NAT ;
A7: stop (I ';' J) c= (Initialize s) +* (stop (I ';' J)) by FUNCT_4:26;
A8: 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 ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k;
set CRSk = (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS );
set CIJk = Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k);
set CRk1 = Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1);
set CRSk1 = (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1))) + (card I)),SCMPDS );
set CIJk1 = Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (k + 1));
assume A9: (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT ; :: thesis: S1[k + 1]
A10: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) = CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))
proof
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))) = (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))) by COMPOS_1:38;
A11: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) = (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) . (IC ((Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ))) by A9, Y, COMPOS_1:24
.= (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) . ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)) by FUNCT_4:121 ;
reconsider n = IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) as Element of NAT ;
A12: stop (I ';' J) = I ';' (stop J) by SCMPDS_4:46;
Initialize (stop J) c= (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J) by I3, FUNCT_4:26;
then A13: IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) in dom (stop J) by SCMPDS_4:def 9;
then n < card (stop J) by AFINSQ_1:70;
then n + (card I) < (card (stop J)) + (card I) by XREAL_1:8;
then n + (card I) < card (stop (I ';' J)) by A12, SCMPDS_4:45;
then A14: (IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I) in dom (stop (I ';' J)) by AFINSQ_1:70;
Y: (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) /. (IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) = (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) . (IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) by COMPOS_1:38;
stop J c= Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k by AMI_1:81, FUNCT_4:26;
hence CurInstr (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) = (stop J) . (IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) by A13, Y, GRFUNC_1:8
.= (stop (I ';' J)) . ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)) by A13, A12, SCMPDS_4:38
.= ((Initialize s) +* (stop (I ';' J))) . ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)) by A7, A14, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) by A11, AMI_1:54 ;
:: thesis: verum
end;
Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ) equal_outside NAT by A9, FUNCT_7:28;
then Exec (CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)), Exec (CurInstr (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),((Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS )) equal_outside NAT by A10, SCMPDS_4:15;
then A15: Exec (CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)),(Following (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k))) + (card I)),SCMPDS ) equal_outside NAT by Th35, I3;
T: ProgramPart ((Initialize s) +* (stop (I ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) by AMI_1:123;
Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (k + 1)) = Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) + 1) ;
then A16: Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (k + 1)) = Following (ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k)) by AMI_1:14;
A17: now
let a be Int_position ; :: thesis: ((Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1))) + (card I)),SCMPDS )) . a = (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (k + 1))) . a
S: ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) = ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) by AMI_1:123;
thus ((Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1))) + (card I)),SCMPDS )) . a = (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1)) . a by SCMPDS_3:14
.= (Following (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) . a by AMI_1:14
.= ((Following (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k))) + (card I)),SCMPDS )) . a by S, SCMPDS_3:14
.= (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (k + 1))) . a by A16, A15, T, SCMPDS_4:13 ; :: thesis: verum
end;
S: ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)) = ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) by AMI_1:123;
IC ((Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1))) + (card I)),SCMPDS )) = (IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1))) + (card I) by FUNCT_4:121
.= (IC (Following (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k))) + (card I) by AMI_1:14 ;
then IC ((Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1)) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),(k + 1))) + (card I)),SCMPDS )) = IC ((Following (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) +* (Start-At ((IC (Following (ProgramPart (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)),(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k))) + (card I)),SCMPDS )) by S, FUNCT_4:121
.= IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (k + 1))) by A16, A15, T, COMPOS_1:24 ;
hence S1[k + 1] by A17, SCMPDS_4:11; :: thesis: verum
end;
Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),0 = (Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J) by AMI_1:13;
then A18: S1[ 0 ] by A5, SCMPDS_4:11;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A18, A8);
 hence (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT ; :: thesis: verum