let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
let I be parahalting Program of SCMPDS; :: thesis: for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
let J be Program of SCMPDS; :: thesis: for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* (stop I)),(Initialize s)) implies NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k)) )
set spI = stop I;
set s1 = Initialize s;
set P1 = P +* (stop I);
set s2 = Initialize s;
set P2 = P +* (I ';' J);
set n = LifeSpan ((P +* (stop I)),(Initialize s));
defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies NPP (Comput ((P +* (stop I)),(Initialize s),$1)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),$1)) );
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: ( m <= LifeSpan ((P +* (stop I)),(Initialize s)) implies NPP (Comput ((P +* (stop I)),(Initialize s),m)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),m)) ) ; :: thesis: S₁[m + 1]
A4: Comput ((P +* (I ';' J)),(Initialize s),(m + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m)))),(Comput ((P +* (I ';' J)),(Initialize s),m))) ;
A5: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by FUNCT_4:26, SCMPDS_4:def 9;
A6: Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m)))),(Comput ((P +* (stop I)),(Initialize s),m))) ;
assume A7: m + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: NPP (Comput ((P +* (stop I)),(Initialize s),(m + 1))) = NPP (Comput ((P +* (I ';' J)),(Initialize s),(m + 1)))
then A8: IC (Comput ((P +* (stop I)),(Initialize s),m)) = IC (Comput ((P +* (I ';' J)),(Initialize s),m)) by A3, COMPOS_1:230, NAT_1:13;
A9: m < LifeSpan ((P +* (stop I)),(Initialize s)) by A7, NAT_1:13;
then IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I by Th28;
then A10: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (I ';' J) by FUNCT_4:13;
A11: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I by A9, Th28;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by PBOOLE:158
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A5, FUNCT_4:14
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A11, AFINSQ_1:def 4
.= (I ';' J) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A11, AFINSQ_1:def 4
.= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A10, FUNCT_4:14
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m))) by A8, PBOOLE:158 ;
hence NPP (Comput ((P +* (stop I)),(Initialize s),(m + 1))) = NPP (Comput ((P +* (I ';' J)),(Initialize s),(m + 1))) by A3, A7, A6, A4, NAT_1:13, SCMPDS_4:15; :: thesis: verum

end;

A12: Comput ((P +* (I ';' J)),(Initialize s),0) = Initialize s by EXTPRO_1:3;
A13: Comput ((P +* (stop I)),(Initialize s),0) = Initialize s by EXTPRO_1:3;
A15: S₁[ 0 ] by A13, A12;
A16: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A15, A2);
assume k <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
hence NPP (Comput ((P +* (stop I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k)) by A16; :: thesis: verum