/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/2.45.trs

The program

(VAR x y z u v)
(RULES
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
)
(COMMENT Example 2.45 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend