Nuprl - Pf not_list_exists_rank_gt_0_rank

PrintForm Definitions sequent rank Sections ClassicalProps(jlc) Doc

hyp,concl:Formula List. fhyp.((f) > 0) fconcl.((f) > 0) ( < hyp,concl > ) = 0

By: Analyze 0 THEN ListInd -1

Generated subgoals:

1 1. hyp: Formula List
concl:Formula List. fnil.((f) > 0) fconcl.((f) > 0) ( < nil,concl > ) = 0

2 1. hyp: Formula List
2. u: Formula
3. v: Formula List
4. concl:Formula List. fv.((f) > 0) fconcl.((f) > 0) ( < v,concl > ) = 0
concl:Formula List. f(u.v).((f) > 0) fconcl.((f) > 0) ( < u.v,concl > ) = 0

About:

1	1. `hyp:` `Formula List` `concl:Formula List. fnil.((f) > 0) fconcl.((f) > 0) ( < nil,concl > ) = 0`
2	1. `hyp:` `Formula List` 2. `u:` `Formula` 3. `v:` `Formula List` 4. `concl:Formula List. fv.((f) > 0) fconcl.((f) > 0) ( < v,concl > ) = 0` `concl:Formula List. f(u.v).((f) > 0) fconcl.((f) > 0) ( < u.v,concl > ) = 0`