let I, J be Program of SCM+FSA; for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s )
let s be State of SCM+FSA; ( I is_closed_on s & I is_halting_on s implies ( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s ) )
set IJ2 = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA);
assume A1:
I is_closed_on s
; ( not I is_halting_on s or ( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s ) )
set s1 = s +* (I +* (Start-At (0,SCM+FSA)));
set s2 = s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)));
assume A2:
I is_halting_on s
; ( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s )
then A3:
ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))
by A1, Lm5;
A4:
LifeSpan ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2
by A1, A2, Lm5;
now let k be
Element of
NAT ;
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
(
k <= LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) or
k >= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 )
by NAT_1:13;
then
(
k <= LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) or
k = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 or
k > (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 )
by XXREAL_0:1;
then A5:
(
k <= LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA))))) or
k = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 or
k >= ((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1 )
by NAT_1:13;
card (Stop SCM+FSA) = 1
by COMPOS_1:46;
then A6:
card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) =
(card ((I ';' (Goto ((card J) + 1))) ';' J)) + 1
by SCMFSA6A:61
.=
((card (I ';' (Goto ((card J) + 1)))) + (card J)) + 1
by SCMFSA6A:61
.=
(((card I) + (card (Goto ((card J) + 1)))) + (card J)) + 1
by SCMFSA6A:61
.=
(((card I) + 1) + (card J)) + 1
by Lm1
.=
(card I) + (((card J) + 1) + 1)
;
0 <= (card J) + 1
by NAT_1:2;
then
0 + 0 < ((card J) + 1) + 1
by XREAL_1:10;
then A7:
(card I) + 0 < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
by A6, XREAL_1:8;
per cases
( k <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) or k = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 or k >= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2 )
by A5;
suppose A8:
k <= LifeSpan (
(ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),
(s +* (I +* (Start-At (0,SCM+FSA)))))
;
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))reconsider n =
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) as
Element of
NAT ;
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k))
by A1, A2, A8, Lm5;
then
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) in dom I
by A1, SCMFSA7B:def 7;
then
n < card I
by AFINSQ_1:70;
then
n < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
by A7, XXREAL_0:2;
hence
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
by AFINSQ_1:70;
verum end; suppose
k = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1
;
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))then
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) = card I
by A1, A2, Lm5;
hence
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
by A7, AFINSQ_1:70;
verum end; suppose A9:
k >= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 2
;
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) = (((card I) + (card J)) + 1) + 1
by A6;
then A10:
(((card I) + (card J)) + 1) + 0 < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
by XREAL_1:8;
k >= LifeSpan (
(ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),
(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))
by A1, A2, A9, Lm5;
then IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) =
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))))))
by A3, Th5
.=
((card I) + (card J)) + 1
by A1, A2, A4, Lm5
;
hence
IC (Comput ((ProgramPart (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
by A10, AFINSQ_1:70;
verum end; end;
hence
((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s
by SCMFSA7B:def 7; ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s
thus
((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s
by A3, SCMFSA7B:def 8; verum