let s be State of ; :: thesis: for P being initial FinPartState of st P is_pseudo-closed_on s holds
for n being Element of NAT st n < pseudo-LifeSpan s,P holds
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P & CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA )
let P be initial FinPartState of ; :: thesis: ( P is_pseudo-closed_on s implies for n being Element of NAT st n < pseudo-LifeSpan s,P holds
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P & CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA ) )
set k = pseudo-LifeSpan s,P;
assume A1: P is_pseudo-closed_on s ; :: thesis: for n being Element of NAT st n < pseudo-LifeSpan s,P holds
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P & CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA )
then A2: IC (Computation (s +* (P +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,P)) = insloc (card (ProgramPart P)) by Def5;

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan s,P implies ( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P & not CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) = halt SCM+FSA ) )
assume A3: n < pseudo-LifeSpan s,P ; :: thesis: ( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P & not CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) = halt SCM+FSA )
hence IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P by A1, Def5; :: thesis: not CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) = halt SCM+FSA
then A4: IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom [(ProgramPart P)] by AMI_1:106;
assume CurInstr (Computation (s +* (P +* (Start-At (insloc 0 )))),n) = halt SCM+FSA ; :: thesis: contradiction
then IC (Computation (s +* (P +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,P)) = IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) by A3, AMI_1:52;
hence contradiction by A2, A4, SCMFSA6A:15; :: thesis: verum

end;