let s be State of SCM+FSA ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) )
assume A1:
s . a > 0
; :: thesis: ( 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 ) )
assume A2:
I is_closed_on s
; :: thesis: ( 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 A3:
I is_halting_on s
; :: thesis: ( 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));
A4:
(I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
I ';' (Stop SCM+FSA ) is_halting_on s
by A2, A3, SCMFSA8A:46;
then A5:
s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting
by SCMFSA7B:def 8;
A6:
I ';' (Stop SCM+FSA ) is_closed_on s
by A2, A3, SCMFSA8A:46;
DataPart s = DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))
by SCMFSA8A:11;
then A7:
I ';' (Stop SCM+FSA ) is_closed_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by A6, Th6;
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;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At (insloc 0 )))
by SF_MASTR:65;
then A10: 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
;
A11: (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, A9, FUNCT_4:14
.=
(if>0 a,I,J) . (insloc 0 )
by A8, SCMFSA6B:7
.=
a >0_goto (insloc ((card J) + 3))
by Lm3
;
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 A10, A11
;
A13: 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)
;
( not a in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) & a in dom s )
by SCMFSA6B:12, SCMFSA_2:66;
then A14:
(s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . a > 0
by A1, FUNCT_4:12;
A15:
(if>0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then A16:
if>0 a,I,J c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))
by A15, XBOOLE_1:1;
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;
then
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if>0 a,I,J
by A13, Lm1;
then
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))
by A16, 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 A17:
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;
A18:
IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) = insloc ((card J) + 3)
by A12, A14, SCMFSA_2:97;
A19:
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;
A20:
now let a be
Int-Location ;
:: thesis: (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 A19, SCMFSA6A:38
.=
(Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
by A12, SCMFSA_2:97
;
:: thesis: verum end;
now let f be
FinSeq-Location ;
:: thesis: (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 A19, SCMFSA6A:38
.=
(Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
by A12, SCMFSA_2:97
;
:: thesis: verum end;
then A21:
DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1)
by A20, SCMFSA6A:38;
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 A4, A7, A17, A18, A21, Th11
.=
IncAddr (halt SCM+FSA ),((card J) + 3)
by A5, AMI_1:def 46
.=
halt SCM+FSA
by SCMFSA_4:8
;
then A22:
s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) is halting
by AMI_1:def 20;
now let k be
Element of
NAT ;
:: thesis: 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
;
:: thesis: 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 A23:
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;
A25:
card (I ';' (Stop SCM+FSA )) = (card I) + 1
by SCMFSA6A:61, SCMFSA8A:17;
A26:
card (if>0 a,I,J) =
((card I) + (card J)) + 4
by Th15
.=
((card J) + 3) + (card (I ';' (Stop SCM+FSA )))
by A25
;
insloc m in dom (I ';' (Stop SCM+FSA ))
by A6, SCMFSA7B:def 7;
then
m < card (I ';' (Stop SCM+FSA ))
by SCMFSA6A:15;
then A27:
m + ((card J) + 3) < card (if>0 a,I,J)
by A26, 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 A23, AMI_1:51
.=
insloc (m + ((card J) + 3))
by A4, A7, A17, A18, A21, Th11
;
hence
IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if>0 a,I,J)
by A27, SCMFSA6A:15;
:: thesis: verum end; end;
hence
if>0 a,I,J is_closed_on s
by SCMFSA7B:def 7; :: thesis: if>0 a,I,J is_halting_on s
thus
if>0 a,I,J is_halting_on s
by A22, SCMFSA7B:def 8; :: thesis: verum