Nuprl - Proof: rel inverse exp

(14steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Search Doc

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel inverse exp

T:Type, R:(T

Prop), n:

, x,y:T. (x R^n^-1 y)

(x R^-1^n y)

By:	InductionOnNat

Generated subgoals:

1 1. T : Type
2. R : TTProp
  x,y:T. (x R^0^-1 y)  (x R^-1^0 y)
1 step

2 1. T : Type
2. R : TTProp
3. n :
4. 0<n
5. x,y:T. (x R^n-1^-1 y)  (x R^-1^n-1 y)
  x,y:T. (x R^n^-1 y)  (x R^-1^n y)
12 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(14steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Search Doc

1	1. T : Type 2. R : TTProp x,y:T. (x R^0^-1 y) (x R^-1^0 y)	1 step
2	1. T : Type 2. R : TTProp 3. n : 4. 0<n 5. x,y:T. (x R^n-1^-1 y) (x R^-1^n-1 y) x,y:T. (x R^n^-1 y) (x R^-1^n y)	12 steps