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 & I is_closed_on s & I 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 & I is_closed_on s & I 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 & I is_closed_on s & I 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 s1 = s +* ((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 i = a >0_goto ((card J) + 3);
A1:
not a in dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA6B:12;
A2:
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
dom (if>0 a,I,J) c= dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
then A3: (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 0 =
((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . 0
by A2, FUNCT_4:14
.=
(if>0 a,I,J) . 0
by A2, SCMFSA6B:7
.=
a >0_goto ((card J) + 3)
by Lm3
;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by SF_MASTR:65;
then A4: 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
;
A5:
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 A6:
if>0 a,I,J c= s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by A5, XBOOLE_1:1;
A7:
if>0 a,I,J = (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))
by SCMFSA6A:67;
card (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) =
card (((Macro (a >0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1)))
by SCMFSA6A:def 6
.=
(card ((Macro (a >0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))
by SCMFSA6A:61
.=
(card ((Macro (a >0_goto ((card J) + 3))) ';' J)) + 1
by SCMFSA8A:29
.=
((card (Macro (a >0_goto ((card J) + 3)))) + (card J)) + 1
by SCMFSA6A:61
.=
((card J) + 2) + 1
by SCMFSA7B:6
.=
(card J) + (2 + 1)
;
then
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if>0 a,I,J
by A7, Lm1;
then
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by A6, XBOOLE_1:1;
then
ProgramPart (ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3))) 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 ))),1
by AMI_1:99;
then A8:
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) 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 ))),1
by RELAT_1:209;
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;
A9: 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 A4, A3, Y
;
A10:
DataPart (s +* ((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;
A11:
now let f be
FinSeq-Location ;
(s +* ((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 ))),1) . fthus (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . f =
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . f
by A10, 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 A9, SCMFSA_2:97
;
verum end;
now let a be
Int-Location ;
(s +* ((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 ))),1) . athus (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . a =
(s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a
by A10, 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 A9, SCMFSA_2:97
;
verum end;
then A12:
DataPart (s +* ((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 ))),1)
by A11, SCMFSA6A:38;
assume
s . a > 0
; ( not I is_closed_on s or not I 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 A1, 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) = (card J) + 3
by A9, SCMFSA_2:97;
assume A14:
I is_closed_on s
; ( not I is_halting_on s or ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
assume A15:
I is_halting_on s
; ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
then A16:
I ';' (Stop SCM+FSA ) is_closed_on s
by A14, SCMFSA8A:46;
I ';' (Stop SCM+FSA ) is_halting_on s
by A14, A15, SCMFSA8A:46;
then A17:
ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA7B:def 8;
DataPart s = DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))
by SCMFSA8A:11;
then A18:
I ';' (Stop SCM+FSA ) is_closed_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by A16, Th6;
A19:
(I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:26;
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)per cases
( 0 < k or k = 0 )
;
suppose
0 < 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 A20:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k1) as
Element of
NAT ;
m in dom (I ';' (Stop SCM+FSA ))
by A16, SCMFSA7B:def 7;
then A21:
m < card (I ';' (Stop SCM+FSA ))
by AFINSQ_1:70;
card (Stop SCM+FSA ) = 1
by COMPOS_1:46;
then A22:
card (I ';' (Stop SCM+FSA )) = (card I) + 1
by SCMFSA6A:61;
card (if>0 a,I,J) =
((card I) + (card J)) + 4
by Th15
.=
((card J) + 3) + (card (I ';' (Stop SCM+FSA )))
by A22
;
then A23:
m + ((card J) + 3) < card (if>0 a,I,J)
by A21, XREAL_1:8;
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;
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 (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),k1)
by A20, AMI_1:51
.=
m + ((card J) + 3)
by A19, A18, A8, A13, A12, Th11, T
;
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 A23, 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 A2, A4, AMI_1:13;
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 ))),1)
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 +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1) = 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),(LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))))
by AMI_1:51;
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 +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1)) =
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 ))),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),(LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))
by x, T
.=
IncAddr (CurInstr (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))),((card J) + 3)
by A19, A18, A8, A13, A12, Th11
.=
IncAddr (halt SCM+FSA ),((card J) + 3)
by A17, 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