let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of
for J being parahalting shiftable Program of
for k being Nat st stop (I ';' J) c= P holds
IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of
for J being parahalting shiftable Program of
for k being Nat st stop (I ';' J) c= P holds
IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))
let I be halt-free parahalting Program of ; :: thesis: for J being parahalting shiftable Program of
for k being Nat st stop (I ';' J) c= P holds
IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))
let J be parahalting shiftable Program of ; :: thesis: for k being Nat st stop (I ';' J) c= P holds
IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))
let k be Nat; :: thesis: ( stop (I ';' J) c= P implies IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) )
set sIsI = s;
set PIPI = P +* (stop I);
set RI = Result ((P +* (stop I)),s);
set pJ = stop J;
set RIJ = Initialize (Result ((P +* (stop I)),s));
set PRIJ = (P +* (stop I)) +* (stop J);
set pIJ = stop (I ';' J);
set sIsIJ = s;
set PIPIJ = P +* (stop (I ';' J));
A1: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
stop I c= P +* (stop I) by FUNCT_4:25;
then A2: P +* (stop I) halts_on s by SCMPDS_4:def 7;
set s2 = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0));
set s1 = (Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS));
set m1 = LifeSpan ((P +* (stop I)),s);
A3: I c= stop (I ';' J) by Th1;
assume A4: stop (I ';' J) c= P ; :: thesis: IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))
A5: P +* (stop (I ';' J)) = P by A4, FUNCT_4:98;

A6: now :: thesis: ( IC ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) = IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) & ( for a being Int_position holds ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a ) )

thus IC ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) = (IC (Initialize (Result ((P +* (stop I)),s)))) + (card I) by FUNCT_4:113
.= 0 + (card I) by FUNCT_4:113
.= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) by A4, A3, Th14, A5, XBOOLE_1:1 ; :: thesis: for a being Int_position holds ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a

hereby :: thesis: verum

let a be Int_position; :: thesis: ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a
A7: not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
not a in dom (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS)) by SCMPDS_4:18;
hence ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Initialize (Result ((P +* (stop I)),s))) . a by FUNCT_4:11
.= (Result ((P +* (stop I)),s)) . a by A7, FUNCT_4:11
.= (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . a by A2, EXTPRO_1:23
.= (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a by Th18 ;
:: thesis: verum

end;

end;

defpred S₁[ Nat] means IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),$1)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + $1));
A8: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
set CRk = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k);
set PCRk = (P +* (stop I)) +* (stop J);
set CRSk = IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I));
set CIJk = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k));
set PCIJk = P +* (stop (I ';' J));
set CRk1 = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1));
set CRSk1 = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS));
set CIJk1 = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)));
assume A10: IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) ; :: thesis: S₁[k + 1]
A11: CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))

proof

A12: CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) = (P +* (stop (I ';' J))) . (IC (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)))) by A10, PBOOLE:143
.= (P +* (stop (I ';' J))) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by FUNCT_4:113 ;
reconsider n = IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)) as Nat ;
A13: stop (I ';' J) = I ';' (stop J) by AFINSQ_1:27;
A14: IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)) in dom (stop J) by A1, SCMPDS_4:def 6;
then n < card (stop J) by AFINSQ_1:66;
then n + (card I) < (card (stop J)) + (card I) by XREAL_1:6;
then n + (card I) < card (stop (I ';' J)) by A13, AFINSQ_1:17;
then A15: (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I) in dom (stop (I ';' J)) by AFINSQ_1:66;
A16: ((P +* (stop I)) +* (stop J)) /. (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = ((P +* (stop I)) +* (stop J)) . (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) by PBOOLE:143;
stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25;
hence CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = (stop J) . (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) by A14, A16, GRFUNC_1:2
.= (stop (I ';' J)) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by A14, A13, AFINSQ_1:def 3
.= CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by A12, A8, A15, GRFUNC_1:2 ;
:: thesis: verum

end;

A17: Exec ((CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) = IncIC ((Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))),(card I)) by A10, Th19, A11, FUNCT_4:25;
Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))) = Comput ((P +* (stop (I ';' J))),s,(((LifeSpan ((P +* (stop I)),s)) + k) + 1)) ;
then A18: Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))) = Following ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by EXTPRO_1:3;

A19: now :: thesis: for a being Int_position holds ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a

let a be Int_position; :: thesis: ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a
thus ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) . a by SCMPDS_3:6
.= (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))) . a by EXTPRO_1:3
.= (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a by A18, A17, SCMPDS_3:6 ; :: thesis: verum

end;

IC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I) by FUNCT_4:113
.= (IC (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))))) + (card I) by EXTPRO_1:3 ;
then IC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) = IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) by A18, A17, FUNCT_4:113;
hence S₁[k + 1] by A19, SCMPDS_4:2; :: thesis: verum

end;

A20: S₁[ 0 ] by A6, SCMPDS_4:2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A20, A9);
hence IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) ; :: thesis: verum