Nuprl - Pf zero_rank_valid_or_falsifiable 1 1 2 1 1 1 1 1 1 1

PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank valid or falsifiable 1 1 2 1 1 1 1 1 1 1

1. L: Sequent List
2. eqS: {Sequent=}
3. eqF: {Formula=}
4. sL.((s) = 0)
5. sL.(disjoint(eqF;s.H;s.C))
6. z: Sequent
7. x: Formula
8. x(eqF) z.H
9. x(eqF) z.C

|= z

By: Analyze 0

Generated subgoal:

1 10. a: Full(z)
a |= z

About: