YES
0 QTRS
↳1 QTRSRRRProof (⇔, 64 ms)
↳2 QTRS
↳3 RisEmptyProof (⇔, 0 ms)
↳4 YES
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
sum1 > +2 > [s1, nil] > 0
[cons2, prod1] > *2 > +2 > [s1, nil] > 0
+2: [1,2]
0: multiset
s1: multiset
*2: [1,2]
sum1: multiset
nil: multiset
cons2: multiset
prod1: multiset
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))