for R being Relation st ( for a, b being object holds not a,b are_critical_wrt R ) holds
R is locally-confluent