Nuprl - Proof: rel exp list 2 1 1

(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 1

1. T : Type
2. R : T

T

Prop
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. z : T
10. x R z
11. z R^k-1 y@0

L:T List.

||L|| = k+1

& L[0] = x & last(L) = y@0 & (

i:

k. L[i] R L[(i+1)])

By:	AllHyps (InstHyp [z;y@0]) THEN Analyze -1 THEN Thin -1 THEN Analyze -1 THEN ExRepD THEN InstConcl [[x / L]] THEN Reduce 0

Generated subgoals:

1 12. L : T List
13. ||L|| = k-1+1
14. L[0] = z
15. last(L) = y@0
16. i:(k-1). L[i] R L[(i+1)]
  last([x / L]) = y@0
2 steps

2 12. L : T List
13. ||L|| = k-1+1
14. L[0] = z
15. last(L) = y@0
16. i:(k-1). L[i] R L[(i+1)]
17. i : k
  [x / L][i] R [x / L][(i+1)]
4 steps

3 12. L : T List
13. ||L|| = k-1+1
14. L[0] = z
15. last(L) = y@0
16. i:(k-1). L[i] R L[(i+1)]
17. L1 : T List
18. ||L1|| = k+1
  null(L1)
1 step

About:

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