let s be State of SCMPDS; for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)
let P be Instruction-Sequence of SCMPDS; for I, J being Program of
for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)
let I, J be Program of ; for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)
let k be Nat; ( I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k) )
set m = LifeSpan ((P +* (stop I)),(Initialize s));
assume that
A1:
I c= J
and
A2:
I is_closed_on s,P
and
A3:
I is_halting_on s,P
and
A4:
k <= LifeSpan ((P +* (stop I)),(Initialize s))
; Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)
set s1 = Initialize s;
set s2 = Initialize s;
set P1 = P +* J;
set P2 = P +* (stop I);
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),$1) = Comput ((P +* (stop I)),(Initialize s),$1) );
A5:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A6:
S1[
k]
;
S1[k + 1]now ( k + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1)) )A7:
Comput (
(P +* (stop I)),
(Initialize s),
(k + 1)) =
Following (
(P +* (stop I)),
(Comput ((P +* (stop I)),(Initialize s),k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k)))),
(Comput ((P +* (stop I)),(Initialize s),k)))
;
A8:
Comput (
(P +* J),
(Initialize s),
(k + 1)) =
Following (
(P +* J),
(Comput ((P +* J),(Initialize s),k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k)))),
(Comput ((P +* J),(Initialize s),k)))
;
A9:
k < k + 1
by XREAL_1:29;
assume A10:
k + 1
<= LifeSpan (
(P +* (stop I)),
(Initialize s))
;
Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1))then
k < LifeSpan (
(P +* (stop I)),
(Initialize s))
by A9, XXREAL_0:2;
then A11:
IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I
by A2, A3, SCMPDS_6:26;
then A12:
IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I)
by FUNCT_4:12;
A13:
J c= P +* J
by FUNCT_4:25;
A14:
dom I c= dom J
by A1, RELAT_1:11;
CurInstr (
(P +* J),
(Comput ((P +* J),(Initialize s),k))) =
(P +* J) . (IC (Comput ((P +* (stop I)),(Initialize s),k)))
by A6, A10, A9, PBOOLE:143, XXREAL_0:2
.=
J . (IC (Comput ((P +* (stop I)),(Initialize s),k)))
by A13, A14, A11, GRFUNC_1:2
.=
I . (IC (Comput ((P +* (stop I)),(Initialize s),k)))
by A1, A11, GRFUNC_1:2
.=
(stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),k)))
by A11, AFINSQ_1:def 3
.=
(P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k)))
by A12, FUNCT_4:13
.=
CurInstr (
(P +* (stop I)),
(Comput ((P +* (stop I)),(Initialize s),k)))
by PBOOLE:143
;
hence
Comput (
(P +* J),
(Initialize s),
(k + 1))
= Comput (
(P +* (stop I)),
(Initialize s),
(k + 1))
by A6, A10, A9, A8, A7, XXREAL_0:2;
verum end; hence
S1[
k + 1]
;
verum end;
A15:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A5);
hence
Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)
by A4; verum