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 |= qr 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)

the other theories