let s be State of SCM+FSA ; for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 & J is_closed_on s & J is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
let I, J be Program of SCM+FSA ; for a being read-write Int-Location st s . a <= 0 & J is_closed_on s & J is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
let a be read-write Int-Location ; ( s . a <= 0 & J is_closed_on s & J is_halting_on s implies ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
set I1 = I ';' (Stop SCM+FSA );
set JI2 = ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA );
set s2 = s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
set s3 = s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ));
set s4 = Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1;
set s5 = Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2;
set i = a >0_goto ((card J) + 3);
A1:
(((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:26;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by SF_MASTR:65;
then A2: IC (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) =
((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA )
by FUNCT_4:14
.=
0
by SF_MASTR:66
;
A3:
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
(if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ) c= s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:26;
then A4:
if>0 a,I,J c= s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by A3, XBOOLE_1:1;
A5: if>0 a,I,J =
(((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))
by SCMFSA6A:67
.=
((a >0_goto ((card J) + 3)) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )))
by SCMFSA6A:67
.=
(a >0_goto ((card J) + 3)) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA ))))
by SCMFSA6A:71
.=
(a >0_goto ((card J) + 3)) ';' ((J ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))
by SCMFSA6A:67
.=
(a >0_goto ((card J) + 3)) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))
by SCMFSA6A:67
.=
(Macro (a >0_goto ((card J) + 3))) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))
by SCMFSA6A:def 6
;
then
ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),(card (Macro (a >0_goto ((card J) + 3))))) c= if>0 a,I,J
by Lm1;
then
ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2) c= if>0 a,I,J
by SCMFSA7B:6;
then
ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2) c= s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by A4, XBOOLE_1:1;
then
ProgramPart (ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2)) c= Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2
by AMI_1:99;
then A6:
ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2) c= Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2
by AMI_1:105;
A7:
not a in dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA6B:12;
A8:
0 in dom (if>0 a,I,J)
by Lm2;
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A9:
dom (if>0 a,I,J) c= dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
then A10: (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 0 =
((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . 0
by A8, FUNCT_4:14
.=
(if>0 a,I,J) . 0
by A8, SCMFSA6B:7
.=
a >0_goto ((card J) + 3)
by Lm3
;
A11:
1 in dom (if>0 a,I,J)
by Lm2;
Y:
(ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) /. (IC (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) = (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))))
by AMI_1:150;
A12: Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(0 + 1) =
Following (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 )
by AMI_1:14
.=
Following (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))
by AMI_1:13
.=
Exec (a >0_goto ((card J) + 3)),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))
by A2, A10, Y
;
assume
s . a <= 0
; ( not J is_closed_on s or not J is_halting_on s or ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
then
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a <= 0
by A7, FUNCT_4:12;
then A13: IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) =
succ 0
by A2, A12, SCMFSA_2:97
.=
0 + 1
;
A14: (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . 1 =
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 1
by AMI_1:54
.=
((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . 1
by A9, A11, FUNCT_4:14
.=
(if>0 a,I,J) . 1
by A11, SCMFSA6B:7
.=
goto 2
by Lm3
;
assume A15:
J is_closed_on s
; ( not J is_halting_on s or ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
Y:
(ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)) /. (IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)) = (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . (IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1))
by AMI_1:150;
T:
ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)
by AMI_1:144;
A16: Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(1 + 1) =
Following (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)
by AMI_1:14
.=
Exec (goto 2),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)
by A13, A14, Y, T
;
A17:
DataPart (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = DataPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))
by SCMFSA6A:39, SCMFSA8A:14;
A18:
now let f be
FinSeq-Location ;
(s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . f = (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . fthus (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . f =
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . f
by A17, SCMFSA6A:38
.=
(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . f
by A12, SCMFSA_2:97
.=
(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . f
by A16, SCMFSA_2:95
;
verum end;
now let a be
Int-Location ;
(s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . a = (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . athus (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . a =
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a
by A17, SCMFSA6A:38
.=
(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . a
by A12, SCMFSA_2:97
.=
(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . a
by A16, SCMFSA_2:95
;
verum end;
then A19:
DataPart (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = DataPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)
by A18, SCMFSA6A:38;
assume A20:
J is_halting_on s
; ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
then A21:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s
by A15, SCMFSA8A:58;
then A22:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by Th10;
A23:
ProgramPart (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by A15, A20, SCMFSA8A:59;
A24:
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) = 2
by A16, SCMFSA_2:95;
now let k be
Element of
NAT ;
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),b1) in dom (if>0 a,I,J)
(
k = 0 or
0 + 1
< k + 1 )
by XREAL_1:8;
then A25:
(
k = 0 or 1
<= k )
by NAT_1:13;
per cases
( 1 < k or k = 0 or k = 1 )
by A25, XXREAL_0:1;
suppose A26:
1
< k
;
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),b1) in dom (if>0 a,I,J)then consider k1 being
Nat such that A27:
k1 + 1
= k
by NAT_1:6;
0 + 1
< k1 + 1
by A26, A27;
then consider k2 being
Nat such that A28:
k2 + 1
= k1
by NAT_1:6;
reconsider k1 =
k1,
k2 =
k2 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Comput (ProgramPart (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k2) as
Element of
NAT ;
A29:
card (if>0 a,I,J) =
(card (Macro (a >0_goto ((card J) + 3)))) + (card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))
by A5, SCMFSA6A:61
.=
2
+ (card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))
by SCMFSA7B:6
;
S:
ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)
by AMI_1:144;
X:
Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),
(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),1
= Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),
(1 + 1)
by AMI_1:51;
T:
ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),1)
by AMI_1:144;
m in dom (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))
by A21, SCMFSA7B:def 7;
then
m < card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))
by SCMFSA6A:15;
then A30:
m + 2
< card (if>0 a,I,J)
by A29, XREAL_1:8;
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) =
IC (Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),k1)
by A27, T, S, AMI_1:51
.=
IC (Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)),(Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),1),k2)
by A28, AMI_1:51
.=
IC (Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(1 + 1))),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(1 + 1)),k2)
by X, S, T
.=
m + 2
by A1, A22, A6, A24, A19, Th11
;
hence
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if>0 a,I,J)
by A30, SCMFSA6A:15;
verum end; suppose
k = 0
;
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),b1) in dom (if>0 a,I,J)hence
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if>0 a,I,J)
by A8, A2, AMI_1:13;
verum end; suppose
k = 1
;
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),b1) in dom (if>0 a,I,J)hence
IC (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if>0 a,I,J)
by A13, Lm2;
verum end; end;
hence
if>0 a,I,J is_closed_on s
by SCMFSA7B:def 7; if>0 a,I,J is_halting_on s
T:
ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)
by AMI_1:144;
x:
Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 2) = Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2),(LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))))
by AMI_1:51;
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 2))),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 2)) =
CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2),(LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)),(Comput (ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2),(LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))
by x, T
.=
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))),2
by A1, A22, A6, A24, A19, Th11
.=
IncAddr (halt SCM+FSA ),2
by A23, AMI_1:def 46
.=
halt SCM+FSA
by SCMFSA_4:8
;
then
ProgramPart (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by AMI_1:146;
hence
if>0 a,I,J is_halting_on s
by SCMFSA7B:def 8; verum