PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
list
1
1
nat
1
1
1
2
1
1.
q:
2.
b:
a:
q*. enum(a) = b
By:
Inst
Thm*
q:
, a:
.
l:
q*. enum(l) = a [q;b]
Generated subgoal:
1
3.
l:
q*. enum(l) = b
a:
q*. enum(a) = b
About:
l:
q*. enum(l) = b
a:q*. enum(a) = b
a:q*. enum(a) = b
q:, a:. l:q*. enum(l) = a
[q;b]l:q*. enum(l) = b a:q*. enum(a) = b
