Nuprl - Proof: rel exp list

(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

T:Type, R:(T

T

Prop), k:

, x,y:T.

(x R^k y)

(

L:T List.

(||L|| = k+1

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

i:

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

By:	InductionOnNat THEN RecUnfold `rel_exp` 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. R : TTProp
  x,y:T.
  x = y

  (L:T List.
  (||L|| = 1   & L[0] = x & last(L) = y & (i:0. L[i] R L[(i+1)]))
2 steps

2 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)]))
  x,y:T.
  (x if k=0 x,y. x = y else x,y. z:T. (x R z) & (z R^k-1 y) fi y)

  (L:T List.
  (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))
23 steps

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