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
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
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
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
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 IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I )
assume that
A1: P +* I halts_on s and
A3: Directed I c= P and
A4: Start-At (0,SCM+FSA) c= s ; :: thesis: IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
A5: I c= P +* I by FUNCT_4:26;
set sISA0 = s +* (Start-At (0,SCM+FSA));
A6: s +* (Start-At (0,SCM+FSA)) = s by A4, FUNCT_4:104;
set s2 = s +* (Start-At (0,SCM+FSA));
set IAt = Initialize I;
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)))))));
A8: Start-At (0,SCM+FSA) c= s +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
A9: I c= P +* I by FUNCT_4:26;
A10: IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) in dom I by Def2, A9, A8;
set s1 = s +* (Start-At (0,SCM+FSA));
A11: P +* (I ';' I) = P +* (I +* (I ';' I)) by SCMFSA6A:57
.= (P +* I) +* (I ';' I) by FUNCT_4:15 ;

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 +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),k)) )
defpred S₁[ Nat] means ( $1 <= k implies NPP (Comput ((P +* (I ';' I)),(s +* (Start-At (0,SCM+FSA))),$1)) = NPP (Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),$1)) );
assume A13: 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 +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),k))
A14: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

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

end;

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

end;

then B30: NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = NPP (Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) ;
then A30: IC (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) = IC (Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) by COMPOS_1:230;
A31: dom (P +* I) = NAT by PARTFUN1:def 4;
I c= P +* I by FUNCT_4:26;
then A32: 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 A10, 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 A31, PARTFUN1:def 8
.= halt SCM+FSA by A1, A6, EXTPRO_1:def 14 ;
IC (Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) in dom I by A10, B30, COMPOS_1:230;
then IC (Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) in dom (Directed I) by FUNCT_4:105;
then A33: (P +* (Directed I)) . (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 A30, FUNCT_4:14
.= goto (card I) by A10, A32, FUNCT_4:112 ;
A35: P +* (Directed I) = P by A3, FUNCT_4:104;
B36: dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by EXTPRO_1:4
.= Exec ((goto (card I)),(Comput ((P +* (Directed I)),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))))))) by B36, A30, A33, PARTFUN1:def 8 ;
hence IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I by A6, A35, SCMFSA_2:95; :: thesis: verum