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)));
I1:
(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
A1:
I c= J
and
A2:
I is_closed_on s
and
A3:
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 )
A4:
dom I c= dom J
by A1, 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 ;
A5:
stop I c= Initialize (stop I)
by COMPOS_1:126;
Initialize (stop I) c= (Initialize s) +* (stop I)
by I1, FUNCT_4:26;
then A6:
stop I c= (Initialize s) +* (stop I)
by A5, XBOOLE_1:1;
A7:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by A3, SCMPDS_6:def 3;
A8:
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 A2, SCMPDS_6:def 2;
card (stop I) = (card I) + 1
by SCMPDS_5:7;
then
n < (card I) + 1
by A8, AFINSQ_1:70;
then A9:
n <= card I
by INT_1:20;
A10:
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 A1, A2, A3, Th39, COMPOS_1:24;
now per cases
( n < card I or n = card I )
by A9, 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 A11:
n in dom I
by AFINSQ_1:70;
Y:
(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;
Z:
(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;
TX:
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 A7, TX, 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 Y, 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 A8, A6, 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 A11, 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 A1, A11, 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 A4, A10, A11, 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 Z, 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