+ | ((Terms.Node (Terms.Leaf op1::t) as x),y)
+ | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+ let rec term_leaves = function
+ | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
+ | Terms.Leaf x -> [x]
+ | _ -> []
+ in
+ if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then
+ dependencies op tl (op1::acc)
+ else
+ dependencies op tl acc