let s be 0 -started State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
let P be Instruction-Sequence of SCM+FSA; for I being really-closed Program of st P +* I halts_on s & Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
let I be really-closed Program of ; ( P +* I halts_on s & Directed I c= P implies IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I )
assume that
A1:
P +* I halts_on s
and
A2:
Directed I c= P
; IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
A3:
I c= P +* I
by FUNCT_4:25;
set s2 = s;
set m = LifeSpan ((P +* I),s);
set l1 = IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
A4:
I c= P +* I
by FUNCT_4:25;
IC s = 0
by MEMSTR_0:def 11;
then
IC s in dom I
by AFINSQ_1:65;
then A5:
IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) in dom I
by A4, AMISTD_1:21;
set s1 = s;
A6: P +* (I ";" I) =
P +* (I +* (I ";" I))
by SCMFSA6A:18
.=
(P +* I) +* (I ";" I)
by FUNCT_4:14
;
now for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (Directed I)),s,k)let k be
Nat;
( k <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,k) = Comput ((P +* (Directed I)),s,k) )defpred S1[
Nat]
means ( $1
<= k implies
Comput (
(P +* (I ";" I)),
s,$1)
= Comput (
(P +* (Directed I)),
s,$1) );
assume A7:
k <= LifeSpan (
(P +* I),
s)
;
Comput ((P +* I),s,k) = Comput ((P +* (Directed I)),s,k)A8:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A9:
(
n <= k implies
Comput (
(P +* (I ";" I)),
s,
n)
= Comput (
(P +* (Directed I)),
s,
n) )
;
S1[n + 1]
A10:
Comput (
(P +* (Directed I)),
s,
(n + 1)) =
Following (
(P +* (Directed I)),
(Comput ((P +* (Directed I)),s,n)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,n)))),
(Comput ((P +* (Directed I)),s,n)))
;
A11:
Comput (
(P +* (I ";" I)),
s,
(n + 1)) =
Following (
(P +* (I ";" I)),
(Comput ((P +* (I ";" I)),s,n)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (I ";" I)),(Comput ((P +* (I ";" I)),s,n)))),
(Comput ((P +* (I ";" I)),s,n)))
;
A12:
n <= n + 1
by NAT_1:12;
assume A13:
n + 1
<= k
;
Comput ((P +* (I ";" I)),s,(n + 1)) = Comput ((P +* (Directed I)),s,(n + 1))
IC s = 0
by MEMSTR_0:def 11;
then A14:
IC s in dom I
by AFINSQ_1:65;
n <= k
by A13, A12, XXREAL_0:2;
then
Comput (
(P +* I),
s,
n)
= Comput (
(P +* (I ";" I)),
s,
n)
by A3, Th10, A6, A1, A7, XXREAL_0:2;
then
IC (Comput ((P +* (I ";" I)),s,n)) in dom I
by A3, AMISTD_1:21, A14;
then A15:
IC (Comput ((P +* (Directed I)),s,n)) in dom (Directed I)
by A13, A9, A12, FUNCT_4:99, XXREAL_0:2;
dom (P +* (Directed I)) = NAT
by PARTFUN1:def 2;
then A16:
(P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),s,n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),s,n)))
by PARTFUN1:def 6;
A17:
dom (P +* (I ";" I)) = NAT
by PARTFUN1:def 2;
Directed I c= P +* (Directed I)
by FUNCT_4:25;
then A18:
CurInstr (
(P +* (Directed I)),
(Comput ((P +* (Directed I)),s,n)))
= (Directed I) . (IC (Comput ((P +* (Directed I)),s,n)))
by A15, A16, GRFUNC_1:2;
A19:
(
dom I c= dom (I ";" I) &
CurInstr (
(P +* (I ";" I)),
(Comput ((P +* (I ";" I)),s,n)))
= (P +* (I ";" I)) . (IC (Comput ((P +* (I ";" I)),s,n))) )
by A17, PARTFUN1:def 6, SCMFSA6A:17;
A20:
Directed I c= I ";" I
by SCMFSA6A:16;
I ";" I c= P +* (I ";" I)
by FUNCT_4:25;
then
Directed I c= P +* (I ";" I)
by A20, XBOOLE_1:1;
hence
Comput (
(P +* (I ";" I)),
s,
(n + 1))
= Comput (
(P +* (Directed I)),
s,
(n + 1))
by A9, A13, A12, A18, A11, A10, A15, A19, GRFUNC_1:2, XXREAL_0:2;
verum
end; A21:
S1[
0 ]
;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A21, A8);
then
Comput (
(P +* (I ";" I)),
s,
k)
= Comput (
(P +* (Directed I)),
s,
k)
;
hence
Comput (
(P +* I),
s,
k)
= Comput (
(P +* (Directed I)),
s,
k)
by A7, Th10, A6, A1, FUNCT_4:25;
verum end;
then A22:
Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s)))
;
A23:
dom (P +* I) = NAT
by PARTFUN1:def 2;
I c= P +* I
by FUNCT_4:25;
then A24: I . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) =
(P +* I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))
by A5, GRFUNC_1:2
.=
CurInstr ((P +* I),(Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))
by A23, PARTFUN1:def 6
.=
halt SCM+FSA
by A1, EXTPRO_1:def 15
;
IC (Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s)))) in dom (Directed I)
by A5, A22, FUNCT_4:99;
then A25: (P +* (Directed I)) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) =
(Directed I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))))
by A22, FUNCT_4:13
.=
goto (card I)
by A5, A24, FUNCT_4:106
;
A26:
P +* (Directed I) = P
by A2, FUNCT_4:98;
A27:
dom (P +* (Directed I)) = NAT
by PARTFUN1:def 2;
Comput ((P +* (Directed I)),s,((LifeSpan ((P +* I),s)) + 1)) =
Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s)))))
by EXTPRO_1:3
.=
Exec ((goto (card I)),(Comput ((P +* (Directed I)),s,(LifeSpan ((P +* I),s)))))
by A27, A22, A25, PARTFUN1:def 6
;
hence
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
by A26, SCMFSA_2:69; verum