kdrag.theories.set.FamilyUnion

kdrag.theories.set.FamilyUnion(family: ArrayRef) → ArrayRef

Countable union 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], FamilyUnion(smt.Lambda([i], smt.Lambda([j], i == j)))[k]))
    |= ForAll(k,
       Lambda(x!...,
              Exists(i!...,
                     Lambda(i, Lambda(j, i == j))[i!...][x!...]))[k])

Parameters:

family (ArrayRef)

Return type:

ArrayRef