let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds
NPP (Comput (P,s,k)) = NPP (Comput ((P +* (stop I)),s,k))
let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS
for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds
NPP (Comput (P,s,k)) = NPP (Comput ((P +* (stop I)),s,k))
let I be parahalting Program of SCMPDS; :: thesis: for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds
NPP (Comput (P,s,k)) = NPP (Comput ((P +* (stop I)),s,k))
let k be Element of NAT ; :: thesis: ( I c= P & k <= LifeSpan ((P +* (stop I)),s) implies NPP (Comput (P,s,k)) = NPP (Comput ((P +* (stop I)),s,k)) )
set m = LifeSpan ((P +* (stop I)),s);
assume that
A1: I c= P and
A2: k <= LifeSpan ((P +* (stop I)),s) ; :: thesis: NPP (Comput (P,s,k)) = NPP (Comput ((P +* (stop I)),s,k))
set s2 = s;
set P2 = P +* (stop I);
defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),s) implies NPP (Comput (P,s,$1)) = NPP (Comput ((P +* (stop I)),s,$1)) );
A3: P = P +* I by A1, FUNCT_4:104;

A4: now

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

now

A6: Comput ((P +* (stop I)),s,(k + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k)))),(Comput ((P +* (stop I)),s,k))) ;
A7: Comput (P,s,(k + 1)) = Following (P,(Comput (P,s,k))) by EXTPRO_1:4
.= Exec ((CurInstr (P,(Comput (P,s,k)))),(Comput (P,s,k))) ;
A8: k < k + 1 by XREAL_1:31;
assume A9: k + 1 <= LifeSpan ((P +* (stop I)),s) ; :: thesis: NPP (Comput (P,s,(k + 1))) = NPP (Comput ((P +* (stop I)),s,(k + 1)))
then A10: k < LifeSpan ((P +* (stop I)),s) by A8, XXREAL_0:2;
then IC (Comput ((P +* (stop I)),s,k)) in dom I by Th28;
then A11: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by FUNCT_4:13;
A12: IC (Comput ((P +* (stop I)),s,k)) in dom I by A10, Th28;
IC (Comput (P,s,k)) = IC (Comput ((P +* (stop I)),s,k)) by A5, A9, A8, COMPOS_1:230, XXREAL_0:2;
then CurInstr (P,(Comput (P,s,k))) = P . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:158
.= I . (IC (Comput ((P +* (stop I)),s,k))) by A3, A10, Th28, FUNCT_4:14
.= (stop I) . (IC (Comput ((P +* (stop I)),s,k))) by A12, AFINSQ_1:def 4
.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by A11, FUNCT_4:14
.= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) by PBOOLE:158 ;
hence NPP (Comput (P,s,(k + 1))) = NPP (Comput ((P +* (stop I)),s,(k + 1))) by A5, A9, A8, A7, A6, SCMPDS_4:15, XXREAL_0:2; :: thesis: verum

end;

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

end;

A13: S₁[ 0 ]

proof

assume 0 <= LifeSpan ((P +* (stop I)),s) ; :: thesis: NPP (Comput (P,s,0)) = NPP (Comput ((P +* (stop I)),s,0))
A14: Comput ((P +* (stop I)),s,0) = s by EXTPRO_1:3;
Comput (P,s,0) = s by EXTPRO_1:3;
hence NPP (Comput (P,s,0)) = NPP (Comput ((P +* (stop I)),s,0)) by A14; :: thesis: verum

end;

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