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_onInit s,p & I is_halting_onInit s,p holds
for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds
Comput ((p +* I),(Initialized s),m) = Comput ((p +* (loop I)),(Initialized s),m)
let s be State of SCM+FSA; for I being Program of SCM+FSA st I is_closed_onInit s,p & I is_halting_onInit s,p holds
for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds
Comput ((p +* I),(Initialized s),m) = Comput ((p +* (loop I)),(Initialized s),m)
let I be Program of SCM+FSA; ( I is_closed_onInit s,p & I is_halting_onInit s,p implies for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds
Comput ((p +* I),(Initialized s),m) = Comput ((p +* (loop I)),(Initialized s),m) )
set s1 = Initialized s;
set p1 = p +* I;
A1:
I c= p +* I
by FUNCT_4:25;
set s2 = Initialized s;
set p2 = p +* (loop I);
A2:
loop I c= p +* (loop I)
by FUNCT_4:25;
assume A3:
I is_closed_onInit s,p
; ( not I is_halting_onInit s,p or for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds
Comput ((p +* I),(Initialized s),m) = Comput ((p +* (loop I)),(Initialized s),m) )
defpred S1[ Nat] means ( $1 <= LifeSpan ((p +* I),(Initialized s)) implies Comput ((p +* I),(Initialized s),$1) = Comput ((p +* (loop I)),(Initialized s),$1) );
assume
I is_halting_onInit s,p
; for m being Element of NAT st m <= LifeSpan ((p +* I),(Initialized s)) holds
Comput ((p +* I),(Initialized s),m) = Comput ((p +* (loop I)),(Initialized s),m)
then A4:
p +* I halts_on Initialized s
by Def5;
A5:
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 A6:
(
m <= LifeSpan (
(p +* I),
(Initialized s)) implies
Comput (
(p +* I),
(Initialized s),
m)
= Comput (
(p +* (loop I)),
(Initialized s),
m) )
;
S1[m + 1]
A7:
IC (Comput ((p +* I),(Initialized s),m)) in dom I
by A3, Def4;
then A8:
IC (Comput ((p +* I),(Initialized s),m)) in dom (loop I)
by FUNCT_4:99;
A9:
(p +* I) /. (IC (Comput ((p +* I),(Initialized s),m))) = (p +* I) . (IC (Comput ((p +* I),(Initialized s),m)))
by PBOOLE:143;
A10:
CurInstr (
(p +* I),
(Comput ((p +* I),(Initialized s),m)))
= I . (IC (Comput ((p +* I),(Initialized s),m)))
by A7, A9, A1, GRFUNC_1:2;
A11:
Comput (
(p +* (loop I)),
(Initialized s),
(m + 1)) =
Following (
(p +* (loop I)),
(Comput ((p +* (loop I)),(Initialized s),m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((p +* (loop I)),(Comput ((p +* (loop I)),(Initialized s),m)))),
(Comput ((p +* (loop I)),(Initialized s),m)))
;
A12:
Comput (
(p +* I),
(Initialized s),
(m + 1)) =
Following (
(p +* I),
(Comput ((p +* I),(Initialized s),m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((p +* I),(Comput ((p +* I),(Initialized s),m)))),
(Comput ((p +* I),(Initialized s),m)))
;
assume A13:
m + 1
<= LifeSpan (
(p +* I),
(Initialized s))
;
Comput ((p +* I),(Initialized s),(m + 1)) = Comput ((p +* (loop I)),(Initialized s),(m + 1))
then
m < LifeSpan (
(p +* I),
(Initialized s))
by NAT_1:13;
then
I . (IC (Comput ((p +* I),(Initialized s),m))) <> halt SCM+FSA
by A4, A10, EXTPRO_1:def 15;
then A14:
I . (IC (Comput ((p +* I),(Initialized s),m))) = (loop I) . (IC (Comput ((p +* I),(Initialized s),m)))
by FUNCT_4:105;
A15:
(p +* (loop I)) /. (IC (Comput ((p +* (loop I)),(Initialized s),m))) = (p +* (loop I)) . (IC (Comput ((p +* (loop I)),(Initialized s),m)))
by PBOOLE:143;
thus
Comput (
(p +* I),
(Initialized s),
(m + 1))
= Comput (
(p +* (loop I)),
(Initialized s),
(m + 1))
by A6, A13, A12, A11, A8, A10, A15, A14, A2, GRFUNC_1:2, NAT_1:13;
verum
end;
A16:
S1[ 0 ]
proof
assume
0 <= LifeSpan (
(p +* I),
(Initialized s))
;
Comput ((p +* I),(Initialized s),0) = Comput ((p +* (loop I)),(Initialized s),0)
Initialized s = Comput (
(p +* (loop I)),
(Initialized s),
0)
by EXTPRO_1:2;
hence
Comput (
(p +* I),
(Initialized s),
0)
= Comput (
(p +* (loop I)),
(Initialized s),
0)
by EXTPRO_1:2;
verum
end;
thus
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A16, A5); verum