let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being paraclosed Program of SCM+FSA st P +* I halts_on s & Directed I c= P & Start-At (0,SCM+FSA) c= s holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being paraclosed Program of SCM+FSA st P +* I halts_on s & Directed I c= P & Start-At (0,SCM+FSA) c= s holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
set A = NAT ;
let I be paraclosed Program of SCM+FSA; :: thesis: ( P +* I halts_on s & Directed I c= P & Start-At (0,SCM+FSA) c= s implies DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) )
assume that
A1: P +* I halts_on s and
A3: Directed I c= P and
A4: Start-At (0,SCM+FSA) c= s ; :: thesis: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
set sISA0 = s +* (Start-At (0,SCM+FSA));
A5: s +* (Start-At (0,SCM+FSA)) = s by A4, FUNCT_4:104;
set s1 = s +* (Start-At (0,SCM+FSA));
A6: I c= P +* I by FUNCT_4:26;
set s2 = s +* (Start-At (0,SCM+FSA));
set IAt = Initialize I;
A8: s +* (Start-At (0,SCM+FSA)) = s by A4, FUNCT_4:104;
set m = LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))));
set l1 = IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))));
A9: Start-At (0,SCM+FSA) c= s +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
B9: Start-At (0,SCM+FSA) c= s +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
A12: IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) in dom I by Def2, B9, A6;

now

let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))) implies NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput (P,s,k)) )
defpred S₁[ Nat] means ( $1 <= k implies NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),$1)) = NPP (Comput (P,s,$1)) );
assume A14: k <= LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))) ; :: thesis: NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput (P,s,k))
A15: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

A16: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
A17: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A18: ( n <= k implies NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n)) = NPP (Comput (P,s,n)) ) ; :: thesis: S₁[n + 1]
A19: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:4
.= Exec ((CurInstr (P,(Comput (P,s,n)))),(Comput (P,s,n))) ;
A20: Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),(n + 1)) = Following (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n))) by EXTPRO_1:4
.= Exec ((CurInstr (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n)))),(Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n))) ;
A21: n <= n + 1 by NAT_1:12;
assume A22: n + 1 <= k ; :: thesis: NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),(n + 1))) = NPP (Comput (P,s,(n + 1)))
then A23: IC (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n)) = IC (Comput (P,s,n)) by A18, A21, COMPOS_1:230, XXREAL_0:2;
n <= k by A22, A21, XXREAL_0:2;
then NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),n)) = NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n)) by Th36, A5, A9, A14, A6, A1, XXREAL_0:2;
then IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),n)) = IC (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n)) by COMPOS_1:230;
then A24: IC (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n)) in dom I by Def2, B9, A6;
then A25: IC (Comput (P,s,n)) in dom (Directed I) by A23, FUNCT_4:105;
A26: dom P = NAT by PARTFUN1:def 4;
A27: CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A26, PARTFUN1:def 8
.= (Directed I) . (IC (Comput (P,s,n))) by A25, A3, GRFUNC_1:8 ;
A28: dom ((P +* I) +* (I ';' I)) = NAT by PARTFUN1:def 4;
CurInstr (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n))) = ((P +* I) +* (I ';' I)) . (IC (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n))) by A28, PARTFUN1:def 8
.= (I ';' I) . (IC (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n))) by A17, A24, FUNCT_4:14
.= (Directed I) . (IC (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),n))) by A16, A23, A25, GRFUNC_1:8 ;
hence NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),(n + 1))) = NPP (Comput (P,s,(n + 1))) by A18, A22, A21, A23, A27, A20, A19, AMISTD_2:def 20, XXREAL_0:2; :: thesis: verum

end;

( Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),0) = s +* (Start-At (0,SCM+FSA)) & Comput (P,s,0) = s ) by EXTPRO_1:3;
then A29: S₁[ 0 ] by A8;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A29, A15);
then A30: NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput (P,s,k)) ;
NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput (((P +* I) +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),k)) by A5, A14, A1, A6, Th36, B9;
hence NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput (P,s,k)) by A30; :: thesis: verum

end;

then B31: NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = NPP (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) ;
then A31: IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = IC (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) by COMPOS_1:230;
A32: dom (P +* I) = NAT by PARTFUN1:def 4;
I c= P +* I by FUNCT_4:26;
then A33: I . (IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by A12, GRFUNC_1:8
.= CurInstr ((P +* I),(Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by A32, PARTFUN1:def 8
.= halt SCM+FSA by A5, A1, EXTPRO_1:def 14 ;
IC (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) in dom I by A12, B31, COMPOS_1:230;
then IC (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) in dom (Directed I) by FUNCT_4:105;
then A34: P . (IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) = (Directed I) . (IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by A31, A3, GRFUNC_1:8
.= goto (card I) by A12, A33, FUNCT_4:112 ;
A35: dom P = NAT by PARTFUN1:def 4;
Comput (P,s,((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1)) = Following (P,(Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by EXTPRO_1:4
.= Exec ((goto (card I)),(Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by A31, A34, A35, PARTFUN1:def 8 ;
then ( ( for a being Int-Location holds (Comput (P,s,((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1))) . a = (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . a ) & ( for f being FinSeq-Location holds (Comput (P,s,((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1))) . f = (Comput (P,s,(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . f ) ) by SCMFSA_2:95;
hence DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by A5, SCMFSA6A:38; :: thesis: verum