PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
imp
falsifiable
lemma
1
1.
a:
Assignment
2.
q:
Formula
3.
r:
Formula
a |
q
r
a |= q & a |
r
By:
Analyze 0
THEN
Analyze 0
Generated subgoals:
1
4.
a |
q
r
a |= q & a |
r
2
4.
a |= q & a |
r
a |
q
r
About:
q
r
a |= q & a | r r a | qr a | qr 
a |= q & a | r qr a |= q & a | r r a | qr