PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
zero
rank
valid
or
falsifiable
1
1
2
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))
s
L.|= s
By:
Using [`eq',eqS] (BackThru
Thm*
eq:{T=
}, P:(T
Prop), L:T List.
x
L.P(x)
(
z:T. z(
eq) L
P(z)))
Generated subgoal:
1
z:Sequent. z(
eqS) L
|= z
About:
z:Sequent. z(
eqS) L 
|= z 
}}sL.(
(s) = 0)sL.(
disjoint(eqF;s.H;s.C)) sL.|= s eq:{T=}, P:(T
Prop), L:T List.
xL.P(x) 
(z:T. z(eq) L P(z))) z:Sequent. z(eqS) L |= z 
