Thm* a:Assignment, q,r:Formula. a | qr 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 |= qr a |= q a |= r formula_or_sat_lemma

Thm* a:Assignment, q,r:Formula. a | qr a | q a | r formula_and_falsifiable_lemma

Thm* a:Assignment, q,r:Formula. a |= qr a |= q & a |= r formula_and_sat_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: core fun 1 well fnd int 1 bool 1 rel 1 quot 1 int 2 list 1 bool 2 jlc discrete jlc core 3 jlc list 3 jlc