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

At: fun-graph-rel-graph 3 2 1
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. b: AA
7. b1:B. 2of(b) = f(1of(b),b1)
a:(AB). < 1of(a),f(1of(a),2of(a)) > = b {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }
By: ((Analyze -2) THEN (All Reduce) THEN ExRepD THEN (InstConcl [ < b1,b1@0 > ]) THEN (Reduce 0)) THENA (Auto THEN (Analyze -1) THEN (Reduce 0) THEN Analyze THEN (Reduce 0) THEN Obvious)
Generated subgoal:

16. b1: A
7. b2: A
8. b1@0: B
9. b2 = f(b1,b1@0)
< b1,f(b1,b1@0) > = < b1,b2 > {p:(AA)| b:B. 2of(p) = f(1of(p),b) A }		3 steps

About:
pairproductdecidablesetfunction
universeequalimpliesallexists

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