let s be State of ; for I, J being Program of
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 ; 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 (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 i = a =0_goto (insloc ((card J) + 3));
A1:
not a in dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by SCMFSA6B:12;
A2:
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
dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
then A3: (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) =
((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 )
by A2, FUNCT_4:14
.=
(if=0 a,I,J) . (insloc 0 )
by A2, SCMFSA6B:7
.=
a =0_goto (insloc ((card J) + 3))
by Lm3
;
IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by SF_MASTR:65;
then A4: 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
;
A5:
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 A6:
if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by A5, XBOOLE_1:1;
A7:
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;
card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) =
card (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))
by SCMFSA6A:def 6
.=
(card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))
by SCMFSA6A:61
.=
(card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1
by SCMFSA8A:29
.=
((card (Macro (a =0_goto (insloc ((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 (insloc 0 )))
by A6, XBOOLE_1:1;
then
ProgramPart [(ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)))] c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1
by AMI_1:99;
then A8:
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1
by AMI_1:105;
A9: 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 A4, A3
;
A10:
DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by SCMFSA6A:39, SCMFSA8A:14;
A11:
now let f be
FinSeq-Location ;
(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . fthus (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . f
by A10, SCMFSA6A:38
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
by A9, SCMFSA_2:96
;
verum end;
now let a be
Int-Location ;
(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . athus (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a
by A10, SCMFSA6A:38
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
by A9, SCMFSA_2:96
;
verum end;
then A12:
DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),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 (insloc 0 )))) . a = 0
by A1, FUNCT_4:12;
then A13:
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) = insloc ((card J) + 3)
by A9, SCMFSA_2:96;
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 (insloc 0 )))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by SCMFSA7B:def 8;
DataPart s = DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))
by SCMFSA8A:11;
then A18:
I ';' (Stop SCM+FSA ) is_closed_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by A16, Th6;
A19:
(I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
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)per cases
( 0 < k or k = 0 )
;
suppose
0 < 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 A20:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k1) as
Element of
NAT by ORDINAL1:def 13;
insloc m in dom (I ';' (Stop SCM+FSA ))
by A16, SCMFSA7B:def 7;
then A21:
m < card (I ';' (Stop SCM+FSA ))
by SCMFSA6A:15;
A22:
card (I ';' (Stop SCM+FSA )) = (card I) + 1
by SCMFSA6A:61, SCMFSA8A:17;
card (if=0 a,I,J) =
((card I) + (card J)) + 4
by Th14
.=
((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;
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 A20, AMI_1:51
.=
insloc (m + ((card J) + 3))
by A19, A18, A8, A13, A12, Th11
;
hence
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J)
by A23, 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 +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1)) =
CurInstr (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),(LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))))
by AMI_1:51
.=
IncAddr (CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))))),((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 (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