PrintForm
Definitions
formula
satisfaction
Sections
ClassicalProps(jlc)
Doc
At:
sq
stable
formula
sat
a:Assignment, F:Formula. SqStable(a |= F )
By:
Unfold `sq_stable` 0
THEN
Unfold `formula_sat` 0
Generated subgoal:
1
1.
a:
Assignment
2.
F:
Formula
3.
((F under a) = 3
)
(F under a) = 3
About:
((F under a) = 3
)
(F under a) = 3 
a:Assignment, F:Formula. SqStable(a |= F )((F under a) = 3) (F under a) = 3
