let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of
for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
let I, J be Program of ; :: thesis: for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
let s be 0 -started State of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P ) )
set G = Goto ((card J) + 1);
set IJ = (I ';' (Goto ((card J) + 1))) ';' J;
set J2 = I ';' ((Goto ((card J) + 1)) ';' J);
set pJ = stop (I ';' ((Goto ((card J) + 1)) ';' J));
set pI = stop I;
set P1 = P +* (stop I);
set P2 = P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
set m = LifeSpan ((P +* (stop I)),s);
set SS = Stop SCMPDS;
set s3 = Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)));
set s4 = Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)));
set P3 = P +* (stop I);
set P4 = P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
A1: Initialize s = s by MEMSTR_0:44;
A2: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:27;
A3: I c= stop I by AFINSQ_1:74;
stop I c= P +* (stop I) by FUNCT_4:25;
then A4: I c= P +* (stop I) by A3, XBOOLE_1:1;
A5: dom (stop I) c= dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by SCMPDS_5:13;
set JS = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS);
reconsider n = IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) as Nat ;
A6: card (stop I) = (card I) + 1 by COMPOS_1:55;
assume A7: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P ) )
then IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) in dom (stop I) by A1;
then n < (card I) + 1 by A6, AFINSQ_1:66;
then A8: n <= card I by INT_1:7;
A9: stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by FUNCT_4:25;
A10: 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 ;
then I c= stop (I ';' ((Goto ((card J) + 1)) ';' J)) by AFINSQ_1:74;
then I c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A9, XBOOLE_1:1;
then A11: I c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) ;
assume A12: I is_halting_on s,P ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
then A13: P +* (stop I) halts_on s by A1;
A14: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
A15: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
per cases ( IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) <> card I or IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = card I ) ;
suppose IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) <> card I ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
then n < card I by A8, XXREAL_0:1;
then A16: IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) in dom I by AFINSQ_1:66;
A17: halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A13, EXTPRO_1:def 15
.= I . (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A4, A16, A14, GRFUNC_1:2
.= (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A11, A16, GRFUNC_1:2
.= CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) by A7, A12, Th16, A15 ;
then A18: P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) halts_on s by EXTPRO_1:29;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P by A2, A1; :: thesis: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P
now :: thesis: for k being Nat holds IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
let k be Nat; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,b1)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Comput ((P +* (stop I)),s,k));
set C2k = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k));
per cases ( k <= LifeSpan ((P +* (stop I)),s) or k > LifeSpan ((P +* (stop I)),s) ) ;
suppose A19: k <= LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,b1)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A7, A1;
then IC (Comput ((P +* (stop I)),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A5;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A7, A12, A19, Th16; :: thesis: verum
end;
suppose A20: k > LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,b1)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set m2 = LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s);
A21: LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s) <= LifeSpan ((P +* (stop I)),s) by A17, A18, EXTPRO_1:def 15;
then IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s)))) by A18, A20, EXTPRO_1:25, XXREAL_0:2
.= IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s)))) by A7, A12, A21, Th16 ;
then IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop I) by A7, A1;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A5; :: thesis: verum
end;
end;
end;
hence (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P by A2, A1; :: thesis: verum
end;
suppose A22: IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = card I ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
then A23: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A7, A12, Th16;
A24: 0 in dom (Goto ((card J) + 1)) by Th10;
A25: card (Stop SCMPDS) = 1 by AFINSQ_1:34;
A26: ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS) = (Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27;
then A27: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS))) by AFINSQ_1:17
.= 1 + (card (J ';' (Stop SCMPDS))) by COMPOS_1:54
.= ((card J) + 1) + 1 by A25, AFINSQ_1:17 ;
then A28: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:66;
(card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by A27, NAT_1:13;
then A29: (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 A10, A27, AFINSQ_1:17
.= (((card I) + (card J)) + 1) + 1 ;
then A30: ((card I) + (card J)) + 1 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by NAT_1:13;
then A31: ((card I) + (card J)) + 1 in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:66;
A32: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
A33: card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) by A10, AFINSQ_1:17;
0 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) ;
then (card I) + 0 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by XREAL_1:6, A33;
then A34: card I in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:66;
A35: CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (card I) by A7, A12, A22, Th16, A32
.= (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (card I)
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . (0 + (card I)) by A10, A9, A34, GRFUNC_1:2
.= (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 by A28, AFINSQ_1:def 3
.= (Goto ((card J) + 1)) . 0 by A26, A24, AFINSQ_1:def 3
.= goto ((card J) + 1) ;
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 A36: (((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 ;
A37: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;
A38: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) = IC (Following ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)))))) by EXTPRO_1:3
.= ICplusConst ((Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)))),((card J) + 1)) by A35, SCMPDS_2:54
.= (card I) + ((card J) + 1) by A23, Th4
.= ((card I) + (card J)) + 1 ;
then A39: CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (((card I) + (card J)) + 1) by A37
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A10, A9, A31, GRFUNC_1:2
.= halt SCMPDS by A29, A36, AFINSQ_1:def 3 ;
then A40: P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) halts_on s by EXTPRO_1:29;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P by A2, A1; :: thesis: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P
now :: thesis: for k being Nat holds IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
let k be Nat; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,b1)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Comput ((P +* (stop I)),s,k));
set C2k = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k));
per cases ( k <= LifeSpan ((P +* (stop I)),s) or k > LifeSpan ((P +* (stop I)),s) ) ;
suppose A41: k <= LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,b1)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A7, A1;
then IC (Comput ((P +* (stop I)),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A5;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A7, A12, A41, Th16; :: thesis: verum
end;
suppose A42: k > LifeSpan ((P +* (stop I)),s) ; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,b1)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set m2 = LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s);
A43: LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s) <= (LifeSpan ((P +* (stop I)),s)) + 1 by A39, A40, EXTPRO_1:def 15;
k >= (LifeSpan ((P +* (stop I)),s)) + 1 by A42, INT_1:7;
then IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s)))) by A40, A43, EXTPRO_1:25, XXREAL_0:2
.= ((card I) + (card J)) + 1 by A38, A40, A43, EXTPRO_1:25 ;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A30, AFINSQ_1:66; :: thesis: verum
end;
end;
end;
hence (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P by A2, A1; :: thesis: verum
end;
end;