a:Assignment, f:Formula, a':Assignment.
a' extends a 
(a |= f a' |= f ) & (a |
f a' | f)
assignment_monotone
F == (F under a) = 3
Thm* a:Assignment, f:Formula, a':Assignment.
a' extends a (a |= f a' |= f ) & (a | f a' | f)
assignment_monotone
Thm* a:Assignment, F:Formula. a | F 
a |= F
formula_falsifiable_lemma1
Thm* a:Assignment, q,r:Formula. a | q
r 
a |= q & a | r
formula_imp_falsifiable_lemma
Thm* a:Assignment, q,r:Formula. a |= qr a | q 
a |= r
formula_imp_sat_lemma
Thm* a:Assignment, q,r:Formula. a | qr a | q & a | r
formula_or_falsifiable_lemma
Thm* a:Assignment, q,r:Formula. a | q
r a | q a | r
formula_and_falsifiable_lemma
Thm* F:Formula, a:Assignment. a | 
F a |= F
formula_not_falsifiable_lemma
Thm* F:Formula, a:Assignment. a |= F a | F
formula_not_sat_lemma
In prior sections: formula falsification