Skip to content
Snippets Groups Projects
Commit 2107f2b0 authored by Rony Abecidan's avatar Rony Abecidan
Browse files

Merge branch 'patch-1' into 'master'

parents 6f5a7ab2 dc780797
No related branches found
No related tags found
No related merge requests found
......@@ -20,10 +20,12 @@ free variables** and, for each **I** over **R** and valuation $`ν`$ over free(
Let's say that : $`\Psi = \Phi \ \varphi \ \Phi^{\prime}`$ . In that case $`\Psi^{\prime} = \Phi \ \psi \ \Phi^{\prime}`$.
$`\blacksquare`$ Clearly, $`free(\Psi)=free(\varphi) \ \text{and} \ free(\Psi^{\prime})=free(\psi)`$
$`\blacksquare`$ Clearly, $`free(\Psi)=free(\Phi) \cup free(\varphi) \cup free(\Phi^{\prime}) \ \text{and} \ free(\Psi^{\prime})= free(\Phi) \cup free(\psi) \cup free(\Phi^{\prime})`$
By hypothesis, $`\varphi`$ and $`\psi`$ are equivalent and so :
$`free(\Psi)=free(\varphi)=free(\psi)=free(\Psi^{\prime})`$
$`free(\varphi)=free(\psi)`$
Hence, $`free(\Psi)=free(\Psi^{\prime})`$
$`\blacksquare`$ Let's **I** an instance over **R** and $`v`$ a valuation over $`free(\Psi)=free(\Psi^{\prime})`$.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment