PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
n
unique
1
1.
q:
2.
n:
3.
i:
4.
r1:
(q
n)
5.
r2:
(q
n+i)
6.
(q
n
)+r1 =
(q
n+i
)+r2
False
By:
Inst
Thm*
q,n:
, i:
.
(q
n
)+(q
n)
(q
n+i
) [q;n;i]
Generated subgoal:
1
7.
(q
n
)+(q
n)
(q
n+i
)
False
About:
(q
n
)+(qn)
(qn+i)
False
(qn)(qn+i)(qn)+r1 = (qn+i)+r2 False
q,n:, i:. (qn)+(qn)(qn+i)
[q;n;i](qn)+(qn)(qn+i) False
