Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:herbrand_universe_for_equality [2008/04/02 22:58] vkuncak |
sav08:herbrand_universe_for_equality [2008/04/02 22:59] vkuncak |
||
|---|---|---|---|
| Line 24: | Line 24: | ||
| - $S$ has a model; | - $S$ has a model; | ||
| - $S' \cup AxEq$ has a model (where $AxEq$ are [[Axioms for Equality]] and $S'$ is result of replacing '=' with 'eq' in $S$); | - $S' \cup AxEq$ has a model (where $AxEq$ are [[Axioms for Equality]] and $S'$ is result of replacing '=' with 'eq' in $S$); | ||
| - | - $S$ has a model whose domain is the quotient $[GT]$ of ground terms under some congruence. | + | - $S$ has a model whose domain is the quotient $[GT]$ of the set of ground terms under some congruence. |