Proposition 20   Let Σ be a formula from PROPρ s and V ⊆ P S.  We have ForgetVar(Σ, V) ≡ ForgetLit(Σ, Lv)
Proof: By induction on |V|. The proposition trivially holds for |V| = 0. Let us assume it is true whenever [V] = k. Let V = {v1,...,vk+1}. By definition, we have ForgetVar(Σ,V) = ForgetVar(ForgetVar(Σ,{v1,...,vk}); {vk+1})
By the induction hypothesis, ForgetVar(E,V) is equivalent to ForgetVar(D, {Vk+1}),
where Φ is defined as:
Φ = ForgetLit(Σ, { x; x ∈ { v 1, . . . , v k }} ∪ {¬x; x ∈ { v 1, . . , v k }})
We have ForgetVar(E,V) = ForgetVar(D, {Vk+1}). By definition, ForgetVar(Φ,vk+1) = Φvk+1 ←0 V Φvk+1←1 We also have ForgetLit(Φ, {υk+1, ¬υk +1})
=
ForgetLit(ForgetLit(Φ,{υk+1}),{¬υk+1})

Forget Lit ((¬vk+1 ∧ Φvk+1 ←0) V Φvk+1 ←1, {¬vk+1})
( Vk +1 A ((¬Vk +1 A Ävk+1 ←0) V Ävk+1 ←1)vk+1 ←1)V ((¬Vk +1 A Ävk+1 ←0) V Ävk+1 ←1)vk+1 ←0 .

This simplifies to (vk+1 A Qvk+1 -1) V Qvk+1 -0 V Qvk+1 -1 -1 -1 -1 which is also equivalent to Φvk+i ← 0 V Φvk+i ← 1, hence equivalent to ForgetVar (Φ, { vk + 1} ). Consequently, we have For g et V ar ( Σ, V)
= ForgetLit(ForgetLit(Σ t { x ; x ∈ { v 1 , . . , v k }} ∪ {¬x; x ∈ { v 1 , . . , v k }}); { v k +1 ; ¬v k +1 })
Forget Lit (Σ, V).

=
Proposition 21   Let Σ, Φ be two formulas from PROPρς, and V be a subset of P S.  If V Æ, then ForgetVar(E A Φ, V) ≡ Σ ∧ ForgetVar(Φ, V).

Proof: Let us consider the case where V = {v}. By definition, we have ForgetVar(Σ Λ
Φ, {v}) = (Σ ∧ Φ) v ← 0 ∨ (Σ ∧ Φ) v ← 1   Equivalently, ForgetVar(Σ ∧ Φ, {v}) ≡ (Σ v ← 0 ∧
Q v ( ) V ( Σ v ← 1 ∧ Φ v ← 1 ). When v ̸ A + Σ, we have Σ ≡ Σ v ← 0 ≡ Σ v ← 1 . Accordingly, ForgetVar(Σ ∧ Φ t {v}) ≡ Σ ∧ (Φ v ← o ∨ Φ v ← 1 ) ≡ Σ ∧ Forget(Φ,{v}).  A straightforward induction completes the proof. Proposition 22   Let Σ, Φ be two formulas from PROPρς, and P, Q, Z be three disjoint sets of variables from PS (such that Var(E)UVar(Φ)⊆ PUQUZ). It holds: