:: deftheorem defines complete REWRITE1:def 25 :
for R being Relation holds
( R is complete iff ( R is confluent & R is strongly-normalizing ) );