Does this Haskell code represent a decision procedure for a theorem?

Question

The following is a natural language description of a first order theory from Worboys. Only Axiom 11 and the Theorem 4 are written in mathematical notation.

Theory 1

1. Aland, Bland, Cland, and Dland are countries.

2. Eye, Jay, Cay, Em, and Ell are cities.

3. Exe and Wye are rivers.

4. City Eye belongs to Aland.

5. City Jay belongs to Bland.

6. City Cay belongs to Cland.

7. City Ell belongs to Dland.

8. City Em belongs to Bland.

9. Cities Eye, Ell Em, and Cay lie on the River Exe.

10. City Jay lies on the River Wye.

11. Each river passes through all countries to which the cities that lie on it belong. $\forall r \forall x \forall c \bullet ((lieOn(c, r) \land belongs(c, x)) \Rightarrow passesThrough(r, x))$

Theorems

1. River Exe passes through countries Aland, Dland, and Cland.

2. River Wye passes through country Bland.

3. River Exe passes through the country Bland.

4. There exists a country that both rivers Exe and Wye pass through. $\exists c \bullet (passesThrough(Exe,c) \land passesThrough(Wye,c)) $

Listing 1 is my attempt to represent Theory 1 in Haskell.

data Country =  Aland | Bland  | Cland | Dland deriving (Show,Eq) -- Axiom 1
data River =  Exe | Wye  deriving (Show,Eq) -- Axiom 2
data City =  Eye | Jay | Cay | Ell | Em  deriving (Show,Eq) -- Axiom 2

belongs (Eye,Aland) = True   -- Axiom 4-9
belongs (Jay,Bland) = True  
belongs (Cay,Cland) = True    
belongs (Ell,Dland) = True    
belongs (Em,Bland) = True
belongs (_,_) = False -- otherwise

lieOn (Eye, Exe) = True 
lieOn (Cay,Exe) = True  
lieOn (Ell,Exe) = True   
lieOn (Em, Exe) = True 
lieOn (Jay,Wye) = True  
lieOn (_,_) = False -- otherwise


-- Constructs a list of elemenets (countries) common to both input lists.
commonCountry [] cs = []
commonCountry cs [] = []
commonCountry  cs1 (country:cs2)  = if (elem country cs1) then (country : (commonCountry cs1 cs2)) else []  


-- Create a list of countries for a given fixed list of cities
city2Country cityList =  [ y | x  <- cityList, y <- [Aland,Bland,Cland ,Dland], belongs (x,y)]

-- Create a list all cities for a given river 1:M
river2City r =  [ x | x  <- [Eye,Jay,Cay,Ell,Em], lieOn (x,r)]

passesThrough river =  city2Country (river2City river)

theorem1 = passesThrough Exe
theorem2 = elem Bland (passesThrough Wye)
theorem3 = elem Bland (passesThrough Exe)
theorem4 = commonCountry (passesThrough Exe) (passesThrough Wye) 
-- > Gives expected result [Bland]

I have two questions:

1) Can the Haskell program Listing 1 be considered as a faithful representation of Theory 1?

2) Can the execution of the Haskell encoding of theorem4, be considered as a decision procedure for Theorem 4 in Theory 1?

Where a decision procedure is an algorithm that terminates with a correct true or false answer.

My thoughts on question 1). Axioms 1-3 are represented by the data statements. Axioms 4-9 are represented by equations, but the two equations defined to be False have no explicit correspondence in Theory 1. Axiom 11 is not directly represented in my code. I found the computational steps difficult to relate to logic, I just intuitively wrote code to give the desired result.

My thoughts on question 2). The execution theorem4 gives the expected result. We can reason "about" Haskell programs using "equational reasoning", which seems to be related to equational logic. If the representation is OK, is there is some grounds for believing that the execution might "some way" provide a decision procedure and indirectly a proof for Theorem 4.

Related to an earlier question. I am motivated by the work of Thompson, who shows how the definitions of a functional program can be interpreted as logical equations. I do not understand the precise relation (if any) between logic and my attempt to represent that logic in a Haskell program.

UPDATE

I translated the Haskell code in Listing 1 to the equational specification language CafeOBJ which has a functional sub-language roughly equivalent to Haskell (at least wrt to this case). I then used the built-in FOL theorem prover to prove:

$\exists c:Country \bullet (elem(c,passesThrough(Exe)) \land elem(c,passesThrough(Wye))))$

which is as close as I can get to the FOL Theorem 4 (theorem4 in the Haskell code):

$\exists c:Country \bullet (passesThrough(Exe,c) \land passesThrough(Wye,c))$.

Provided my translation is correct, what can I say about the relationship between the Haskell program (or the CafeOBJ equivalent) and the original FOL Theory 1? Can I say, for example, that the program(s) provides an algorithm (or model?) that satisfies Theorem 4? or that the Haskell program represents a search algorithm related to the theorems?