24.9 Test Two-Element Subsets
The species ℘[2] of two-element subsets is defined by E2 ⋅E where E is the species
of sets and E2 the species of two-element sets.
640⟨test TwoElement Subset 640⟩≡ (626)
testTwoElementSubset(): () == check(
Times(RestrictedSpecies(SetSpecies, 2), SetSpecies),
[0,0,1,3,6,10,15,21,28,36,45,55, 66,78,91,105,120,136,153,171,190],
[0,0,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],
[
0,
0,
(inv 2)*x(1,2)+(inv 2)*x(2,1),
(inv 2)*x(1,3)+(inv 2)*x(1,1)*x(2,1),
(inv 4)*x(1,4)+(inv 2)*x(1,2)*x(2,1)+(inv 4)*x(2,2),
(inv 12)*x(1,5)+(inv 3)*x(1,3)*x(2,1)+(inv 6)*x(1,2)*x(3,1)
+(inv 4)*x(1,1)*x(2,2)+(inv 6)*x(2,1)*x(3,1),
(inv 48)*x(1,6)+(7/48)*x(1,4)*x(2,1)+(inv 6)*x(1,3)*x(3,1)
+(3/16)*x(1,2)*x(2,2)+(inv 8)*x(1,2)*x(4,1)
+(inv 6)*x(1,1)*x(2,1)*x(3,1)+(inv 16)*x(2,3)
+(inv 8)*x(2,1)*x(4,1)
]
);
Uses RestrictedSpecies 127, SetSpecies 117, and Times 175a.