relation.refl_trans_gen

refl_trans_gen r: reflexive transitive closure of r

relation.refl_gen

refl_gen r: reflexive closure of r

relation.trans_gen

trans_gen r: transitive closure of r