Nuprl - Pf not_list_exists_rank_gt_0_rank

PrintForm Definitions sequent rank Sections ClassicalProps(jlc) Doc

At: not list exists rank gt 0 rank 0 2 1 1 1

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

f(u.v).((f) > 0) fconcl.((f) > 0) ( < u.v,concl > ) = 0

By: MoveToConcl -1 THEN ListInd -1

Generated subgoals:

1 (fv.((f) > 0) fnil.((f) > 0) ( < v,nil > ) = 0) f(u.v).((f) > 0) fnil.((f) > 0) ( < u.v,nil > ) = 0

2 4. u1: Formula
5. v1: Formula List
6. (fv.((f) > 0) fv1.((f) > 0) ( < v,v1 > ) = 0) f(u.v).((f) > 0) fv1.((f) > 0) ( < u.v,v1 > ) = 0
(fv.((f) > 0) f(u1.v1).((f) > 0) ( < v,u1.v1 > ) = 0) f(u.v).((f) > 0) f(u1.v1).((f) > 0) ( < u.v,u1.v1 > ) = 0

About:

1	`(fv.((f) > 0) fnil.((f) > 0) ( < v,nil > ) = 0) f(u.v).((f) > 0) fnil.((f) > 0) ( < u.v,nil > ) = 0`
2	4. `u1:` `Formula` 5. `v1:` `Formula List` 6. `(fv.((f) > 0) fv1.((f) > 0) ( < v,v1 > ) = 0) f(u.v).((f) > 0) fv1.((f) > 0) ( < u.v,v1 > ) = 0` `(fv.((f) > 0) f(u1.v1).((f) > 0) ( < v,u1.v1 > ) = 0) f(u.v).((f) > 0) f(u1.v1).((f) > 0) ( < u.v,u1.v1 > ) = 0`