YES
0 QTRS
↳1 QTRSRRRProof (⇔, 74 ms)
↳2 QTRS
↳3 RisEmptyProof (⇔, 0 ms)
↳4 YES
admit(x, nil) → nil
admit(x, .(u, .(v, .(w, z)))) → cond(=(sum(x, u, v), w), .(u, .(v, .(w, admit(carry(x, u, v), z)))))
cond(true, y) → y
[admit2, w] > nil
[admit2, w] > [.2, =2, sum3, carry3] > cond2
admit2: [2,1]
nil: multiset
.2: [2,1]
w: multiset
cond2: multiset
=2: [1,2]
sum3: [3,1,2]
carry3: [3,1,2]
true: multiset
admit(x, nil) → nil
admit(x, .(u, .(v, .(w, z)))) → cond(=(sum(x, u, v), w), .(u, .(v, .(w, admit(carry(x, u, v), z)))))
cond(true, y) → y