PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
assignment
monotone
1
1.
a:
Assignment
2.
f:
Formula
3.
a':
Assignment
4.
a' extends a
(a |= f
a' |= f ) & (a |
f
a' |
f)
By:
OnHyps [-1;-1;-2] MoveToConcl
Generated subgoal:
1
1.
f:
Formula
a,a':Assignment. a' extends a
(a |= f
a' |= f ) & (a |
f
a' |
f)
About:
a,a':Assignment. a' extends a 
(a |= f a' |= f ) & (a |
f a' | f) (a |= f a' |= f ) & (a | f a' | f) a,a':Assignment. a' extends a (a |= f a' |= f ) & (a | f a' | f)
