F
S.H.a |
F 
FS.C.a |= F 
S:Sequent, a:Assignment. Dec(a |= S)a:Assignment, S:Sequent. SqStable(a |= S)
| def | sequent_satisfiable | a |= S == FS.H.a | F FS.C.a |= F |
| THM | decidable__sequent_satisfiable | S:Sequent, a:Assignment. Dec(a |= S) |
| THM | sq_stable__sequent_satisfiable | a:Assignment, S:Sequent. SqStable(a |= S) |