:: deftheorem Def62 defines -ranked FOMODEL4:def 62 :
for m being Nat
for S being Language
for D being RuleSet of S holds
( ( m = 0 implies ( D is m -ranked iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D ) ) ) & ( m = 1 implies ( D is m -ranked iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) ) ) & ( m = 2 implies ( D is m -ranked iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) & ( not m = 0 & not m = 1 & not m = 2 implies ( D is m -ranked iff D = {} ) ) );