let s be State of SCMPDS; :: thesis: 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)),()) holds
Comput ((P +* J),(),k) = Comput ((P +* (stop I)),(),k)

let P be Instruction-Sequence of SCMPDS; :: thesis: 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)),()) holds
Comput ((P +* J),(),k) = Comput ((P +* (stop I)),(),k)

let I, J be Program of ; :: thesis: 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)),()) holds
Comput ((P +* J),(),k) = Comput ((P +* (stop I)),(),k)

let k be Nat; :: thesis: ( I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),()) implies Comput ((P +* J),(),k) = Comput ((P +* (stop I)),(),k) )
set m = LifeSpan ((P +* (stop I)),());
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)),()) ; :: thesis: Comput ((P +* J),(),k) = Comput ((P +* (stop I)),(),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)),()) implies Comput ((P +* J),(),\$1) = Comput ((P +* (stop I)),(),\$1) );
A5: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 <= LifeSpan ((P +* (stop I)),()) implies Comput ((P +* J),(),(k + 1)) = Comput ((P +* (stop I)),(),(k + 1)) )
A7: Comput ((P +* (stop I)),(),(k + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k)))),(Comput ((P +* (stop I)),(),k))) ;
A8: Comput ((P +* J),(),(k + 1)) = Following ((P +* J),(Comput ((P +* J),(),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* J),(Comput ((P +* J),(),k)))),(Comput ((P +* J),(),k))) ;
A9: k < k + 1 by XREAL_1:29;
assume A10: k + 1 <= LifeSpan ((P +* (stop I)),()) ; :: thesis: Comput ((P +* J),(),(k + 1)) = Comput ((P +* (stop I)),(),(k + 1))
then k < LifeSpan ((P +* (stop I)),()) by ;
then A11: IC (Comput ((P +* (stop I)),(),k)) in dom I by ;
then A12: IC (Comput ((P +* (stop I)),(),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 ;
CurInstr ((P +* J),(Comput ((P +* J),(),k))) = (P +* J) . (IC (Comput ((P +* (stop I)),(),k))) by
.= J . (IC (Comput ((P +* (stop I)),(),k))) by
.= I . (IC (Comput ((P +* (stop I)),(),k))) by
.= (stop I) . (IC (Comput ((P +* (stop I)),(),k))) by
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(),k))) by
.= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),k))) by PBOOLE:143 ;
hence Comput ((P +* J),(),(k + 1)) = Comput ((P +* (stop I)),(),(k + 1)) by ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A15: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A15, A5);
hence Comput ((P +* J),(),k) = Comput ((P +* (stop I)),(),k) by A4; :: thesis: verum