Fix , a finite set of symbols. is a rewrite system if is a finite set of rewrite rules. Proposition If is fixed, there are countably many rewrite systems on .