# The `append` predicate

`: (? (append (a b) (c) @X)) @X=(a b c)-> NIL`
`: (? (append @X @Y (a b c))) @X=NIL @Y=(a b c) @X=(a) @Y=(b c) @X=(a b) @Y=(c) @X=(a b c) @Y=NIL-> NIL`
`(be append (NIL @X @X))`
`(be append ((@A . @X) @Y (@A . @Z)) (append @X @Y @Z))`
`: (? append (append (a b) (c) @X))2 (append (a b) (c) (a . @Z))2 (append (b) (c) (b . @Z))1 (append NIL (c) (c)) @X=(a b c) -> NIL`

# The `reverse`predicate

`: (? (reverse (a b c) @X)) @X = (c b a)`
`(be reverse (NIL NIL))(be reverse ((@A . @X) @R)   (reverse @X @Z)   (append @Z (@A) @R))`

# Using an accumulator

`(be accRev ((@H . @T) @A @R)   (accRev @T (@H . @A) @R) )(be accRev (NIL @A @A))`
`(be reverse (@L @R)   (accRev @L NIL @R))`
`: (? reverse accRev ( reverse (a b c) @X))1 (reverse (a b c) @R)1 (accRev (a b c) NIL @R)1 (accRev (b c) (a) @R)1 (accRev (c) (b a) @R)2 (accRev NIL (c b a) (c b a)) @X=(c b a)-> NIL`

# Example: Palindrome Checker

`(be palindrome (@L)   (reverse @L @L) )`
`: (? (palindrome ( r o t a t o r)))-> T: (? (palindrome ( a b c d e f g)))-> NIL`

--

--