PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
not
sat
lemma
1
1
1.
F:
Formula
2.
a:
Assignment
3.
a |=
F
a |
F
By:
Analyze 3
THEN
Unfold `formula_falsifiable` 0
Generated subgoal:
1
3.
(
F under a) = 3
(F under a) = 3
About:
F under a) = 3
(F under a) = 3
F a |
FF under a) = 3 (F under a) = 3