5通りにする

X = T はどんなに頑張ってもだめだったので、 X = T - 1 = T^2 を試してみた。
すなわち

match t1, t2, t3, t4, t5, t6, t7 with
| Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, Node s1 s2 => f_2 s1 s2
| s1, s2, s3, s4, s5, s6, s7 =>
  Node s1 (Node s2 (Node s3 (Node s4 (Node s5 (Node s6 s7))))) 
end

の場合を考えると
Y = T^7 - X = T^7 - T + 1
T - Y = (1 + T + T^2 + T^3 + T^4 + T^5 + T^7) - Y
T - Y = T + T^2 + T^3 + T^4 + T^5 + T
なので
f_2 : T - 1 \to T + T^2 + T^3 + T^4 + T^5 + T
となる。

T - 1 = T^2
T - 1 = (1 + T^2)^2
T - 1 = 1 + T^2 + T^2 + T^4
T - 1 = 1 + T^2 + (T + T^2 + T^3 + T^5) + T^4
T - 1 = T + T^2 + T^3 + T^4 + T^5 + T
でできあがり。これを圧縮すると5通りの場合わけになる。