let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m)
let s be State of SCM+FSA; for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m)
set A = NAT ;
let I be Program of SCM+FSA; ( I is_closed_on s,P & I is_halting_on s,P implies for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m) )
set s1 = Initialize s;
set P1 = P +* I;
A2:
I c= P +* I
by FUNCT_4:25;
set s2 = Initialize s;
set P2 = P +* (loop I);
A3:
loop I c= P +* (loop I)
by FUNCT_4:25;
assume A4:
I is_closed_on s,P
; ( not I is_halting_on s,P or for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m) )
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),$1) = Comput ((P +* (loop I)),(Initialize s),$1) );
assume
I is_halting_on s,P
; for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m)
then A5:
P +* I halts_on Initialize s
by SCMFSA7B:def 7;
A6:
for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be
Element of
NAT ;
( S1[m] implies S1[m + 1] )
assume A7:
(
m <= LifeSpan (
(P +* I),
(Initialize s)) implies
Comput (
(P +* I),
(Initialize s),
m)
= Comput (
(P +* (loop I)),
(Initialize s),
m) )
;
S1[m + 1]
A8:
Comput (
(P +* I),
(Initialize s),
(m + 1))
= Following (
(P +* I),
(Comput ((P +* I),(Initialize s),m)))
by EXTPRO_1:3;
A9:
Comput (
(P +* (loop I)),
(Initialize s),
(m + 1))
= Following (
(P +* (loop I)),
(Comput ((P +* (loop I)),(Initialize s),m)))
by EXTPRO_1:3;
A10:
IC (Comput ((P +* I),(Initialize s),m)) in dom I
by A4, SCMFSA7B:def 6;
A11:
(P +* I) /. (IC (Comput ((P +* I),(Initialize s),m))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),m)))
by PBOOLE:143;
A12:
CurInstr (
(P +* I),
(Comput ((P +* I),(Initialize s),m)))
= I . (IC (Comput ((P +* I),(Initialize s),m)))
by A10, A11, A2, GRFUNC_1:2;
assume A13:
m + 1
<= LifeSpan (
(P +* I),
(Initialize s))
;
Comput ((P +* I),(Initialize s),(m + 1)) = Comput ((P +* (loop I)),(Initialize s),(m + 1))
then
m < LifeSpan (
(P +* I),
(Initialize s))
by NAT_1:13;
then B14:
I . (IC (Comput ((P +* I),(Initialize s),m))) <> halt SCM+FSA
by A5, A12, EXTPRO_1:def 15;
A15:
(P +* (loop I)) /. (IC (Comput ((P +* (loop I)),(Initialize s),m))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),(Initialize s),m)))
by PBOOLE:143;
A16:
IC (Comput ((P +* I),(Initialize s),m)) in dom (loop I)
by A10, FUNCT_4:99;
CurInstr (
(P +* I),
(Comput ((P +* I),(Initialize s),m))) =
(P +* I) . (IC (Comput ((P +* I),(Initialize s),m)))
by PBOOLE:143
.=
I . (IC (Comput ((P +* I),(Initialize s),m)))
by A2, A10, GRFUNC_1:2
.=
(loop I) . (IC (Comput ((P +* I),(Initialize s),m)))
by B14, FUNCT_4:105
.=
(P +* (loop I)) . (IC (Comput ((P +* I),(Initialize s),m)))
by A3, A16, GRFUNC_1:2
.=
CurInstr (
(P +* (loop I)),
(Comput ((P +* (loop I)),(Initialize s),m)))
by A7, A13, A15, NAT_1:13
;
hence
Comput (
(P +* I),
(Initialize s),
(m + 1))
= Comput (
(P +* (loop I)),
(Initialize s),
(m + 1))
by A7, A13, A8, A9, NAT_1:13;
verum
end;
A17:
S1[ 0 ]
proof
assume
0 <= LifeSpan (
(P +* I),
(Initialize s))
;
Comput ((P +* I),(Initialize s),0) = Comput ((P +* (loop I)),(Initialize s),0)
Initialize s = Comput (
(P +* (loop I)),
(Initialize s),
0)
by EXTPRO_1:2;
hence
Comput (
(P +* I),
(Initialize s),
0)
= Comput (
(P +* (loop I)),
(Initialize s),
0)
by EXTPRO_1:2;
verum
end;
thus
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A17, A6); verum