+
+ let rec lpo s t =
+ match s,t with
+ | Terms.Var i, Terms.Var j when i = j ->
+ XEQ
+ | Terms.Var _, Terms.Var _ ->
+ XINCOMPARABLE
+ | Terms.Var _, _ ->
+ (match lpo t s with
+ | XGT -> XLT
+ | XLT -> XGT
+ | o -> o)
+ | _, Terms.Var i ->
+ if (List.mem i (Terms.vars_of_term s)) then XGT
+ else XINCOMPARABLE
+ | Terms.Leaf a1, Terms.Leaf a2 ->
+ let cmp = B.compare a1 a2 in
+ if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+ | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
+ (match lpo hd1 hd2 with
+ | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+ else XINCOMPARABLE
+ | XLT -> if List.for_all (fun x -> lpo s x = XLT) tl2 then XLT
+ else XINCOMPARABLE
+ | XEQ -> List.fold_left2
+ (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+ XEQ tl1 tl2
+ | XINCOMPARABLE -> XINCOMPARABLE
+ | _ -> assert false)
+ | _ -> assert false
+
+ ;;
+