One-Point Rule
In many formula simplifications we use the one-point rule:
![\begin{equation*}
(\exists x.\ x=t \land F) \ \leftrightarrow\ F[x:=t]
\end{equation*}](/w/lib/exe/fetch.php?media=wiki:latex:/img2188399dffaaf1897f345cfa78e889b0.png "Equation")
Recall: we have shown in lecture03b.pdf that then
![\begin{equation*}
(\forall x.\ x=t \rightarrow F) \ \leftrightarrow\ F[x:=t]
\end{equation*}](/w/lib/exe/fetch.php?media=wiki:latex:/img30506300be5c541503f98691edb3c3f5.png "Equation")
follows.
Menu
In many formula simplifications we use the one-point rule:
Recall: we have shown in lecture03b.pdf that then
follows.