PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
assignment
monotone
1
1
2
1
1
1
1.
f:
Formula
2.
x:
Formula
3.
a:
Assignment
4.
a':
Assignment
5.
a' extends a
6.
a |= x
a' |= x
7.
a |
x
a' |
x
8.
a |=
x
a' |=
x
By:
BackThru
Thm*
F:Formula, a:Assignment. a |=
F
a |
F
Generated subgoal:
1
a' |
x
About:
a' |
x
a' |= x 
x 
F:Formula, a:Assignment. a |= 
