let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being initial Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) <> halt SCM+FSA )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being initial Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) <> halt SCM+FSA )
let I be initial Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) <> halt SCM+FSA ) )
set k = pseudo-LifeSpan (s,P,I);
assume A1: I is_pseudo-closed_on s,P ; :: thesis: for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) <> halt SCM+FSA )
then A2: IC (Comput ((P +* (ProgramPart I)),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = card (ProgramPart I) by Def5;

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan (s,P,I) implies ( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & not CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) = halt SCM+FSA ) )
assume A3: n < pseudo-LifeSpan (s,P,I) ; :: thesis: ( IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I & not CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) = halt SCM+FSA )
hence IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom I by A1, Def5; :: thesis: not CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) = halt SCM+FSA
then A4: IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) in dom (ProgramPart I) by COMPOS_1:16;
assume CurInstr ((P +* (ProgramPart I)),(Comput ((P +* (ProgramPart I)),(Initialize s),n))) = halt SCM+FSA ; :: thesis: contradiction
then IC (Comput ((P +* (ProgramPart I)),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = IC (Comput ((P +* (ProgramPart I)),(Initialize s),n)) by A3, EXTPRO_1:6;
hence contradiction by A2, A4; :: thesis: verum

end;