Nuprl - Proof: length of not nil

(5steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: length of not nil

A:Type, as:A List.

as = nil

||as||

By:	RepD THEN (OnVar `as' Analyze) THEN (Reduce 0)

Generated subgoals:

1 1. A : Type
2. A List
3. nil = nil  A List
  01
1 step

2 1. A : Type
2. A List
3. u : A
4. v : A List
5. u.v = nil
  ||v||+11
Auto

3 1. A : Type
2. A List
3. u : A
4. v : A List
5. ||v||+11
  u.v = nil
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(5steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc

1	1. A : Type 2. A List 3. nil = nil A List 01	1 step
2	1. A : Type 2. A List 3. u : A 4. v : A List 5. u.v = nil \|\|v\|\|+11	Auto
3	1. A : Type 2. A List 3. u : A 4. v : A List 5. \|\|v\|\|+11 u.v = nil	2 steps