let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being initial Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) holds
k < pseudo-LifeSpan (s,P,I)
let s be State of SCM+FSA; :: thesis: for I being initial Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) holds
k < pseudo-LifeSpan (s,P,I)
let I be initial Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) holds
k < pseudo-LifeSpan (s,P,I) )
assume I is_pseudo-closed_on s,P ; :: thesis: for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) holds
k < pseudo-LifeSpan (s,P,I)
then IC (Comput ((P +* (ProgramPart I)),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = card (ProgramPart I) by SCMFSA8A:def 5;
then A1: not IC (Comput ((P +* (ProgramPart I)),(Initialize s),(pseudo-LifeSpan (s,P,I)))) in dom (ProgramPart I) ;
let k be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ) implies k < pseudo-LifeSpan (s,P,I) )
assume A2: for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I ; :: thesis: k < pseudo-LifeSpan (s,P,I)
assume pseudo-LifeSpan (s,P,I) <= k ; :: thesis: contradiction
hence contradiction by A2, A1, COMPOS_1:16; :: thesis: verum