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 (s +* ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (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 (s +* (I +* (Start-At 0 ,SCM+FSA ))) or
k >= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 )
by NAT_1:13;
then
(
k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) or
k = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 or
k > (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 )
by XXREAL_0:1;
then A5:
(
k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) or
k = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 or
k >= ((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + 1 )
by NAT_1:13;
card (Stop SCM+FSA ) = 1
by SCMNORM:3;
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 (s +* (I +* (Start-At 0 ,SCM+FSA ))) or k = (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 or k >= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 2 )
by A5;
suppose A8:
k <= LifeSpan (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 SCMFSA6A:15;
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 SCMFSA6A:15;
verum end; suppose
k = (LifeSpan (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, SCMFSA6A:15;
verum end; suppose A9:
k >= (LifeSpan (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 (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 (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, SCMFSA6A:15;
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