YES
0 QTRS
↳1 QTRSRRRProof (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 3 ms)
↳6 QTRS
↳7 RisEmptyProof (⇔, 0 ms)
↳8 YES
and(x, false) → false
and(x, not(false)) → x
not(not(x)) → x
implies(false, y) → not(false)
implies(x, false) → not(x)
implies(not(x), not(y)) → implies(y, and(x, y))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(and(x1, x2)) = 2·x1 + x2
POL(false) = 2
POL(implies(x1, x2)) = 2 + 2·x1 + 2·x2
POL(not(x1)) = 2·x1
and(x, not(false)) → x
implies(false, y) → not(false)
implies(x, false) → not(x)
and(x, false) → false
not(not(x)) → x
implies(not(x), not(y)) → implies(y, and(x, y))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(and(x1, x2)) = x1 + x2
POL(false) = 1
POL(implies(x1, x2)) = x1 + 2·x2
POL(not(x1)) = 1 + 2·x1
not(not(x)) → x
implies(not(x), not(y)) → implies(y, and(x, y))
and(x, false) → false
false > and2
false=1
and_2=0
and(x, false) → false