Nuprl - Proof: order split

(9steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: order split

T:Type, R:(T

Prop).

Order(T;x,y.R(x,y))

(

x,y:T. Dec(x = y))

(

a,b:T. R(a,b)

strict_part(x,y.R(x,y);a;b)

a = b)

By:	Unfold `strict_part` 0 THEN AGenRepD ["compound";"basic"]

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. a:T. R(a,a)
4. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
5. x,y:T. R(x,y)  R(y,x)  x = y
6. x,y:T. Dec(x = y)
7. a : T
8. b : T
9. R(a,b)
  R(a,b) & R(b,a)  a = b
4 steps

2 1. T : Type
2. R : TTProp
3. a:T. R(a,a)
4. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
5. x,y:T. R(x,y)  R(y,x)  x = y
6. x,y:T. Dec(x = y)
7. a : T
8. b : T
9. R(a,b) & R(b,a)  a = b
  R(a,b)
4 steps

About:

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

(9steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc

1	1. T : Type 2. R : TTProp 3. a:T. R(a,a) 4. a,b,c:T. R(a,b) R(b,c) R(a,c) 5. x,y:T. R(x,y) R(y,x) x = y 6. x,y:T. Dec(x = y) 7. a : T 8. b : T 9. R(a,b) R(a,b) & R(b,a) a = b	4 steps
2	1. T : Type 2. R : TTProp 3. a:T. R(a,a) 4. a,b,c:T. R(a,b) R(b,c) R(a,c) 5. x,y:T. R(x,y) R(y,x) x = y 6. x,y:T. Dec(x = y) 7. a : T 8. b : T 9. R(a,b) & R(b,a) a = b R(a,b)	4 steps