let s be 0 -started State of SCM+FSA; SCMFSA6B:def 4 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) = s . (intloc 0)
let P be Instruction-Sequence of SCM+FSA; ( I ";" J c= P implies for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A1:
I ";" J c= P
; for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A2:
I c= P +* I
by FUNCT_4:25;
A3:
P = P +* (I ";" J)
by A1, FUNCT_4:98;
per cases
( P +* I halts_on s or not P +* I halts_on s )
;
suppose A4:
P +* I halts_on s
;
for k being Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)let k be
Nat;
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)hereby verum
per cases
( k <= LifeSpan ((P +* I),s) or k > LifeSpan ((P +* I),s) )
;
suppose A6:
k > LifeSpan (
(P +* I),
s)
;
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)set LS =
LifeSpan (
(P +* I),
s);
consider p being
Element of
NAT such that A7:
k = (LifeSpan ((P +* I),s)) + p
and A8:
1
<= p
by A6, FINSEQ_4:84;
consider r being
Nat such that A9:
p = 1
+ r
by A8, NAT_1:10;
(
dom (Start-At (0,SCM+FSA)) = {(IC )} &
intloc 0 <> IC )
by SCMFSA_2:56;
then A10:
not
intloc 0 in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
reconsider r =
r as
Element of
NAT by ORDINAL1:def 12;
(
dom (Start-At (((IC (Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r))) + (card I)),SCM+FSA)) = {(IC )} &
intloc 0 <> IC )
by SCMFSA_2:56;
then A11:
not
intloc 0 in dom (Start-At (((IC (Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r))) + (card I)),SCM+FSA))
by TARSKI:def 1;
A12:
IncIC (
(Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r)),
(card I))
= Comput (
(P +* (I ";" J)),
s,
(((LifeSpan ((P +* I),s)) + 1) + r))
by A4, Th16, A1;
A13:
J c= (P +* I) +* J
by FUNCT_4:25;
(Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),r)) . (intloc 0) =
(Initialize (Result ((P +* I),s))) . (intloc 0)
by Def2, A13
.=
(Result ((P +* I),s)) . (intloc 0)
by A10, FUNCT_4:11
.=
(Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . (intloc 0)
by A4, EXTPRO_1:23
.=
s . (intloc 0)
by Def2, A2
;
hence
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
by A7, A9, A12, A3, A11, FUNCT_4:11;
verum end; end;
end; end; end;