PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
propositional
decidability
1
1
1
1
1.
S:
Sequent
2.
L:
Sequent List
3.
s
L.(
(s) = 0)
4.
s
L.|= s
|= S
5.
a:Assignment.
s
L.a |
s
a |
S
6.
s
L.|= s
|= S
(
a:Assignment. a |
S)
By:
FwdThru -3 [-1]
Generated subgoal:
1
7.
|= S
|= S
(
a:Assignment. a |
S)
About:
|= S 
(
a:Assignment. a |
S)
s
L.(
(s) = 0)sL.|= s 
|= S a:Assignment. sL.a | s a | SsL.|= s |= S (a:Assignment. a | S) |= S (a:Assignment. a | S)
