:: deftheorem defines is-accepted-by MODELC_3:def 39 :
for W being non empty set
for B being BuchiAutomaton over W
for w being Element of Inf_seq W holds
( w is-accepted-by B iff ex run being sequence of the carrier of B st
( run . 0 in the InitS of B & ( for i being Nat holds
( [[(run . i),((CastSeq (w,W)) . i)],(run . (i + 1))] in the Tran of B & ( for FSet being set st FSet in the FinalS of B holds
{ k where k is Element of NAT : run . k in FSet } is infinite set ) ) ) ) );