(CoFI) Total FUN-DEFNs

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear friends,

I refer to a proposal of Bernd and myself:

>FUN-DEFNs should be partial *and total*
>---------------------------------------
>Bernd Krieg-Brueckner, Till Mossakowski
>
>Proposed change
>---------------
>
>FUN-DEFN	::= fun-defn FUN-NAME FUN-TYPE TERM
>SORTS		::= sorts SORT*
>		|   parameters VAR-DECL+

It should be added that, for a total FUN-DEFN, 
the TERM has to consist of total function symbols
only. Otherwise, an extension consisting of total FUN-DEFNs
is not conservative in all cases; namely, new definedness
properties may be introduced:

def f(x1:s1, ... xn:sn) =s= t

forces t to be defined since f(x1:s1, ... xn:sn) is defined.

Greetings,
Till