PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
unique
1
1
2
1
1.
q:
2.
n1:
3.
n2:
4.
r1:
(q
n1)
5.
r2:
(q
n2)
6.
(q
n1
)+r1 =
(q
n2
)+r2
7.
n1 < n2
8.
n1 > n2
n1 = n2
By:
Inst
Thm*
q:
, n:
, i:
, r1:
(q
n), r2:
(q
n+i).
(q
n
)+r1 =
(q
n+i
)+r2
False [q;n2;n1-n2;r2;r1]
Generated subgoals:
None
About:
(q
n1)(qn2)
(qn1
)+r1 = (qn2)+r2
n1 < n2
n1 = n2
q:, n:, i:, r1:(qn), r2:(qn+i).
(qn)+r1 = (qn+i)+r2 
False
[q;n2;n1-n2;r2;r1]