Nuprl - Proof: symmetrized preorder 3

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: symmetrized preorder 3

1. T : Type
2. R : T

Prop
3. Refl(T;x,y.R(x,y))
4. Trans x,y:T. R(x,y)

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

By:	OnCls [4;0] (Unfold `trans`)

Generated subgoals:

1 4. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
5. a : T
6. b : T
7. c : T
8. R(a,b)
9. R(b,a)
10. R(b,c)
11. R(c,b)
  R(a,c)
1 step

2 4. a,b,c:T. R(a,b)  R(b,c)  R(a,c)
5. a : T
6. b : T
7. c : T
8. R(a,b)
9. R(b,a)
10. R(b,c)
11. R(c,b)
  R(c,a)
1 step

About:

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

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

1	4. a,b,c:T. R(a,b) R(b,c) R(a,c) 5. a : T 6. b : T 7. c : T 8. R(a,b) 9. R(b,a) 10. R(b,c) 11. R(c,b) R(a,c)	1 step
2	4. a,b,c:T. R(a,b) R(b,c) R(a,c) 5. a : T 6. b : T 7. c : T 8. R(a,b) 9. R(b,a) 10. R(b,c) 11. R(c,b) R(c,a)	1 step