PrintForm
Definitions
sequent
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
not
sequent
satisfiable
and
falsifiable
1
1
1
1
1.
eqF:
{Formula=
}
2.
S1:
Formula List
3.
S2:
Formula List
4.
a:
Assignment
5.
F
S1.a |
F
F
S2.a |= F
6.
F
S1.a |= F &
F
S2.a |
F
False
By:
Analyze -1
THEN
Analyze -3
Generated subgoals:
1
5.
F
S1.a |
F
6.
F
S1.a |= F
7.
F
S2.a |
F
False
2
5.
F
S2.a |= F
6.
F
S1.a |= F
7.
F
S2.a |
F
False
About: