add first cut at formal proof for PartitionedXOR