let s be State of SCM+FSA; SCM_HALT:def 2 ( Initialize ((intloc 0) .--> 1) c= s implies for p being Instruction-Sequence of SCM+FSA st I ";" J c= p holds
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A1:
Initialize ((intloc 0) .--> 1) c= s
; for p being Instruction-Sequence of SCM+FSA st I ";" J c= p holds
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1
then A2:
Initialized s = s
by FUNCT_4:98;
let p be Instruction-Sequence of SCM+FSA; ( I ";" J c= p implies for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A3:
I ";" J c= p
; for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1
then A4:
p +* (I ";" J) = p
by FUNCT_4:98;
A5:
I c= p +* I
by FUNCT_4:25;
A6:
Initialize ((intloc 0) .--> 1) c= Initialized s
by FUNCT_4:25;
per cases
( p +* I halts_on Initialized s or not p +* I halts_on Initialized s )
;
suppose A7:
p +* I halts_on Initialized s
;
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1let k be
Nat;
(Comput (p,s,k)) . (intloc 0) = 1A8:
Initialized s = s
by A1, FUNCT_4:98;
per cases
( k <= LifeSpan ((p +* I),(Initialized s)) or k > LifeSpan ((p +* I),(Initialized s)) )
;
suppose A9:
k <= LifeSpan (
(p +* I),
(Initialized s))
;
(Comput (p,s,k)) . (intloc 0) = 1
(Comput ((p +* I),(Initialized s),k)) . (intloc 0) = 1
by Def2, A5, A6;
hence
(Comput (p,s,k)) . (intloc 0) = 1
by A2, A7, A9, Th12, A4;
verum end; suppose A10:
k > LifeSpan (
(p +* I),
(Initialized s))
;
(Comput (p,s,k)) . (intloc 0) = 1set LS =
LifeSpan (
(p +* I),
(Initialized s));
consider pp being
Element of
NAT such that A11:
k = (LifeSpan ((p +* I),(Initialized s))) + pp
and A12:
1
<= pp
by A10, FINSEQ_4:84;
consider r being
Nat such that A13:
pp = 1
+ r
by A12, NAT_1:10;
reconsider r =
r as
Element of
NAT by ORDINAL1:def 12;
set Rr =
Comput (
((p +* I) +* J),
((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),
r);
set Sr =
Start-At (
((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),
SCM+FSA);
A14:
Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:25;
J c= (p +* I) +* J
by FUNCT_4:25;
then A15:
(Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) . (intloc 0) = 1
by Def2, A14;
(
dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) = {(IC )} &
intloc 0 <> IC )
by SCMFSA_2:56;
then A16:
not
intloc 0 in dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA))
by TARSKI:def 1;
(Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) = Comput (
(p +* (I ";" J)),
s,
(((LifeSpan ((p +* I),(Initialized s))) + 1) + r))
by A1, A7, A8, Th14, A3;
hence
(Comput (p,s,k)) . (intloc 0) = 1
by A11, A13, A15, A16, A4, FUNCT_4:11;
verum end; end; suppose A17:
not
p +* I halts_on Initialized s
;
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1let k be
Nat;
(Comput (p,s,k)) . (intloc 0) = 1
(Comput ((p +* I),(Initialized s),k)) . (intloc 0) = 1
by Def2, A5, A6;
hence
(Comput (p,s,k)) . (intloc 0) = 1
by A2, A4, A17, Th15;
verum end;