let s be State of ; :: thesis: for P being initial FinPartState of 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 ; :: 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 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
then IC (Computation (s +* (P +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,P)) = insloc (card (ProgramPart P)) by SCMFSA8A:def 5;
then A1: not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,P)) in dom [(ProgramPart P)] by SCMFSA6A:15;
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
assume pseudo-LifeSpan s,P <= k ; :: thesis: contradiction
hence contradiction by A2, A1, AMI_1:106; :: thesis: verum