:: deftheorem defines dominated_by_0 CATALAN2:def 1 :
for p being XFinSequence of NAT holds
( p is dominated_by_0 iff ( rng p c= {0,1} & ( for k being Nat st k <= dom p holds
2 * (Sum (p | k)) <= k ) ) );