let P be Instruction-Sequence of SCMPDS; :: thesis:
let I be halt-free Program of SCMPDS; :: thesis:
let J be Program of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
assume A1: I is_closed_on s,P ; :: thesis:
set G1 = Goto ((card J) + 1);
set SS = Stop SCMPDS;
set J2 = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS);
set IJ = (I ';' (Goto ((card J) + 1))) ';' J;
set pJ = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set s1 = s;
set P1 = P +* (stop I);
set s2 = s;
reconsider P2 = P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) as Instruction-Sequence of SCMPDS ;
assume A4: I is_halting_on s,P ; :: thesis:
I: Initialize s = s by MEMSTR_0:44;
set sm = Comput (P2,s,(LifeSpan ((P +* (stop I)),s)));
A5: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:27;
then A6: IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) by A1, A4, Th39;
then A7: IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) = card I by A1, A4, Th43, I;
A8: 0 in dom (Goto ((card J) + 1)) by Th33;
A9: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 = ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS))) . 0 by AFINSQ_1:27
.= (Goto ((card J) + 1)) . 0 by A8, AFINSQ_1:def 3
.= goto ((card J) + 1) by Th33 ;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by AFINSQ_1:17
.= 1 + (card J) by COMPOS_1:54 ;
then A11: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . ((card J) + 1) = (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . (0 + (card ((Goto ((card J) + 1)) ';' J)))
.= halt SCMPDS by Lm1, Lm2, AFINSQ_1:def 3 ;
A12: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS))) by AFINSQ_1:27
.= (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS))) by AFINSQ_1:17
.= 1 + (card (J ';' (Stop SCMPDS))) by COMPOS_1:54 ;
then A13: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:66;
A14: stop ((I ';' (Goto ((card J) + 1))) ';' J) = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCMPDS)
.= (I ';' ((Goto ((card J) + 1)) ';' J)) ';' (Stop SCMPDS) by AFINSQ_1:27
.= I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:27 ;
then A15: card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) by AFINSQ_1:17;
then (card I) + 0 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by XREAL_1:6;
then A16: card I in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:66;
A17: card (Stop SCMPDS) = 1 by AFINSQ_1:33;
A18: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = 1 + ((card J) + (card (Stop SCMPDS))) by A12, AFINSQ_1:17
.= (card J) + (1 + (card (Stop SCMPDS))) ;
then (card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by A17, XREAL_1:6;
then A19: (card J) + 1 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:66;
card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (((card I) + (card J)) + 1) + 1 by A15, A18, A17;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A20: ((card I) + (card J)) + 1 in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by AFINSQ_1:66;
A21: P2 /. (IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s))))) = P2 . (IC (Comput (P2,s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
A23: CurInstr (P2,(Comput (P2,s,(LifeSpan ((P +* (stop I)),s))))) = P2 . (card I) by A1, A4, A6, Th43, A21, I
.= P2 . (card I)
.= (stop ((I ';' (Goto ((card J) + 1))) ';' J)) . (card I) by A16, FUNCT_4:13
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . (0 + (card I)) by A14
.= goto ((card J) + 1) by A13, A9, AFINSQ_1:def 3 ;

A24: now

let a be Int_position ; :: thesis:
thus (Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1))) . a = (Following (P2,(Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))))) . a by EXTPRO_1:3
.= (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) . a by A23, SCMPDS_2:54 ; :: thesis:

end;

A25: P2 /. (IC (Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = P2 . (IC (Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;
thus IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) = IC (Following (P2,(Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))))) by EXTPRO_1:3
.= ICplusConst ((Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))),((card J) + 1)) by A23, SCMPDS_2:54
.= (card I) + ((card J) + 1) by A7, Th23
.= ((card I) + (card J)) + 1 ; :: thesis:
then A27: CurInstr (P2,(Comput (P2,s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = P2 . (((card I) + (card J)) + 1) by A25
.= (stop ((I ';' (Goto ((card J) + 1))) ';' J)) . (((card I) + (card J)) + 1) by A20, FUNCT_4:13
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A14
.= halt SCMPDS by A19, A11, AFINSQ_1:def 3 ;
DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput (P2,s,(LifeSpan ((P +* (stop I)),s)))) by A1, A4, A5, Th39;
hence DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) by A24, SCMPDS_4:8; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A30: k <= LifeSpan ((P +* (stop I)),s) ; :: thesis:

per cases ;

suppose A31: k < LifeSpan ((P +* (stop I)),s) ; :: thesis:

then CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) <> halt SCMPDS by A1, A4, Th42, I;
hence CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,k))) <> halt SCMPDS by A1, A4, A5, A31, Th41; :: thesis:

end;

suppose LifeSpan ((P +* (stop I)),s) <= k ; :: thesis:

then k = LifeSpan ((P +* (stop I)),s) by A30, XXREAL_0:1;
hence CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,k))) <> halt SCMPDS by A23; :: thesis:

end;

thus IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A1, A4, A6, Th43, I; :: thesis:
thus A32: P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on s by A27, EXTPRO_1:29; :: thesis:

now

let k be Element of NAT ; :: thesis:
assume CurInstr (P2,(Comput (P2,s,k))) = halt SCMPDS ; :: thesis:
then LifeSpan ((P +* (stop I)),s) < k by A28;
hence (LifeSpan ((P +* (stop I)),s)) + 1 <= k by INT_1:7; :: thesis:

end;

hence LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + 1 by A27, A32, EXTPRO_1:def 15; :: thesis: