Nuprl - Proof: compose bij

(6steps total) PrintForm Definitions mb list 2 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: compose bij

T:Type, f,g:(T

T). Bij(T; T; f)

Bij(T; T; g)

Bij(T; T; f o g)

By:	Unfold `biject` 0 THEN Unfolds [`inject`;`surject`] 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. f : TT
3. g : TT
4. a1,a2:T. f(a1) = f(a2)  a1 = a2
5. b:T. a:T. f(a) = b
6. a1,a2:T. g(a1) = g(a2)  a1 = a2
7. b:T. a:T. g(a) = b
8. a1 : T
9. a2 : T
10. f(g(a1)) = f(g(a2))
  a1 = a2
1 step

2 1. T : Type
2. f : TT
3. g : TT
4. a1,a2:T. f(a1) = f(a2)  a1 = a2
5. b:T. a:T. f(a) = b
6. a1,a2:T. g(a1) = g(a2)  a1 = a2
7. b:T. a:T. g(a) = b
8. b : T
  a:T. f(g(a)) = b
4 steps

About:

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

(6steps total) PrintForm Definitions mb list 2 Sections MarkB generic Search Doc

1	1. T : Type 2. f : TT 3. g : TT 4. a1,a2:T. f(a1) = f(a2) a1 = a2 5. b:T. a:T. f(a) = b 6. a1,a2:T. g(a1) = g(a2) a1 = a2 7. b:T. a:T. g(a) = b 8. a1 : T 9. a2 : T 10. f(g(a1)) = f(g(a2)) a1 = a2	1 step
2	1. T : Type 2. f : TT 3. g : TT 4. a1,a2:T. f(a1) = f(a2) a1 = a2 5. b:T. a:T. f(a) = b 6. a1,a2:T. g(a1) = g(a2) a1 = a2 7. b:T. a:T. g(a) = b 8. b : T a:T. f(g(a)) = b	4 steps