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. |= < hyp,[q; r/ M @ N] >
7. a: Full( < hyp,M @ (qr.N) > )

a |= < hyp,M @ (qr.N) >

By: With a (Analyze -2)

Generated subgoals:

1 6. a: Full( < hyp,M @ (qr.N) > )
a Full( < hyp,[q; r/ M @ N] > )

2 6. a: Full( < hyp,M @ (qr.N) > )
7. a |= < hyp,[q; r/ M @ N] >
a |= < hyp,M @ (qr.N) >

About:

1	6. `a:` `Full( < hyp,M @ (qr.N) > )` `a Full( < hyp,[q; r/ M @ N] > )`
2	6. `a:` `Full( < hyp,M @ (qr.N) > )` 7. `a \|= < hyp,[q; r/ M @ N] >` `a \|= < hyp,M @ (qr.N) >`