kdrag.theories.set.PowerSet

kdrag.theories.set.PowerSet(A: ArrayRef) ArrayRef

Power set of A : Set( Set(T) ) >>> IntSet = Set(smt.IntSort()) >>> A = Singleton(smt.IntVal(3)) >>> P = PowerSet(A) >>> kd.prove(member(IntSet.empty, P)) |= Lambda(c!…, subset(c!…, Store(K(Int, False), 3, True)))[K(Int,

False)]

Parameters:

A (ArrayRef)

Return type:

ArrayRef