LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:herbrand_universe_for_equality [2008/04/02 22:59]
vkuncak
sav08:herbrand_universe_for_equality [2015/04/21 17:30] (current)
Line 2: Line 2:
  
 Recall example of formula $F$: Recall example of formula $F$:
-\[+\begin{equation*}
     P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)     P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)
-\]+\end{equation*}
 Replace '​='​ with '​eq':​ Replace '​='​ with '​eq':​
-\[+\begin{equation*}
     P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. eq(x,a) \lor eq(x,b))     P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. eq(x,a) \lor eq(x,b))
-\]+\end{equation*}
 call the resulting formula $F'$. call the resulting formula $F'$.