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 & J is_closed_on s,P & J 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 & J is_closed_on s,P & J 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 & J is_closed_on s,P & J 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 & J is_closed_on s,P & J 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 JI2 = ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);
set s2 = Initialize s;
set P2 = P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA));
A3:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) c= P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by FUNCT_4:25;
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 s5 = Comput ((P +* (if=0 (a,I,J))),(Initialize s),2);
set i = a =0_goto ((card J) + 3);
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
then A5: IC (Initialize s) =
IC (Start-At (0,SCM+FSA))
by FUNCT_4:13
.=
0
by FUNCOP_1:72
;
A8:
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:25;
A9: if=0 (a,I,J) =
(((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA))
by SCMFSA6A:25
.=
((a =0_goto ((card J) + 3)) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(a =0_goto ((card J) + 3)) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))))
by SCMFSA6A:29
.=
(a =0_goto ((card J) + 3)) ';' ((J ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)))
by SCMFSA6A:25
.=
(Macro (a =0_goto ((card J) + 3))) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by SCMFSA6A:25
;
then
Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),(card (Macro (a =0_goto ((card J) + 3))))) c= if=0 (a,I,J)
by Lm1;
then A10:
Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= if=0 (a,I,J)
by COMPOS_1:56;
A12:
Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= P +* (if=0 (a,I,J))
by A10, A8, XBOOLE_1:1;
B13:
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
A14:
0 in dom (if=0 (a,I,J))
by Lm2;
A15:
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:25;
A16: (P +* (if=0 (a,I,J))) . 0 =
(if=0 (a,I,J)) . 0
by A14, FUNCT_4:13
.=
a =0_goto ((card J) + 3)
by Lm3
;
A17:
1 in dom (if=0 (a,I,J))
by Lm2;
A18: 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))
by EXTPRO_1:2
.=
Exec ((a =0_goto ((card J) + 3)),(Initialize s))
by A5, A16, PBOOLE:143
;
assume
s . a <> 0
; ( not J is_closed_on s,P or not J 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 B13, FUNCT_4:11;
then A19: IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) =
succ 0
by A5, A18, SCMFSA_2:70
.=
0 + 1
;
A20: (P +* (if=0 (a,I,J))) . 1 =
(if=0 (a,I,J)) . 1
by A17, A15, GRFUNC_1:2
.=
goto 2
by Lm3
;
assume A21:
J is_closed_on s,P
; ( not J 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 ) )
A22: Comput ((P +* (if=0 (a,I,J))),(Initialize s),(1 + 1)) =
Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)))
by A19, A20, PBOOLE:143
;
A24:
now let f be
FinSeq-Location ;
(Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . fthus (Initialize s) . f =
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . f
by A18, SCMFSA_2:70
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . f
by A22, SCMFSA_2:69
;
verum end;
now let a be
Int-Location ;
(Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . athus (Initialize s) . a =
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . a
by A18, SCMFSA_2:70
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . a
by A22, SCMFSA_2:69
;
verum end;
then A25:
DataPart (Initialize s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2))
by A24, SCMFSA6A:7;
assume A26:
J 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 A27:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on s,P
by A21, SCMFSA8A:37;
then A28:
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on Initialize s,P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by Th10;
A29:
P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) halts_on Initialize s
by A21, A26, SCMFSA8A:38;
A30:
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) = 2
by A22, SCMFSA_2:69;
now let k be
Element of
NAT ;
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),b1)) in dom (if=0 (a,I,J))
(
k = 0 or
0 + 1
< k + 1 )
by XREAL_1:6;
then A31:
(
k = 0 or 1
<= k )
by NAT_1:13;
per cases
( 1 < k or k = 0 or k = 1 )
by A31, XXREAL_0:1;
suppose A32:
1
< 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 A33:
k1 + 1
= k
by NAT_1:6;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 12;
0 + 1
< k1 + 1
by A32, A33;
then consider k2 being
Nat such that A34:
k2 + 1
= k1
by NAT_1:6;
reconsider k2 =
k2 as
Element of
NAT by ORDINAL1:def 12;
reconsider m =
IC (Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialize s),k2)) as
Element of
NAT ;
A35:
card (if=0 (a,I,J)) =
(card (Macro (a =0_goto ((card J) + 3)))) + (card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))
by A9, SCMFSA6A:21
.=
2
+ (card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))
by COMPOS_1:56
;
m in dom (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by A27, SCMFSA7B:def 6;
then
m < card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))
by AFINSQ_1:66;
then A36:
m + 2
< card (if=0 (a,I,J))
by A35, 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 A33, EXTPRO_1:4
.=
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)),1)),k2))
by A34, EXTPRO_1:4
.=
IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),(1 + 1))),k2))
by EXTPRO_1:4
.=
m + 2
by A28, A30, A25, Th11, A12, A3
;
hence
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),k)) in dom (if=0 (a,I,J))
by A36, 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 +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialize s))) + 2)))) =
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialize s))))))
by EXTPRO_1:4
.=
IncAddr ((CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialize s),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Initialize s))))))),2)
by A28, A30, A25, Th11, A12, A3
.=
IncAddr ((halt SCM+FSA),2)
by A29, EXTPRO_1:def 15
.=
halt SCM+FSA
by COMPOS_1:11
;
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