Step 3: T2-Rules

The NOT-Operator is pushed down the syntax tree and some other reductions are processed. All rules are listed in Table 8.





Rule Operator replaced by



20 (x) x
21 (x y) x y
22 (x y) x y
23 (x y) x˙∨y
24 (x∨˙y) x y
25 (x [,,<,>, =,=] y) x [>,<,,,=, =] y
26 atleast(k)i xi , (k 1) atmost(k - 1)i xi
26a atleast(0)i xi atleast(1)i xi
27 atmost(k)i xi atleast(k + 1)i xi
28 exactly(k)i xi , (k 1) atmost(k - 1)i xi   atleast(k + 2)i xi
29 x = 1 (1 = x,x = 0, 0 = x) x
29a x = 0 (0 = x,x = 1, 1 = x) x
30 x = y x y
31 x y (x y)   (x y)
32 x = y x < y x > y
33 x∨˙y (x y)   (x y))
34 exactly(k)i xi , (k 1) ixi = k
35 atmost(k)i xi , (k 1) ixi k
35a atmost(0)i xi atleast(0)i xi
36 atleast(k)i xi , (k 2) ixi k




Table 8: T2-Rules