let s be State of SCM+FSA ; :: thesis: for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ) holds
k < pseudo-LifeSpan s,P
let P be initial FinPartState of SCM+FSA ; :: thesis: ( P is_pseudo-closed_on s implies for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ) holds
k < pseudo-LifeSpan s,P )
assume A1: P is_pseudo-closed_on s ; :: thesis: for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ) holds
k < pseudo-LifeSpan s,P
let k be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n <= k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ) implies k < pseudo-LifeSpan s,P )
assume A2: for n being Element of NAT st n <= k holds
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P ; :: thesis: k < pseudo-LifeSpan s,P
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,P)) = insloc (card (ProgramPart P)) by A1, SCMFSA8A:def 5;
then A3: not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,P)) in dom [(ProgramPart P)] by SCMFSA6A:15;
assume pseudo-LifeSpan s,P <= k ; :: thesis: contradiction
hence contradiction by A2, A3, AMI_1:106; :: thesis: verum