PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
zero
rank
valid
or
falsifiable
1
1
2
1
1.
L:
Sequent List
2.
eqS:
{Sequent=
}
3.
eqF:
{Formula=
}
4.
s
L.(
(s) = 0)
5.
s
L.disjoint(eqF;s.H;s.C)
6.
s
L.(
disjoint(eqF;s.H;s.C))
s
L.|= s
(
a:Assignment.
s
L.a |
s)
By:
Thin -2
THEN
Choose [1]
Generated subgoal:
1
5.
s
L.(
disjoint(eqF;s.H;s.C))
s
L.|= s
About:
s
L.(
disjoint(eqF;s.H;s.C))
sL.|= s 
}}sL.(
(s) = 0)
sL.disjoint(eqF;s.H;s.C)sL.(disjoint(eqF;s.H;s.C)) sL.|= s 
(a:Assignment. sL.a |
s)sL.(disjoint(eqF;s.H;s.C)) sL.|= s 
