Nuprl - Pf formula_or_right

PrintForm Definitions elimination Sections ClassicalProps(jlc) Doc

1. hyp: Formula List
2. M: Formula List
3. N: Formula List
4. q: Formula
5. r: Formula
6. a: Assignment
7. Fhyp.a | F a |= q a |= r FM.a |= F FN.a |= F

Fhyp.a | F FM.a |= F a |= q a |= r FN.a |= F

By: RepeatOrHD -1

Generated subgoals:

1 7. Fhyp.a | F
Fhyp.a | F FM.a |= F a |= q a |= r FN.a |= F

2 7. a |= q
Fhyp.a | F FM.a |= F a |= q a |= r FN.a |= F

3 7. a |= r
Fhyp.a | F FM.a |= F a |= q a |= r FN.a |= F

4 7. FM.a |= F
Fhyp.a | F FM.a |= F a |= q a |= r FN.a |= F

5 7. FN.a |= F
Fhyp.a | F FM.a |= F a |= q a |= r FN.a |= F

About:

1	7. `Fhyp.a \| F` `Fhyp.a \| F FM.a \|= F a \|= q a \|= r FN.a \|= F`
2	7. `a \|= q` `Fhyp.a \| F FM.a \|= F a \|= q a \|= r FN.a \|= F`
3	7. `a \|= r` `Fhyp.a \| F FM.a \|= F a \|= q a \|= r FN.a \|= F`
4	7. `FM.a \|= F` `Fhyp.a \| F FM.a \|= F a \|= q a \|= r FN.a \|= F`
5	7. `FN.a \|= F` `Fhyp.a \| F FM.a \|= F a \|= q a \|= r FN.a \|= F`