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