let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of st I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS holds
IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
let I, J be Program of ; :: thesis: ( I c= J & I is_closed_on s,P & I is_halting_on s,P & not CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS implies IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I )
set ss = Initialize s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),(Initialize s));
set s0 = Initialize s;
set P0 = P +* J;
set s1 = Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set s2 = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P1 = P +* J;
set P2 = P +* (stop I);
set Ik = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))));
assume that
A1: I c= J and
A2: I is_closed_on s,P and
A3: I is_halting_on s,P ; :: thesis: ( CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS or IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I )
A4: dom I c= dom J by A1, GRFUNC_1:2;
reconsider n = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) as Nat ;
A5: stop I c= P +* (stop I) by FUNCT_4:25;
A6: P +* (stop I) halts_on Initialize s by A3, SCMPDS_6:def 3;
A7: IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom (stop I) by A2, SCMPDS_6:def 2;
card (stop I) = (card I) + 1 by COMPOS_1:55;
then n < (card I) + 1 by A7, AFINSQ_1:66;
then A8: n <= card I by INT_1:7;
A9: IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by A1, A2, A3, Th18;
now :: thesis: ( ( n < card I & halt SCMPDS = CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) ) or ( n = card I & IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ) )
per cases ( n < card I or n = card I ) by A8, XXREAL_0:1;
case n < card I ; :: thesis: halt SCMPDS = CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
then A10: n in dom I by AFINSQ_1:66;
thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A6, EXTPRO_1:def 15
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A7, A5, GRFUNC_1:2
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A10, AFINSQ_1:def 3
.= J . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A1, A10, GRFUNC_1:2
.= (P +* J) . (IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A4, A9, A10, FUNCT_4:13
.= CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:143 ; :: thesis: verum
end;
case n = card I ; :: thesis: IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
hence IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I by A1, A2, A3, Th18; :: thesis: verum
end;
end;
end;
hence ( CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS or IC (Comput ((P +* J),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ) ; :: thesis: verum