The expressive power of the Haskell foldr function is unbelievable!
1: The filter R (x:xs) function applies an equivalence relation R on every element in the list argument, (x:xs). If R evaluates true, the element x is appended to the result list otherwise it is dropped.
Main> filter (< 3) [1,2,3,4,5]
In the above filter application, (< 3) is the equivalence relation, R. One of the arguments in R is already specified as the value 3. It could be any expression that evaluate to the same type as the elementes of the list. Another condition is that when the function R acts on the elements in the result the result must be a boolean value.
The type signature of the relation R function is R :: (a -> Bool)
Haskell has a corny name called section to denote usually infix operations that is written in a prefix style. Sections are infix operations that are enclosed within a parenthesis. In the above example, (< 3) is a section. (< 3) x in prefix form is the same as x < 3 .
Moving on, the type signature of filter is type signature of R and the type signature of the remaining semantics. The remaining semantics is that filter takes a list parameter and generates another list parameter i.e. ([a] -> [b])
You can also say all of this in another way, the function filter takes 2 arguments, first one is a function with a signature (a -> Bool) and the second is a list of a generic type, called [a] and computes a result which is of a list of the same type as [a].
filter :: (a -> Bool) -> [a] -> [a]
2: The foldr f v (x:xs) function replaces the empty list constructor  in (x:xs) with the function argument v, and the cons operator or (:) with f.
foldr can be concisely (and recursively) represented as
foldr f v (x:xs) = f x (foldr f v (x:xs))
One can construct a filter function using foldr as follows:
filt p (x:xs) = foldr (if p then x:xs else xs)  (x:xs)
This means, for a given list, replace the empty list construct  with , if x is such that p x is true, replace list with (x:xs), else if p x is false, replace (x:xs) with xs.
Please correct me if I am wrong!
I found some pretty interesting list theory theorems in this page
HOL is an interesting link, but I got no idea yet on the use for this kind of tool or the reach for these algorithms.
Anyway! Adios. Hope you enjoyed reading this stuff as much as I am enjoying reading about this from the PPTs here: