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 COMPOS_1:141;
then A2: IC (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) =
IC ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))
by FUNCT_4:14
.=
0
by COMPOS_1:142
;
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 COMPOS_1:150;
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 RELAT_1:209;
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 COMPOS_1:38;
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 EXTPRO_1:4
.=
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 EXTPRO_1:3
.=
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 COMPOS_1:38;
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:123;
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 EXTPRO_1:4
.=
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 COMPOS_1:150
;
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:123;
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 EXTPRO_1:5;
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:123;
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 AFINSQ_1:70;
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, S, EXTPRO_1:5
.=
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, EXTPRO_1:5
.=
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, AFINSQ_1:70;
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, EXTPRO_1:3;
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:123;
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 ((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)))))) + 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 ((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)))))))
by EXTPRO_1:5;
CurInstr ((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)))),((LifeSpan ((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)))))) + 2)))) =
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)))),2))),(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 ((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)))))))))
by x, T
.=
IncAddr ((CurInstr ((ProgramPart (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 ((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)))))))))),2)
by A1, A22, A6, A24, A19, Th11
.=
IncAddr ((halt SCM+FSA),2)
by A23, EXTPRO_1:def 14
.=
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 EXTPRO_1:30;
hence
if>0 (a,I,J) is_halting_on s
by SCMFSA7B:def 8; verum