let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Nat st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for n being Nat st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
let I be Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies for n being Nat st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* 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 Nat st n < pseudo-LifeSpan (s,P,I) holds
( IC (Comput ((P +* I),(Initialize s),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) <> halt SCM+FSA )
then A2: IC (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = card I by Def3;
hereby :: thesis: verum
let n be Nat; :: thesis: ( n < pseudo-LifeSpan (s,P,I) implies ( IC (Comput ((P +* I),(Initialize s),n)) in dom I & not CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ) )
assume A3: n < pseudo-LifeSpan (s,P,I) ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),n)) in dom I & not CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA )
hence A4: IC (Comput ((P +* I),(Initialize s),n)) in dom I by A1, Def3; :: thesis: not CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA
assume CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ; :: thesis: contradiction
then IC (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = IC (Comput ((P +* I),(Initialize s),n)) by A3, EXTPRO_1:5;
hence contradiction by A2, A4; :: thesis: verum
end;