PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
zero
rank
valid
or
falsifiable
1
1
2
1
1
1
1
1
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.
z:
Sequent
7.
z(
eqS) L
8.
disjoint(eqF;z.H;z.C)
9.
x:
Formula
10.
x(
eqF) z.H
11.
x(
eqF) z.C
|= z
By:
OnHyps [-4;-4] Thin
Generated subgoal:
1
7.
x:
Formula
8.
x(
eqF) z.H
9.
x(
eqF) z.C
|= z
About:
eqF) z.HeqF) z.C
|= z 
}}
sL.(
(s) = 0)sL.(
disjoint(eqF;s.H;s.C))eqS) Ldisjoint(eqF;z.H;z.C)eqF) z.HeqF) z.C |= z eqF) z.HeqF) z.C |= z 
