let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of SCMPDS
for k being Element of 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; :: thesis: for I, J being Program of SCMPDS
for k being Element of 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 SCMPDS; :: thesis: for k being Element of 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 Element of NAT ; :: thesis: ( 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)) ; :: thesis: 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 S₁[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),$1) = Comput ((P +* (stop I)),(Initialize s),$1) );

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now

A11: 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))) ;
A13: 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))) ;
A14: k < k + 1 by XREAL_1:29;
assume A15: k + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1))
then k < LifeSpan ((P +* (stop I)),(Initialize s)) by A14, XXREAL_0:2;
then A16: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I by A2, A3, SCMPDS_6:26;
then A17: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by FUNCT_4:12;
X1: J c= P +* J by FUNCT_4:25;
X2: 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 A9, A15, A14, PBOOLE:143, XXREAL_0:2
.= J . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by X1, X2, GRFUNC_1:2, A16
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A1, A16, GRFUNC_1:2
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A16, AFINSQ_1:def 3
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A17, 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 A9, A15, A14, A13, A11, XXREAL_0:2; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A20: S₁[ 0 ]

proof

assume 0 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* J),(Initialize s),0) = Comput ((P +* (stop I)),(Initialize s),0)
Comput ((P +* (stop I)),(Initialize s),0) = Initialize s by EXTPRO_1:2;
hence Comput ((P +* J),(Initialize s),0) = Comput ((P +* (stop I)),(Initialize s),0) by EXTPRO_1:2; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A20, A8);
hence Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k) by A4; :: thesis: verum