PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
geom
unique
1
1
1.
q:
2.
n1:
3.
n2:
4.
r1:
(q
n1)
5.
r2:
(q
n2)
6.
(q
n1
)+r1 =
(q
n2
)+r2
n1 = n2
By:
Decide (n1 < n2)
Generated subgoals:
1
7.
n1 < n2
n1 = n2
2
7.
n1 < n2
n1 = n2
About:
n1 = n2
n1 < n2 n1 = n2
(q
n1)(qn2)
(qn1
)+r1 = (qn2)+r2 n1 = n2 n1 = n2n1 < n2 n1 = n2
