let P be Instruction-Sequence of SCM+FSA; 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 = Initialize s;
set P1 = P +* (I ";" (Stop SCM+FSA));
set s3 = Initialize s;
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(Initialize s),1);
set i = a =0_goto ((card J) + 3);
A1:
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
A2:
0 in dom (if=0 (a,I,J))
by Lm2;
A3: (P +* (if=0 (a,I,J))) . 0 =
(if=0 (a,I,J)) . 0
by A2, FUNCT_4:13
.=
a =0_goto ((card J) + 3)
by Lm3
;
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
then A4: IC (Initialize s) =
IC (Start-At (0,SCM+FSA))
by FUNCT_4:13
.=
0
by FUNCOP_1:72
;
A5:
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:25;
A6:
if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))
by SCMFSA6A:25;
card (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) =
(card ((Macro (a =0_goto ((card J) + 3))) ";" J)) + (card (Goto ((card I) + 1)))
by SCMFSA6A:21
.=
(card ((Macro (a =0_goto ((card J) + 3))) ";" J)) + 1
by SCMFSA8A:15
.=
((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1
by SCMFSA6A:21
.=
((card J) + 2) + 1
by COMPOS_1:56
.=
(card J) + (2 + 1)
;
then A7:
Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J)
by A6, Lm1;
A8:
Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= P +* (if=0 (a,I,J))
by A7, A5, XBOOLE_1:1;
A9: Comput ((P +* (if=0 (a,I,J))),(Initialize s),(0 + 1)) =
Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),0)))
by EXTPRO_1:3
.=
Following ((P +* (if=0 (a,I,J))),(Initialize s))
.=
Exec ((a =0_goto ((card J) + 3)),(Initialize s))
by A4, A3, PBOOLE:143
;
A10:
for f being FinSeq-Location holds (Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . f
by A9, SCMFSA_2:70;
for a being Int-Location holds (Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . a
by A9, SCMFSA_2:70;
then A11:
DataPart (Initialize s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1))
by A10, SCMFSA_M:2;
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
(Initialize s) . a = 0
by A1, FUNCT_4:11;
then A12:
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) = (card J) + 3
by A9, SCMFSA_2:70;
assume A13:
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 A14:
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 A15:
I ";" (Stop SCM+FSA) is_closed_on s,P
by A13, SCMFSA8A:30;
I ";" (Stop SCM+FSA) is_halting_on s,P
by A13, A14, SCMFSA8A:30;
then A16:
P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s
by SCMFSA7B:def 7;
DataPart s = DataPart (Initialize s)
by MEMSTR_0:79;
then A17:
I ";" (Stop SCM+FSA) is_closed_on Initialize s,P +* (I ";" (Stop SCM+FSA))
by A15, Th3;
A18:
I ";" (Stop SCM+FSA) c= P +* (I ";" (Stop SCM+FSA))
by FUNCT_4:25;
now for k being Element of NAT holds IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),k)) in dom (if=0 (a,I,J))let k be
Element of
NAT ;
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),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))),(Initialize s),b1)) in dom (if=0 (a,I,J))then consider k1 being
Nat such that A19:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 12;
reconsider m =
IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k1)) as
Element of
NAT ;
m in dom (I ";" (Stop SCM+FSA))
by A15, SCMFSA7B:def 6;
then A20:
m < card (I ";" (Stop SCM+FSA))
by AFINSQ_1:66;
card (Stop SCM+FSA) = 1
by COMPOS_1:4;
then A21:
card (I ";" (Stop SCM+FSA)) = (card I) + 1
by SCMFSA6A:21;
card (if=0 (a,I,J)) =
((card I) + (card J)) + 4
by Th11
.=
((card J) + 3) + (card (I ";" (Stop SCM+FSA)))
by A21
;
then A22:
m + ((card J) + 3) < card (if=0 (a,I,J))
by A20, XREAL_1:6;
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),k)) =
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)),k1))
by A19, EXTPRO_1:4
.=
m + ((card J) + 3)
by A17, A12, A11, Th8, A18, A8
;
hence
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),k)) in dom (if=0 (a,I,J))
by A22, AFINSQ_1:66;
verum end; end;
hence
if=0 (a,I,J) is_closed_on s,P
by SCMFSA7B:def 6; if=0 (a,I,J) is_halting_on s,P
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),((LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1)))) =
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))))))
by EXTPRO_1:4
.=
IncAddr ((CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))))))),((card J) + 3))
by A17, A12, A11, Th8, A8, A18
.=
IncAddr ((halt SCM+FSA),((card J) + 3))
by A16, EXTPRO_1:def 15
.=
halt SCM+FSA
by COMPOS_0:4
;
then
P +* (if=0 (a,I,J)) halts_on Initialize s
by EXTPRO_1:29;
hence
if=0 (a,I,J) is_halting_on s,P
by SCMFSA7B:def 7; verum