Nuprl - Pf list_quo_choice

PrintForm Definitions automata 5 Sections AutomataTheory Doc

1. q:
2. E: q*q*Prop
3. EquivRel x,y:q*. x E y
4. x,y:q*. Dec(x E y)
5. f: q*
6. g: q*
7. g o f = Id
8. f o g = Id

h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))

By: Inst Thm* E:(Prop). (EquivRel x,y:. x E y) & (x,y:. Dec(x E y)) (h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))) [x,y. (g(x)) E (g(y))]

Generated subgoals:

1 (EquivRel x,y:. x (x,y. (g(x)) E (g(y))) y) & (x,y:. Dec(x (x,y. (g(x)) E (g(y))) y))

2 9. h:(). (n,k:. (n (x,y. (g(x)) E (g(y))) k) h(n) = h(k)) & (n:. n (x,y. (g(x)) E (g(y))) (h(n)))
h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))

About:

1	`(EquivRel x,y:. x (x,y. (g(x)) E (g(y))) y) & (x,y:. Dec(x (x,y. (g(x)) E (g(y))) y))`
2	9. `h:(). (n,k:. (n (x,y. (g(x)) E (g(y))) k) h(n) = h(k)) & (n:. n (x,y. (g(x)) E (g(y))) (h(n)))` `h:(qq). (x,y:q. (x E y) h(x) = h(y)) & (x:q. x E (h(x)))`