let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for s being 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,P & I is_halting_on s,P holds
( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )
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,P & I is_halting_on s,P holds
( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )
let I, J be Program of SCM+FSA; for a being read-write Int-Location st s . a > 0 & I is_closed_on s,P & I is_halting_on s,P holds
( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )
let a be read-write Int-Location ; ( s . a > 0 & I is_closed_on s,P & I is_halting_on s,P implies ( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P ) )
set I1 = I ';' (Stop SCM+FSA);
set s1 = s +* (Initialize (I ';' (Stop SCM+FSA)));
set P1 = P +* (I ';' (Stop SCM+FSA));
set s3 = s +* (Initialize (if>0 (a,I,J)));
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1);
set i = a >0_goto ((card J) + 3);
A1:
I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA))
by FUNCT_4:26;
A2:
ProgramPart (I ';' (Stop SCM+FSA)) = I ';' (Stop SCM+FSA)
by RELAT_1:209;
A3:
ProgramPart (if>0 (a,I,J)) = if>0 (a,I,J)
by RELAT_1:209;
A4:
not a in dom (Initialize (if>0 (a,I,J)))
by SCMFSA6B:12;
A5:
0 in dom (if>0 (a,I,J))
by Lm2;
A6: (P +* (if>0 (a,I,J))) . 0 =
(if>0 (a,I,J)) . 0
by A5, FUNCT_4:14
.=
a >0_goto ((card J) + 3)
by Lm3
;
IC in dom (Initialize (if>0 (a,I,J)))
by COMPOS_1:141;
then A7: IC (s +* (Initialize (if>0 (a,I,J)))) =
IC (Initialize (if>0 (a,I,J)))
by FUNCT_4:14
.=
0
by COMPOS_1:142
;
A8:
if>0 (a,I,J) c= Initialize (if>0 (a,I,J))
by SCMFSA8A:9;
Initialize (if>0 (a,I,J)) c= s +* (Initialize (if>0 (a,I,J)))
by FUNCT_4:26;
then A9:
if>0 (a,I,J) c= s +* (Initialize (if>0 (a,I,J)))
by A8, XBOOLE_1:1;
A10:
if>0 (a,I,J) c= P +* (if>0 (a,I,J))
by FUNCT_4:26;
A11:
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 COMPOS_1:150
.=
(card J) + (2 + 1)
;
then A12:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if>0 (a,I,J)
by A11, Lm1;
then
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= s +* (Initialize (if>0 (a,I,J)))
by A9, XBOOLE_1:1;
then A13:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)
by AMI_1:81;
A14:
Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= P +* (if>0 (a,I,J))
by A12, A10, XBOOLE_1:1;
A15: Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),(0 + 1)) =
Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),0)))
by EXTPRO_1:4
.=
Following ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))))
by EXTPRO_1:3
.=
Exec ((a >0_goto ((card J) + 3)),(s +* (Initialize (if>0 (a,I,J)))))
by A7, A6, PBOOLE:158
;
A16:
DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) = DataPart (s +* (Initialize (if>0 (a,I,J))))
by COMPOS_1:138, SCMFSA8A:14;
A17:
now let f be
FinSeq-Location ;
(s +* (Initialize (I ';' (Stop SCM+FSA)))) . f = (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) . fthus (s +* (Initialize (I ';' (Stop SCM+FSA)))) . f =
(s +* (Initialize (if>0 (a,I,J)))) . f
by A16, SCMFSA6A:38
.=
(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) . f
by A15, SCMFSA_2:97
;
verum end;
now let a be
Int-Location ;
(s +* (Initialize (I ';' (Stop SCM+FSA)))) . a = (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) . athus (s +* (Initialize (I ';' (Stop SCM+FSA)))) . a =
(s +* (Initialize (if>0 (a,I,J)))) . a
by A16, SCMFSA6A:38
.=
(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) . a
by A15, SCMFSA_2:97
;
verum end;
then A18:
DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) = DataPart (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1))
by A17, SCMFSA6A:38;
assume
s . a > 0
; ( not I is_closed_on s,P or not I is_halting_on s,P or ( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P ) )
then
(s +* (Initialize (if>0 (a,I,J)))) . a > 0
by A4, FUNCT_4:12;
then A19:
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) = (card J) + 3
by A15, SCMFSA_2:97;
assume A20:
I is_closed_on s,P
; ( not I is_halting_on s,P or ( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P ) )
assume A21:
I is_halting_on s,P
; ( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )
then A22:
I ';' (Stop SCM+FSA) is_closed_on s,P
by A20, SCMFSA8A:46;
I ';' (Stop SCM+FSA) is_halting_on s,P
by A20, A21, SCMFSA8A:46;
then A23:
P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA)))
by SCMFSA7B:def 8, A2;
DataPart s = DataPart (s +* (Initialize (I ';' (Stop SCM+FSA))))
by SCMFSA8A:11;
then A24:
I ';' (Stop SCM+FSA) is_closed_on s +* (Initialize (I ';' (Stop SCM+FSA))),P +* (I ';' (Stop SCM+FSA))
by A22, Th6;
A25:
Initialize (I ';' (Stop SCM+FSA)) c= s +* (Initialize (I ';' (Stop SCM+FSA)))
by FUNCT_4:26;
now let k be
Element of
NAT ;
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),b1)) in dom (if>0 (a,I,J))per cases
( 0 < k or k = 0 )
;
suppose
0 < k
;
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),b1)) in dom (if>0 (a,I,J))then consider k1 being
Nat such that A26:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider m =
IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k1)) as
Element of
NAT ;
m in dom (I ';' (Stop SCM+FSA))
by A22, SCMFSA7B:def 7, A2;
then A27:
m < card (I ';' (Stop SCM+FSA))
by AFINSQ_1:70;
card (Stop SCM+FSA) = 1
by COMPOS_1:46;
then A28:
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 A28
;
then A29:
m + ((card J) + 3) < card (if>0 (a,I,J))
by A27, XREAL_1:8;
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) =
IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)),k1))
by A26, EXTPRO_1:5
.=
m + ((card J) + 3)
by A25, A24, A13, A19, A18, Th11, A14, A1
;
hence
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (if>0 (a,I,J))
by A29, AFINSQ_1:70;
verum end; suppose
k = 0
;
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),b1)) in dom (if>0 (a,I,J))hence
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (if>0 (a,I,J))
by A5, A7, EXTPRO_1:3;
verum end; end;
hence
if>0 (a,I,J) is_closed_on s,P
by SCMFSA7B:def 7, A3; if>0 (a,I,J) is_halting_on s,P
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) + 1)))) =
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))))))
by EXTPRO_1:5
.=
IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))))))),((card J) + 3))
by A25, A24, A13, A19, A18, Th11, A14, A1
.=
IncAddr ((halt SCM+FSA),((card J) + 3))
by A23, EXTPRO_1:def 14
.=
halt SCM+FSA
by COMPOS_1:93
;
then
P +* (if>0 (a,I,J)) halts_on s +* (Initialize (if>0 (a,I,J)))
by EXTPRO_1:30;
hence
if>0 (a,I,J) is_halting_on s,P
by SCMFSA7B:def 8, A3; verum