PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
and
sat
lemma1
1
1.
a:
Assignment
2.
q:
Formula
3.
r:
Formula
4.
a |= q
r
a |= q & a |= r
By:
UnfoldTopAb -1
THEN
AbReduce -1
Generated subgoal:
1
4.
(q under a)
(r under a) = 3
a |= q & a |= r
About:
(r under a) = 3
a |= q & a |= r 
r a |= q & a |= r (r under a) = 3 a |= q & a |= r 