A Model for Mathematical Analysis of Functional Logic Programs and their Implementations