PrintForm
Definitions
sequent
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
not
sequent
satisfiable
and
falsifiable
1
1
1
1
2
1
1.
eqF:
{Formula=
}
2.
S1:
Formula List
3.
S2:
Formula List
4.
a:
Assignment
5.
F
S2.a |= F
6.
F
S2.a |
F
False
By:
Using [`eq',eqF] (FwdThru
Thm*
eq:{T=
}, P:(T
Prop), L:T List. (
x:T. x(
eq) L & P(x))
y
L.P(y) [-2])
THEN
Analyze -1
THEN
Analyze -1
Generated subgoal:
1
7.
x:
Formula
8.
x(
eqF) S2
9.
a |= x
False
About:
eqF) S2
False
}
FS2.a |= F 
FS2.a |
F Falseeq:{T=}, P:(T
Prop), L:T List.
(x:T. x(eq) L & P(x)) 
yL.P(y)
[-2])
eqF) S2 False
