let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
NPP (Comput ((P +* I),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
NPP (Comput ((P +* I),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))
let I, J be Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies for k being Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
NPP (Comput ((P +* I),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k)) )
set s1 = Initialize s;
set s2 = Initialize s;
set I1 = Initialize I;
set I2 = Initialize (I ';' J);
A1: ProgramPart I = I by RELAT_1:209;
defpred S₁[ Nat] means ( $1 <= pseudo-LifeSpan (s,P,I) implies NPP (Comput ((P +* I),(Initialize s),$1)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),$1)) );
A2: dom (P +* I) = NAT by PARTFUN1:def 4;
A3: dom (P +* (I ';' J)) = NAT by PARTFUN1:def 4;
assume A4: I is_pseudo-closed_on s,P ; :: thesis: for k being Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
NPP (Comput ((P +* I),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k))

A5: now

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

proof

A7: Comput ((P +* (I ';' J)),(Initialize s),(k + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),k)))),(Comput ((P +* (I ';' J)),(Initialize s),k))) ;
A8: Comput ((P +* I),(Initialize s),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k)))),(Comput ((P +* I),(Initialize s),k))) ;
A9: dom I c= dom (I ';' J) by SCMFSA6A:56;
A10: k + 0 < k + 1 by XREAL_1:8;
assume A11: k + 1 <= pseudo-LifeSpan (s,P,I) ; :: thesis: NPP (Comput ((P +* I),(Initialize s),(k + 1))) = NPP (Comput ((P +* (I ';' J)),(Initialize s),(k + 1)))
then A12: k < pseudo-LifeSpan (s,P,I) by A10, XXREAL_0:2;
then A13: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A4, Th31, A1;
A14: I c= P +* I by FUNCT_4:26;
A15: I ';' J c= P +* (I ';' J) by FUNCT_4:26;
A16: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A2, PARTFUN1:def 8
.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A13, GRFUNC_1:8, A14 ;
then I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A4, A12, Th31, A1;
then CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (I ';' J) . (IC (Comput ((P +* I),(Initialize s),k))) by A13, A16, SCMFSA6A:54
.= (P +* (I ';' J)) . (IC (Comput ((P +* I),(Initialize s),k))) by A13, A9, GRFUNC_1:8, A15
.= (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(Initialize s),k))) by A6, A11, A10, COMPOS_1:230, XXREAL_0:2
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),k))) by A3, PARTFUN1:def 8 ;
hence NPP (Comput ((P +* I),(Initialize s),(k + 1))) = NPP (Comput ((P +* (I ';' J)),(Initialize s),(k + 1))) by A6, A11, A10, A8, A7, AMISTD_2:def 20, XXREAL_0:2; :: thesis: verum

end;

end;

A17: S₁[ 0 ]

proof

assume 0 <= pseudo-LifeSpan (s,P,I) ; :: thesis: NPP (Comput ((P +* I),(Initialize s),0)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),0))
NPP (Comput ((P +* I),(Initialize s),0)) = NPP (Initialize s) by EXTPRO_1:3;
hence NPP (Comput ((P +* I),(Initialize s),0)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),0)) by EXTPRO_1:3; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A17, A5); :: thesis: verum