(* returns true iff r1,r2 create a critical pair *)
let critical_pair (r1:rule) (r2:rule) =
  let (l,_) = r1 in
  let (g,_) = r2 in
  let to_compare =
    if (r1 <> r2)
    then List.tl (fun_subterms (rename_term l))
    else fun_subterms (rename_term l)
  in
  List.exists (fun p ->
    match unification p g with
    | Some _ -> printf "%s et %s sont unifiables\n"
      (Pprint.pprint_term p)
      (Pprint.pprint_term g); true
    | None -> false
  ) to_compare

(* returns true iff there exists r1 r2 that create a critical pair *)
let critical system =
  List.exists (fun r1 ->
    List.exists (fun r2 ->
      if critical_pair r1 r2
      then (
        printf "paire critique: %s\n%s\n"
        (Pprint.pprint_rule r1)
        (Pprint.pprint_rule r2); true
      ) else false
    ) system
  ) system