Project Euler 106: Necessary and sufficient conditions Problem Statement

Let S(A) represent the sum of elements in set A of size n. We shall call it a special sum set if for any two non-empty disjoint subsets, B and C, the following properties are true:
  
  
*
  
*S(B) ≠ S(C); that is, sums of subsets cannot be equal.
  
*If B contains more elements than C then S(B) > S(C).
  
  
  For this problem we shall assume that a given set contains n strictly increasing elements and it already satisfies the second rule.
Surprisingly, out of the 25 possible subset pairs that can be obtained from a set for which n = 4, only 1 of these pairs need to be tested for equality (first rule). Similarly, when n = 7, only 70 out of the 966 subset pairs need to be tested.
For n = 12, how many of the 261625 subset pairs that can be obtained need to be tested for equality?

What I've already done:
Sets are represented as lists sorted in ascending order. A list $X$ of length $n$ is addressed as $X[0],\ldots,X[n-1]$. Set cardinality is denoted by $|\cdot|$.
As given, consider $A$ to be a set of size $n$, and $B$ and $C$ to be disjoint nonempty subsets of $A$. W.l.o.g. consider last($C$) $>$ last($B$), because Rules 1 and 2 are satisfied by ($B$,$C$) iff they are satisfied by ($C$,$B$).
Case 1: $|B| > |C|$. Since $A$ already satisfies the second rule (in the problem statement), $S(B) > S(C) \Rightarrow S(B)\neq S(C)$. Hence, testing is not required for such (unordered) pairs ($B$,$C$).
Case 2: $|B| = |C| = x \leq n/2$. Consider the set $B' = \{\text{index of }B[i]\text{ in }A: 0\leq i < x\}$ and $C'$ defined similarly for $C$. Note that we must have last($B'$) < last($C'$) because $A$ was sorted ascending.
Claim (part of Case 2): If $B'[i] < C'[i] \;\forall\; 0\leq i < x$, then Rule 1 is satisfied.
This claim is easily proved.
Question:
The above claim can be proved in an "if .. then .." form. However, I assumed that it is actually true in the form " .. iff ..", wrote the code and voila! The answer matches! (I checked by hand for cases $n=7$, $n=4$; there will also be binomial coefficients, see the code below for details).
However, I am unable to come up with a proof for the " .. if .. " statement.  In other words, (why) does the (unordered) pair require checking iff $B'[i] < C'[i]\; \forall\; 0\leq i < x$?
I intuitively feel that there might be some way to use Rule 2 repeatedly to derive some additional constraints, i.e., there might be more pairs which need not be checked apart from the ones satisfying our criteria.
Code (Python 2.7.10)
from scipy.misc import comb

def check_not_reqd(b,c):
    x = True
    for (bn,cn) in zip(b,c):
        x = x and (bn < cn)
    return x

def recurse(b, length, depth, start, end):
    count = 0
    if depth == 0:
        for b[length-1] in range(start, end):
            c = [x for x in range(2*length) if x not in b]
            if (not check_not_reqd(b,c)):
                count = count + 1
        return count
    else:
        for b[length-1-depth] in range(start, end):
            count = count + recurse(b, length, depth-1, b[length-1-depth]+1, end+1)
        return count

print(sum([comb(12,t)*recurse([0 for s in range(t/2)],t/2,t/2-1,0,t/2) for t in [4,6,8,10,12]]))

If the recurse function seems a bit difficult to comprehend, here is an "unfurled" version for t=8
tot = 8
count = 0
b, c = [0,0,0,0], [0,0,0,7]
start = 0
end = tot/2
for b[0] in range(start,end):
    for b[1] in range(b[0]+1,end+1):
        for b[2] in range(b[1]+1,end+2):
            for b[3] in range(b[2]+1,end+3):
                c = [x for x in range(0, tot) if x not in b]
                if(not check_not_reqd(b,c)):
                    count = count + 1
print(count)
# count == recurse for t = 8

 A: Of course, you don't need to check the pair if either $|B| < |C|$ or indices of $C$ dominate the indices of $B$. The question is, why we have to check all the other pairs of sets. To resolve that problem, for a given pair $(B',C')$ we will construct a set $A$ such that $S(B) = S(C)$ which happens only for these two sets.
We assume that $\operatorname{last}(B') < \operatorname{last}(C')$.
There are four things we need to address:


*

*The numbers ensure property $(2)$.

*The numbers have actually the given indices in $A$, that is $a_i < a_{i+1}$.

*All the indices of $B'$ and $C'$ have to be used, and nothing more.

*The indices of $B'$ and $C'$ cannot be mixed.


The main idea is to use $$a_i = (n^n)^{n^3} + (n^n)^{n^2}\cdot p_i + \sum_{0\leq k < n} (n^n)^{k}\cdot w_{i,k},$$ where the first component takes care of $(1)$, $p_i$ takes care of $(2)$ and $w_{i,k}$'s handle $(3)$ and $(4)$.
Part I: $p_i$
Let $\alpha = S(B')-S(C')$. If $\alpha \geq 0$ then we set
\begin{align}
p_i &= n^3 + i & \text{ for }i < \operatorname{last}(C') \\
p_i &= n^3 + i + |\alpha| & \text{ for }i \geq \operatorname{last}(C')
\end{align}
Otherwise, let $\beta' = \max\{ i \mid B'[i] > C'[i]\}$ and $\beta  = B'[\beta']$ and use
\begin{align}
p_i &= n^3 + i & \text{ for }i < \beta \\
p_i &= n^3 + i + |\alpha| & \text{ for }i \geq \beta
\end{align}
Note, that $p_i < p_{i+1}$ and $\sum_{i\in B'} p_i = \sum_{i \in C'}p_i$.
Part II: $w_{i,k}$
Set
\begin{align}
w_{i,i} &= |B'|      &&\text{ for any } i \\
w_{i,k} &= 1         &&\text{ if } (i,k) \in B'\times C' \cup C'\times B' \\
w_{i,k} &= 0         &&\text{ otherwise } \\
\end{align}
and observe that to have equal sums


*

*you can't take any element of $A \setminus (B \cup C)$, because of $w_{i,i}$ cannot be matched by any other element,

*if you take any element of $B'$, then to match its $w_{i,i}$ only the elements of $C'$ can be used,

*there are only $|B'| = |C'|$ elements that could match $w_{i,i}$ so all the elements of $C'$ have to be used.


Thus, the only pairs with equal sums are $(\varnothing,\varnothing)$ and $(B',C')$.
I hope this helps $\ddot\smile$
