Selected Objects
| THM | formula_not_sat_lemma |  F:Formula, a:Assignment. a |=    F   a | F |
| THM | formula_not_falsifiable_lemma | F:Formula, a:Assignment. a | F a |= F |
| THM | formula_and_sat_lemma | a:Assignment, q,r:Formula. a |= q r a |= q & a |= r |
| THM | formula_and_sat_lemma1 | a:Assignment, q,r:Formula. a |= qr  a |= q & a |= r |
| THM | formula_and_falsifiable_lemma | a:Assignment, q,r:Formula. a | qr a | q  a | r |
| THM | formula_or_sat_lemma | a:Assignment, q,r:Formula. a |= qr a |= q a |= r |
| THM | formula_or_falsifiable_lemma | a:Assignment, q,r:Formula. a | qr a | q & a | r |
| THM | formula_imp_sat_lemma | a:Assignment, q,r:Formula. a |= qr a | q a |= r |
| THM | formula_imp_falsifiable_lemma | a:Assignment, q,r:Formula. a | qr a |= q & a | r |
| THM | formula_falsifiable_lemma1 | a:Assignment, F:Formula. a | F  a |= F |
| THM | assignment_monotone | a:Assignment, f:Formula, a':Assignment. a' extends a (a |= f a' |= f ) & (a | f a' | f) |