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;

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 ) )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: verumper cases
( n < card I or n = card I )
by A8, XXREAL_0:1;

end;

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;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

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;