PrintForm Definitions sequent sat lemmas Sections ClassicalProps(jlc) Doc

At: not sequent satisfiable and falsifiable 1 1 1 1 1 1 1 1 1
1. eqF: {Formula=}
2. S1: Formula List
3. S2: Formula List
4. a: Assignment
5. FS1.a | F
6. x: Formula
7. x(eqF) S1
8. a | x
9. z:Formula. z(eqF) S1 a |= z
10. a |= x

False
By: FwdThru Thm* a:Assignment, F:Formula. a | F a |= F [-3]
Generated subgoal:

111. a |= x
False

About:
falselistassertallimplies