let s be State of SCMPDS; for I, J being Program of SCMPDS st I c= J & I is_closed_on s & I is_halting_on s & not CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS holds
IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I
let I, J be Program of SCMPDS; ( I c= J & I is_closed_on s & I is_halting_on s & not CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS implies IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I )
set ss = (Initialize s) +* (stop I);
set m = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
A1:
(Initialize s) +* (stop I) = s +* (Initialize (stop I))
by COMPOS_1:125;
set s0 = (Initialize s) +* J;
set s1 = Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
set s2 = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
set Ik = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))));
assume that
A2:
I c= J
and
A3:
I is_closed_on s
and
A4:
I is_halting_on s
; ( CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS or IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I )
A5:
dom I c= dom J
by A2, GRFUNC_1:8;
reconsider n = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) as Element of NAT ;
A6:
stop I c= Initialize (stop I)
by COMPOS_1:126;
Initialize (stop I) c= (Initialize s) +* (stop I)
by A1, FUNCT_4:26;
then A7:
stop I c= (Initialize s) +* (stop I)
by A6, XBOOLE_1:1;
A8:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by A4, SCMPDS_6:def 3;
A9:
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom (stop I)
by A3, SCMPDS_6:def 2;
card (stop I) = (card I) + 1
by SCMPDS_5:7;
then
n < (card I) + 1
by A9, AFINSQ_1:70;
then A10:
n <= card I
by INT_1:20;
A11:
IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by A2, A3, A4, Th39, COMPOS_1:24;
now per cases
( n < card I or n = card I )
by A10, XXREAL_0:1;
case
n < card I
;
halt SCMPDS = CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))then A12:
n in dom I
by AFINSQ_1:70;
A13:
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by COMPOS_1:38;
A14:
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) /. (IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by COMPOS_1:38;
A15:
ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = ProgramPart ((Initialize s) +* (stop I))
by AMI_1:123;
thus halt SCMPDS =
CurInstr (
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),
(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A8, A15, EXTPRO_1:def 14
.=
((Initialize s) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A13, AMI_1:54
.=
(stop I) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A9, A7, GRFUNC_1:8
.=
I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A12, AFINSQ_1:def 4
.=
J . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A2, A12, GRFUNC_1:8
.=
((Initialize s) +* J) . (IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A5, A11, A12, FUNCT_4:14
.=
CurInstr (
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),
(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))
by A14, AMI_1:54
;
verum end;
hence
( CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = halt SCMPDS or IC (Comput ((ProgramPart ((Initialize s) +* J)),((Initialize s) +* J),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I )
; verum