At: propositional decidability 1 1 1 2 1 1 1
1. S: Sequent
2. L: Sequent List
3. 
s
L.(
(s) = 0)
4. sL.|= s 
|= S
5. a: Assignment
6. 
sL.a |
s
7. sL.a | s a | S
8. a | S
|= S 
(a:Assignment. a | S)
By:
Choose [2]
THEN
With a (Analyze 0)
Generated subgoals:None
About:
