:: deftheorem defines is_pseudo-closed_on SCMFSA8A:def 2 :
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA holds
( I is_pseudo-closed_on s,P iff ex k being Nat st
( IC (Comput ((P +* I),(Initialize s),k)) = card I & ( for n being Nat st n < k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) ) );