Pattern : curr =
2 3 Ǎ : Ǎ(2, 3, curr) -> (2).Ǎ(3, curr)
2 Ǎ 3 : Ǎ(curr, 2, 3) -> curr.Ǎ(2, 3)
+ × Ǎ 2 : Ǎ(curr + alpha, curr × alpha, 2) -> (curr + alpha).Ǎ(curr × alpha, 2)
A 1 Ǎ 2 : Ǎ(A(curr), 1, 2) -> A(curr).Ǎ(1, 2)
Ǎ + : Ǎ(curr, alpha, alpha + curr) -> curr.Ǎ(alpha, curr + alpha)
Ǎ I : Ǎ(curr, alpha, I(alpha)) -> curr.Ǎ(alpha, I(alpha))
Ǎ 2 : Ǎ(curr, alpha, 2) -> curr.Ǎ(alpha, 2)
Ǎ : Ǎ(curr, alpha, alpha) -> curr.Ǎ(alpha, alpha)