641a⟨test Constructor 641a⟩≡   (626)  641b ⊳
testPlus1(): () == check(
    Plus(SingletonSpecies, SingletonSpecies),
    [0, 2, 0, 0, 0],
    [0, 2, 0, 0, 0],
    [0, 2, 0, 0, 0]
);

Uses Plus 166a and SingletonSpecies 84.

641b⟨test Constructor 641a⟩+≡   (626)  ⊲641a  642a ⊳
testPlus2(): () == check(
    Plus(EmptySetSpecies, SingletonSpecies),
    [1, 1, 0, 0, 0],
    [1, 1, 0, 0, 0],
    [1, x(1),0,0,0,0]
);

Uses EmptySetSpecies 83, Plus 166a, and SingletonSpecies 84.

642a⟨test Constructor 641a⟩+≡   (626)  ⊲641b  642b ⊳
testTimes1(): () == check(
    Times(SingletonSpecies, SingletonSpecies),
    [0, 0, 2, 0, 0, 0],
    [0, 0, 1, 0, 0, 0],
    [0,0,y(2),0,0,0]
);

Uses SingletonSpecies 84 and Times 175a.

642b⟨test Constructor 641a⟩+≡   (626)  ⊲642a
testPlusTimes1(): () == {
        macro {
                E == EmptySetSpecies;
                X == SingletonSpecies;
                + == Plus;
                * == Times;
        }
        check(
            (E+X)*(E+X),
            [1, 2, 2, 0, 0, 0],
            [1, 2, 1, 0, 0, 0],
            [1, 2, 1, 0, 0, 0]
        );
}

Uses EmptySetSpecies 83, Plus 166a, SingletonSpecies 84, and Times 175a.