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 holds
for J being Program of
for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let P be Instruction-Sequence of SCM+FSA; for I being really-closed Program of st P +* I halts_on s holds
for J being Program of
for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let I be really-closed Program of ; ( P +* I halts_on s implies for J being Program of
for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k) )
assume A1:
P +* I halts_on s
; for J being Program of
for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
let J be Program of ; for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
A2:
I c= P +* I
by FUNCT_4:25;
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),s) implies Comput ((P +* I),s,$1) = Comput ((P +* (I ";" J)),s,$1) );
A3:
for m being Nat st S1[m] holds
S1[m + 1]
proof
dom (I ";" J) = (dom I) \/ (dom (Reloc (J,(card I))))
by SCMFSA6A:39;
then A4:
dom I c= dom (I ";" J)
by XBOOLE_1:7;
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A5:
(
m <= LifeSpan (
(P +* I),
s) implies
Comput (
(P +* I),
s,
m)
= Comput (
(P +* (I ";" J)),
s,
m) )
;
S1[m + 1]
A6:
Comput (
(P +* I),
s,
(m + 1)) =
Following (
(P +* I),
(Comput ((P +* I),s,m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* I),(Comput ((P +* I),s,m)))),
(Comput ((P +* I),s,m)))
;
A7:
Comput (
(P +* (I ";" J)),
s,
(m + 1)) =
Following (
(P +* (I ";" J)),
(Comput ((P +* (I ";" J)),s,m)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,m)))),
(Comput ((P +* (I ";" J)),s,m)))
;
IC s = 0
by MEMSTR_0:def 11;
then
IC s in dom I
by AFINSQ_1:65;
then A8:
IC (Comput ((P +* I),s,m)) in dom I
by A2, AMISTD_1:21;
A9:
I c= P +* I
by FUNCT_4:25;
dom (P +* I) = NAT
by PARTFUN1:def 2;
then A10:
CurInstr (
(P +* I),
(Comput ((P +* I),s,m))) =
(P +* I) . (IC (Comput ((P +* I),s,m)))
by PARTFUN1:def 6
.=
I . (IC (Comput ((P +* I),s,m)))
by A8, A9, GRFUNC_1:2
;
assume A11:
m + 1
<= LifeSpan (
(P +* I),
s)
;
Comput ((P +* I),s,(m + 1)) = Comput ((P +* (I ";" J)),s,(m + 1))
A12:
I ";" J c= P +* (I ";" J)
by FUNCT_4:25;
A13:
dom (P +* (I ";" J)) = NAT
by PARTFUN1:def 2;
m < LifeSpan (
(P +* I),
s)
by A11, NAT_1:13;
then
I . (IC (Comput ((P +* I),s,m))) <> halt SCM+FSA
by A1, A10, EXTPRO_1:def 15;
then CurInstr (
(P +* I),
(Comput ((P +* I),s,m))) =
(I ";" J) . (IC (Comput ((P +* I),s,m)))
by A8, A10, SCMFSA6A:15
.=
(P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),s,m)))
by A11, A8, A4, A12, A5, GRFUNC_1:2, NAT_1:13
.=
CurInstr (
(P +* (I ";" J)),
(Comput ((P +* (I ";" J)),s,m)))
by A13, PARTFUN1:def 6
;
hence
Comput (
(P +* I),
s,
(m + 1))
= Comput (
(P +* (I ";" J)),
s,
(m + 1))
by A6, A7, A5, A11, NAT_1:13;
verum
end;
A14:
S1[ 0 ]
;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A14, A3); verum