Nuprl - Proof: fun-graph-rel-graph 3 1

(14steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1. A: Type
2. B: Type
3. f: ABA
4. a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2
5. a,a':A. Dec(b:B. a' = f(a,b))
6. a1: AB
7. a2: AB
8. < 1of(a1),f(1of(a1),2of(a1)) > = < 1of(a2),f(1of(a2),2of(a2)) > {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }

a1 = a2

By: Analyze -3 THEN Analyze -2 THEN All Reduce THEN Analyze -1 THEN Reduce -1

Generated subgoal:

1 6. a3: A
7. a4: B
8. a5: A
9. a6: B
10. < a3,f(a3,a4) > = < a5,f(a5,a6) >
11. b:B. f(a3,a4) = f(a3,b)
< a3,a4 > = < a5,a6 > 3 steps

About:

(14steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc