+*)
+let rec convert_machines ugraph =
+ function
+ [] -> true,ugraph
+ | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
+ let (b,ugraph) as res =
+ aux2 test_equality_only
+ (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
+ in
+ if b then
+ let problems =
+ try
+ Some
+ (List.combine
+ (List.map
+ (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+ s1)
+ (List.map
+ (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+ s2)
+ @ tl)
+ with
+ Invalid_argument _ -> None
+ in
+ match problems with
+ None -> false,ugraph
+ | Some problems -> convert_machines ugraph problems
+ else
+ res
+in
+ convert_machines ugraph
+ [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
+ R.reduce ~delta:true ~subst context (0,[],[],t2,[])]