Selected Objects

def	formula_sat	a |= F == (F under a) = 3
THM	sq_stable__formula_sat	a:Assignment, F:Formula. SqStable(a |= F )
THM	decidable__formula_sat	a:Assignment, f:Formula. Dec(a |= f )