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