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