let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st Start-At (0,SCM+FSA) c= s & I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m))
let s be State of SCM+FSA; :: thesis: for I being paraclosed Program of SCM+FSA st Start-At (0,SCM+FSA) c= s & I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m))
let I be paraclosed Program of SCM+FSA; :: thesis: ( Start-At (0,SCM+FSA) c= s & I c= P & P halts_on s implies for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m)) )
assume B1: Start-At (0,SCM+FSA) c= s ; :: thesis: ( not I c= P or not P halts_on s or for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m)) )
assume A2: I c= P ; :: thesis: ( not P halts_on s or for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m)) )
defpred S₁[ Nat] means ( $1 <= LifeSpan (P,s) implies NPP (Comput (P,s,$1)) = NPP (Comput ((P +* (loop I)),s,$1)) );
assume A3: P halts_on s ; :: thesis: for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m))
A4: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

set sI = s;
set PI = P +* (loop I);
A5: loop I c= P +* (loop I) by FUNCT_4:26;
let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A6: ( m <= LifeSpan (P,s) implies NPP (Comput (P,s,m)) = NPP (Comput ((P +* (loop I)),s,m)) ) ; :: thesis: S₁[m + 1]
A7: IC (Comput (P,s,m)) in dom I by A2, B1, SCMFSA6B:def 2;
then A8: IC (Comput (P,s,m)) in dom (loop I) by FUNCT_4:105;
A9: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PBOOLE:158;
A10: CurInstr (P,(Comput (P,s,m))) = I . (IC (Comput (P,s,m))) by A7, A9, A2, GRFUNC_1:8;
A11: Comput ((P +* (loop I)),s,(m + 1)) = Following ((P +* (loop I)),(Comput ((P +* (loop I)),s,m))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),s,m)))),(Comput ((P +* (loop I)),s,m))) ;
A12: Comput (P,s,(m + 1)) = Following (P,(Comput (P,s,m))) by EXTPRO_1:4
.= Exec ((CurInstr (P,(Comput (P,s,m)))),(Comput (P,s,m))) ;
A13: (P +* (loop I)) /. (IC (Comput ((P +* (loop I)),s,m))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),s,m))) by PBOOLE:158;
assume A14: m + 1 <= LifeSpan (P,s) ; :: thesis: NPP (Comput (P,s,(m + 1))) = NPP (Comput ((P +* (loop I)),s,(m + 1)))
then m < LifeSpan (P,s) by NAT_1:13;
then I . (IC (Comput (P,s,m))) <> halt SCM+FSA by A3, A10, EXTPRO_1:def 14;
then CurInstr (P,(Comput (P,s,m))) = (loop I) . (IC (Comput (P,s,m))) by A10, FUNCT_4:111
.= (P +* (loop I)) . (IC (Comput (P,s,m))) by A8, A5, GRFUNC_1:8
.= CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),s,m))) by A6, A14, A13, COMPOS_1:230, NAT_1:13 ;
hence NPP (Comput (P,s,(m + 1))) = NPP (Comput ((P +* (loop I)),s,(m + 1))) by A6, A14, A12, A11, AMISTD_2:def 20, NAT_1:13; :: thesis: verum

end;

A15: Comput ((P +* (loop I)),s,0) = s by EXTPRO_1:3;
Comput (P,s,0) = s by EXTPRO_1:3;
then A16: S₁[ 0 ] by A15;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A16, A4); :: thesis: verum