Nuprl - Pf zero_rank_valid_or_falsifiable 1 1 1 1 1 1

PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank valid or falsifiable 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. x: Sequent
7. x(eqS) L
8. disjoint(eqF;x.H;x.C)

a:Assignment. sL.a | s

By: Assert ((v.if v(eqF) x.H3 ;v(eqF) x.C3 else 3 fi) Assignment)

Generated subgoals:

1 (v.if v(eqF) x.H3 ;v(eqF) x.C3 else 3 fi) Assignment

2 9. (v.if v(eqF) x.H3 ;v(eqF) x.C3 else 3 fi) Assignment
a:Assignment. sL.a | s

About:

1	`(v.if v(eqF) x.H3 ;v(eqF) x.C3 else 3 fi) Assignment`
2	9. `(v.if v(eqF) x.H3 ;v(eqF) x.C3 else 3 fi) Assignment` `a:Assignment. sL.a \| s`