let s be State of ; for I, J being Program of
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 ; 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 (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );
set s2 = s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
set s3 = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1;
set s5 = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2;
set i = a =0_goto (insloc ((card J) + 3));
A1:
(((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by SF_MASTR:65;
then A2: IC (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) =
((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA )
by FUNCT_4:14
.=
insloc 0
by SF_MASTR:66
;
A3:
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
(if=0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
then A4:
if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by A3, XBOOLE_1:1;
A5: if=0 a,I,J =
(((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA ))
by SCMFSA6A:67
.=
((a =0_goto (insloc ((card J) + 3))) ';' J) ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))
by SCMFSA6A:67
.=
(a =0_goto (insloc ((card J) + 3))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))))
by SCMFSA6A:71
.=
(a =0_goto (insloc ((card J) + 3))) ';' ((J ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )))
by SCMFSA6A:67
.=
(a =0_goto (insloc ((card J) + 3))) ';' (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))
by SCMFSA6A:67
.=
(Macro (a =0_goto (insloc ((card J) + 3)))) ';' (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))
by SCMFSA6A:def 6
;
then
ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),(card (Macro (a =0_goto (insloc ((card J) + 3)))))) c= if=0 a,I,J
by Lm1;
then
ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= if=0 a,I,J
by SCMFSA7B:6;
then
ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by A4, XBOOLE_1:1;
then
ProgramPart [(ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2))] c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2
by AMI_1:99;
then A6:
ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2
by AMI_1:105;
A7:
not a in dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by SCMFSA6B:12;
A8:
insloc 0 in dom (if=0 a,I,J)
by Lm2;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then A9:
dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
then A10: (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) =
((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 )
by A8, FUNCT_4:14
.=
(if=0 a,I,J) . (insloc 0 )
by A8, SCMFSA6B:7
.=
a =0_goto (insloc ((card J) + 3))
by Lm3
;
A11:
insloc 1 in dom (if=0 a,I,J)
by Lm2;
A12: Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) =
Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 )
by AMI_1:14
.=
Following (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by AMI_1:13
.=
Exec (a =0_goto (insloc ((card J) + 3))),(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by A2, A10
;
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 (insloc 0 )))) . a <> 0
by A7, FUNCT_4:12;
then A13: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) =
Next (insloc 0 )
by A2, A12, SCMFSA_2:96
.=
insloc (0 + 1)
;
A14: (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . (insloc 1) =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 1)
by AMI_1:54
.=
((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 1)
by A9, A11, FUNCT_4:14
.=
(if=0 a,I,J) . (insloc 1)
by A11, SCMFSA6B:7
.=
goto (insloc 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 ) )
A16: Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(1 + 1) =
Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1)
by AMI_1:14
.=
Exec (goto (insloc 2)),(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1)
by A13, A14
;
A17:
DataPart (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by SCMFSA6A:39, SCMFSA8A:14;
A18:
now let f be
FinSeq-Location ;
(s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) . fthus (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . f
by A17, SCMFSA6A:38
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
by A12, SCMFSA_2:96
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) . f
by A16, SCMFSA_2:95
;
verum end;
now let a be
Int-Location ;
(s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) . athus (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a
by A17, SCMFSA6A:38
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
by A12, SCMFSA_2:96
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) . a
by A16, SCMFSA_2:95
;
verum end;
then A19:
DataPart (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),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 (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s
by A15, SCMFSA8A:58;
then A22:
((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by Th10;
A23:
ProgramPart (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by A15, A20, SCMFSA8A:59;
A24:
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) = insloc 2
by A16, SCMFSA_2:95;
now let k be
Element of
NAT ;
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),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 (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)then consider k1 being
Nat such that A27:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
0 + 1
< k1 + 1
by A26, A27;
then consider k2 being
Nat such that A28:
k2 + 1
= k1
by NAT_1:6;
reconsider k2 =
k2 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Computation (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k2) as
Element of
NAT by ORDINAL1:def 13;
A29:
card (if=0 a,I,J) =
(card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))
by A5, SCMFSA6A:61
.=
2
+ (card (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))
by SCMFSA7B:6
;
insloc m in dom (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))
by A21, SCMFSA7B:def 7;
then
m < card (((J ';' (Goto (insloc ((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 (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) =
IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),k1)
by A27, AMI_1:51
.=
IC (Computation (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),1),k2)
by A28, AMI_1:51
.=
IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(1 + 1)),k2)
by AMI_1:51
.=
insloc (m + 2)
by A1, A22, A6, A24, A19, Th11
;
hence
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J)
by A30, SCMFSA6A:15;
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
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 2)) =
CurInstr (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2),(LifeSpan (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))))
by AMI_1:51
.=
IncAddr (CurInstr (Computation (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))))),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 (insloc 0 )))) halts_on s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by AMI_1:146;
hence
if=0 a,I,J is_halting_on s
by SCMFSA7B:def 8; verum