fun consapp x (h::t) rest = (x::h) :: consapp x t rest | consapp _ [] rest = rest ; fun subs (h::t) = let val l = subs t in consapp h l l end | subs [] = [[]] ; exception GCEx val cex = ref id ; fun gtest p = let val pp = p comp p in if pp = [] then true else let val cp = conv p val pcp = p comp cp val cpp = cp comp p val lhs = pcp int cpp val rhs1 = ((p comp (diff top pp)) int cp) comp top val cpcp = conv pp val pcint = pp int cpcp val rhs2 = pcint comp pcint val lrd = diff (diff lhs rhs1) rhs2 in if lrd = [] then true else (cex := p ; raise GCEx) end end ;