:: deftheorem defines -derivables FOMODEL4:def 6 :
for S being Language
for D being RuleSet of S
for m being Nat holds (m,D) -derivables = iter ((OneStep D),m);