exponent
Sections
AutomataTheory
Doc
Def
enum(l) ==
(q
||l||
)+en(l)
Thm*
q:
, a:
.
l:
q*. enum(l) = a enum_surj
Thm*
q:
, l1,l2:
q*. enum(l1) = enum(l2)
l1 = l2 enum_inj
q:
, a:. 
l:q*. enum(l) = a enum_surj
(q
||l||
)+en(l)
q:, a:. l:q*. enum(l) = a enum_surj
q:, l1,l2:q*. enum(l1) = enum(l2) 
l1 = l2 enum_inj