kdrag.theories.set.CountInter

kdrag.theories.set.CountInter(seq: ArrayRef) → ArrayRef

Countable intersection of a sequence of sets Int -> A -> Bool.

>>> ISet = Set(smt.IntSort())
>>> i,j,k = smt.Ints("i j k")
>>> kd.prove(smt.ForAll([k], smt.Not(CountInter(smt.Lambda([i], smt.Lambda([j], i == j)))[k])))
|= ForAll(k,
       Not(Lambda(x!...,
                  ForAll(i!...,
                         Lambda(i, Lambda(j, i == j))[i!...][x!...]))[k]))

Parameters:

seq (ArrayRef)

Return type:

ArrayRef