let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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
NPP (Comput ((P +* J),(Initialize s),k)) = NPP (Comput ((P +* (stop I)),(Initialize s),k))
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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
NPP (Comput ((P +* J),(Initialize s),k)) = NPP (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
NPP (Comput ((P +* J),(Initialize s),k)) = NPP (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 NPP (Comput ((P +* J),(Initialize s),k)) = NPP (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: NPP (Comput ((P +* J),(Initialize s),k)) = NPP (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 NPP (Comput ((P +* J),(Initialize s),$1)) = NPP (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:4
.= 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:4
.= Exec ((CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k)))),(Comput ((P +* J),(Initialize s),k))) ;
A14: k < k + 1 by XREAL_1:31;
assume A15: k + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: NPP (Comput ((P +* J),(Initialize s),(k + 1))) = NPP (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:40;
then A17: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by FUNCT_4:13;
A18: (P +* J) /. (IC (Comput ((P +* J),(Initialize s),k))) = (P +* J) . (IC (Comput ((P +* J),(Initialize s),k))) by PBOOLE:158;
A19: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by PBOOLE:158;
X1: J c= P +* J by FUNCT_4:26;
dom I c= dom J by A1, RELAT_1:25;
then X2: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom J by A16;
CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k))) = (P +* J) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A9, A15, A14, A18, COMPOS_1:230, XXREAL_0:2
.= J . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by X1, X2, GRFUNC_1:8
.= J . (IC (Comput ((P +* (stop I)),(Initialize s),k)))
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A1, A16, GRFUNC_1:8
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A16, AFINSQ_1:def 4
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A17, FUNCT_4:14
.= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) by A19 ;
hence NPP (Comput ((P +* J),(Initialize s),(k + 1))) = NPP (Comput ((P +* (stop I)),(Initialize s),(k + 1))) by A9, A15, A14, A13, A11, SCMPDS_4:15, 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: NPP (Comput ((P +* J),(Initialize s),0)) = NPP (Comput ((P +* (stop I)),(Initialize s),0))
A21: Comput ((P +* (stop I)),(Initialize s),0) = Initialize s by EXTPRO_1:3;
B21: Comput ((P +* J),(Initialize s),0) = Initialize s by EXTPRO_1:3;
thus NPP (Comput ((P +* J),(Initialize s),0)) = NPP (Comput ((P +* (stop I)),(Initialize s),0)) by B21, A21; :: thesis: verum

end;

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