(26steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel exp list 2 1 2 2 1
1. T : Type
2. R : TTProp
3. k : 
4. 0<k
5. x,y:T.
5. (x R^k-1 y)
5. 
5. (L:T List. 
5. (||L|| = k-1+1 & L[0] = x & last(L) = y & (i:(k-1). L[i] R L[(i+1)]))
6. k = 0
7. x : T
8. y@0 : T
9. L : T List
10. ||L|| = k+1
11. L[0] = x
12. last(L) = y@0
13. i:k. L[i] R L[(i+1)]
  L1:T List. 
  ||L1|| = k-1+1  
  & L1[0] = L[1] & last(L1) = y@0 & (i:(k-1). L1[i] R L1[(i+1)])
By: ListInd -5 THEN Reduce 0

Generated subgoals:

1 10. u : T
11. v : T List
12. ||v|| = k+1  
12. 
12. v[0] = x
12. 
12. last(v) = y@0
12. 
12. (i:k. v[i] R v[(i+1)])
12. 
12. (L1:T List. 
12. (||L1|| = k-1+1  
12. (& L1[0] = v[1] & last(L1) = y@0 & (i:(k-1). L1[i] R L1[(i+1)]))
13. ||v||+1 = k+1
14. u = x
15. last([u / v]) = y@0
16. i:k. [u / v][i] R [u / v][(i+1)]
  L1:T List. 
  ||L1|| = k-1+1  
  & L1[0] = v[0] & last(L1) = y@0 & (i:(k-1). L1[i] R L1[(i+1)])
6 steps
2 10. u : T
11. v : T List
12. ||v|| = k+1  
12. 
12. v[0] = x
12. 
12. last(v) = y@0
12. 
12. (i:k. v[i] R v[(i+1)])
12. 
12. (L1:T List. 
12. (||L1|| = k-1+1  
12. (& L1[0] = v[1] & last(L1) = y@0 & (i:(k-1). L1[i] R L1[(i+1)]))
13. ||v||+1 = k+1
14. u = x
  null([u / v])
1 step

About:
listconsassertintnatural_numberaddsubtractless_than
functionuniverseequalpropandall
exists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(26steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc