Nuprl - Proof: list decomp reverse 1

(11steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list decomp reverse 1

1. T : Type
2. L : T List
3. 0<||L||

x:T, L':T List. L = (L' @ [x])

By:

ListInd 2

Generated subgoals:

1   0<||nil||  (x:T, L':T List. nil = (L' @ [x]))
1 step

2 3. u : T
4. v : T List
5. 0<||v||  (x:T, L':T List. v = (L' @ [x]))
  0<||[u / v]||  (x:T, L':T List. [u / v] = (L' @ [x]))
8 steps

About:

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

(11steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc

1	0<\|\|nil\|\| (x:T, L':T List. nil = (L' @ [x]))	1 step
2	3. u : T 4. v : T List 5. 0<\|\|v\|\| (x:T, L':T List. v = (L' @ [x])) 0<\|\|[u / v]\|\| (x:T, L':T List. [u / v] = (L' @ [x]))	8 steps