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

At: fun-graph-rel-graph
A,B:Type, f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b))
By:
Auto
THEN
Unfolds [`graph-isomorphic`;`fun-graph`;`rel-graph`] 0
THEN
Reduce 0
THEN
InstConcl [Id;p. < 1of(p),f(1of(p),2of(p)) > ]
Generated subgoals:

11. 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. p: AB
< 1of(p),f(1of(p),2of(p)) > {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }		1 step
 
21. 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))
Bij(A; A; Id)		1 step
 
31. 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))
Bij(AB; {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }; p. < 1of(p),f(1of(p),2of(p)) > )		10 steps
 
41. 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))
(Id,Id) o p. < 1of(p),f(1of(p),2of(p)) > = Id o (p. < 1of(p),f(1of(p),2of(p)) > ) ABAA		1 step

About:
pairproductdecidablesetlambdafunction
universeequalmemberimpliesallexists

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