PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
prop
decide
1
1
1
2
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.
a:Assignment.
s
L.a |
s
|= S
(
a:Assignment. a |
S)
By:
Analyze -1
Generated subgoal:
1
6.
a:
Assignment
7.
s
L.a |
s
|= S
(
a:Assignment. a |
S)
About:
s
L.a |
s
|= S 
(a:Assignment. a | S)
sL.(
(s) = 0)sL.|= s 
|= S a:Assignment. sL.a | s a | Sa:Assignment. sL.a | s |= S (a:Assignment. a | S)sL.a | s |= S (a:Assignment. a | S)
