let trivial_is_implied a1 a2 = TimerSubset.start (); let n1 = Array.length a1 in let n2 = Array.length a2 in let s = if n1 > n2 then false else let i1 = ref 0 in let i2 = ref 0 in while !i1 < n1 && !i2 < n2 do let c = Atom.trivial_is_implied a1.(!i1) a2.(!i2) in if c = 0 then (incr i1; incr i2) else if c < 0 then i2 := n2 else incr i2 done; !i1 = n1 in TimerSubset.pause (); s