- match t1,t2 with
- C.Meta (_, _), C.Meta (_,_) -> Incomparable
- | C.Meta (_,_) as t1,t2 when TermSet.mem t1 (metas_of_term t2)
- -> Lt
- | t1, (C.Meta (_,_) as t2) when TermSet.mem t2 (metas_of_term t1)
- -> Gt
- | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
- (match lex arg1 arg2 with
- | Lt when (check Gt t2 arg1) -> Lt
- | Gt when (check Gt t1 arg2) -> Gt
- | _ -> Incomparable )
- | C.Appl (h1::arg1),C.Appl (h2::arg2) ->
- (match sig_order h1 h2 with
- | Lt when (check Gt t2 arg1) -> Lt
- | Gt when (check Gt t1 arg2) -> Gt
- | _ -> Incomparable )
- | C.Appl (h1::arg1), t2 when atomic t2 ->
- (match sig_order h1 t2 with
- | Lt when (check Gt t2 arg1) -> Lt
- | Gt -> Gt
- | _ -> Incomparable )
- | t1 , C.Appl (h2::arg2) when atomic t1 ->
- (match sig_order t1 h2 with
- | Lt -> Lt
- | Gt when (check Gt t1 arg2) -> Gt
- | _ -> Incomparable )
- | C.Appl [] , _ -> assert false
- | _ , C.Appl [] -> assert false
- | _,_ -> Incomparable
-
-and lex l1 l2 =
+ let first_trie =
+ match t1,t2 with
+ C.Meta (_, _), C.Meta (_,_) -> false
+ | C.Meta (_,_) , t2 -> TermSet.mem t1 (metas_of_term t2)
+ | t1, C.Meta (_,_) -> false
+ | C.Appl [h1;a1],C.Appl [h2;a2] when h1=h2 ->
+ rpo_lt a1 a2
+ | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
+ if lex_lt arg1 arg2 then
+ check_lt arg1 t2
+ else false
+ | C.Appl (h1::arg1),C.Appl (h2::arg2) ->
+ (match sig_order h1 h2 with
+ | Lt -> check_lt arg1 t2
+ | _ -> false)
+ | C.Appl (h1::arg1), t2 when atomic t2 ->
+ (match sig_order h1 t2 with
+ | Lt -> check_lt arg1 t2
+ | _ -> false)
+ | t1 , C.Appl (h2::arg2) when atomic t1 ->
+ (match sig_order t1 h2 with
+ | Lt -> true
+ | _ -> false )
+ | C.Appl [] , _ -> assert false
+ | _ , C.Appl [] -> assert false
+ | t1, t2 when (atomic t1 && atomic t2 && t1<>t2) ->
+ (match sig_order t1 t2 with
+ | Lt -> true
+ | _ -> false)
+ | _,_ -> false
+ in
+ if first_trie then true else
+ match t2 with
+ C.Appl (_::args) ->
+ List.exists (fun a -> t1 = a || rpo_lt t1 a) args
+ | _ -> false
+
+and lex_lt l1 l2 =