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