(1) l +A 2;
(2) Ei ←1 |= Ei ←0; (3)  Σ
(4) E t ← 1 |= Σ.

## Proof:

(1) ⇒ (2): Let v the variable of l and assume that Σ t ← 1 ̸ = Σ t ← 0, which means that there is

a PS \ {v}-world ω such that ω |= Σι ← 1 ∧¬Σι ← 0; since Σ is equivalent to (l ∧Σι ← 1 ) V
(¬l ∧ ∑ t ← 0), we have ω ∧ {l} |= ∑ t ← 1 ∧ l |= ∑ and Force(ω ∧ {l}, ¬l) = ω ∧ {¬l} |=
‡‡
(2) => (3): Assume Et t 1 |= Et t -0. We have the following chain of implications:
I 
E
(l A ElLo)V(¬l A ElLo)
E
(3) => (1): Let us assume that Σ => Σ t ← 0 , and prove that l ̸ => Σ . Indeed, the assumption

cn be rewritten as:
∀ω E Ωps . (ω |= Σ  ⇒ω |= Σι ←o)
Now, ω = Σι 40 is equivalent to say that changing the truth value of l to false, ω is still a model of Σ. In formulas,
∀ω E Ω PS . (ω |= Σ  ⇒ Force(ω, ¬l) |= Σ)
This is exactly the definition of l H E.

(2) ⇒ (4): Same as the proof of (2) ⇒ (3). (4) ⇒ (1): Similar to the proof of (3) ⇒ (1).

Proposition 7   Let Σ be a formula from PROP 5 and x be a variable of P S.  The next four statements are equivalent:
(1) x A + 2;
(2) Σ x ← 0 ≡ Σ x ← 1;
(3) ∑ ≡ ∑ x ← 0 ;
() ∑ ≡ ∑ x ← 1 .

Proof : Easy consequence of the definition of FV-independence (Σ is Var-independent from x if and only if it is Lit-independent from { x, ¬ x}), and Proposition 6).

Proposition 8   Let Σ be a formula from PROPps and L be a subset of Lps. The next statements are equivalent: