Here I'm adopting the notation used on Rui's Site. So what we want to prove is that:

P(ABB) + P(A) = K(x,y,z)P(AB)P(B)

Our setup looks like this in terms of snakes:

It can be verified through algebra that this equation may be rewritten as
M(A)z^(nb/2 + 2)x^(hb/2)y^(wb/2) + M(ABB) = (x^2+y^2+z^2)M(AB)M(B).

Note we may interpret the coefficient next to the M(A) term as the border of B with an additional z^4 term.

Case 1: Decomposition a matching of ABB with y^2 term in U.

This case takes any matching of ABB which has a y^2 term in the second unit to a matching of AB, B, and a lone y^2 term. In polynomials, this corresponds to the matchings y^2*M(AB)M(B).

Case 2: Decomposition of matchings of ABB with a x^2 term in U.

This case takes any matching of ABB which has a x^2 term in the second unit to a matching of AB, B, and a lone x^2 term. This corresponds in polynomials to the matchings of x^2*M(AB)M(B)

Case 3: Decomposition of terms in which U is connected to AB or B in ABB.

Our initial decomposition involves removing the z^2 term that connects U to AB or B. From here, we separate the matchings into separate classes depending on the edges used on the ends of AB and B.
Now on the RHS, we have used up all the (x^2+y^2)M(AB)M(B) terms. So the remaining terms are z^2*M(AB)M(B). We put these matchings into the following classes:



Now we look at our initial decomposition in Case 3 and the RHS and cancel to get the following:

From here, the correspondence we establish between the LHS and RHS is based on whether the matching of AB has a common cut with B.

On the LHS, we can always find a common cut between AB and B along the B parts of the graphs.


The worst case is if the B parts are a matching with no common cut. In this case, we can still cut along the square that connects A to B. Supposing that there is a connection between the lower B part and the square bridging A and B, then this means that the matchings of B must actually contain a common cut in the somewhere in the interior since there is only one pair of matchings in which a snake has no common cut.

To take the LHS to the RHS, we rotate the disconnected B unit by 180 degrees since it is symmetric. From here, we make a cut to exchange x and the y^2 ends of the B snakes. This corresponds on the RHS to all matchings of AB and B that have common cuts. This is illustrated in the top case of the picture below.

The only case where the RHS does NOT have a common cut is if we have the matching on the bottom case. In this case we get a matching of A, and the border of B which is exactly x^(hb/2)y^(wb/2)z^((nb-4)/2). The extra z^4 term represents the the lone z^2 term and another z^2 used in extending the bottom matching with no common cut to the square between A and B.

Finally, here's an example of the tilings matching up for the 169 case: A big picture.
Note it does not follow the cuts of the proof. It was just used in as an example to see how to make a proof.