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