Untitled Document

	$\displaystyle\text{LDL}_{f}\textit{ formula }\varphi$	$\displaystyle::=\varphi_{1}\mid\varphi_{1}\;\texttt{`->'}\;\varphi$
	$\displaystyle\varphi_{1}$	$\displaystyle::=\varphi_{2}\mid\varphi_{1}\;\texttt{`\|'}\;\varphi_{2}$
	$\displaystyle\varphi_{2}$	$\displaystyle::=\varphi_{3}\mid\varphi_{2}\;\texttt{`\&'}\;\varphi_{3}$
	$\displaystyle\varphi_{3}$	$\displaystyle::=\texttt{`last'}\mid\alpha\mid\texttt{`!'}\;\varphi_{3}\mid% \texttt{`<'}\rho\;\texttt{`>'}\;\varphi_{3}\mid\texttt{`['}\rho\;\texttt{`]'}% \;\varphi_{3}\mid\texttt{`('}\;\varphi\;\texttt{`)'}$
	$\displaystyle\textit{Regular path }\rho$	$\displaystyle::=\rho_{1}\mid\rho\;\texttt{`+'}\;\rho_{1}$
	$\displaystyle\rho_{1}$	$\displaystyle::=\rho_{2}\mid\rho_{1}\;\texttt{`;'}\;\rho_{2}$
	$\displaystyle\rho_{2}$	$\displaystyle::=\rho_{3}\mid\texttt{`\{'}\;\varphi\;\texttt{`\}'}\;\texttt{`?'% }\mid\rho_{3}\;\texttt{`*'}$
	$\displaystyle\rho_{3}$	$\displaystyle::=\texttt{`\{'}\;\psi\;\texttt{`\}'}\mid\texttt{`!'}\;\rho_{3}% \mid\texttt{`('}\;\rho\;\texttt{`)'}$
	$\displaystyle\textit{Proposition }\psi$	$\displaystyle::=\psi_{1}\mid\psi_{1}\;\texttt{`->'}\;\psi$
	$\displaystyle\psi_{1}$	$\displaystyle::=\psi_{2}\mid\psi_{1}\;\texttt{`\|'}\;\psi_{2}$
	$\displaystyle\psi_{2}$	$\displaystyle::=\psi_{3}\mid\psi_{2}\;\texttt{`\&'}\;\psi_{3}$
	$\displaystyle\psi_{3}$	$\displaystyle::=\alpha\mid\texttt{`!'}\;\psi_{3}\mid\texttt{`('}\;\psi\;% \texttt{`)'}$
	$\displaystyle\textit{Atomic proposition }\alpha$	$\displaystyle::=\texttt{`true'}\mid\texttt{`false'}\mid\textit{symbol}$