PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
rem
quo
unique
1
2
2
1
1
1
1.
n:
2.
r1:
n
3.
r2:
n
4.
q1:
5.
q2:
6.
q1
n+r2 = q2
n+r2
7.
r1 = r2
8.
q1
n = q2
n
q1 = q2
By:
RWH (LemmaC Thm*
a,b:
. a
b = b
a) 8
Generated subgoal:
1
8.
n
q1 = n
q2
q1 = q2
About:
q1 = nq2
q1 = q2
nnn+r2 = q2n+r2n = q2n q1 = q2
a,b:
. ab = ba) 8q1 = nq2 q1 = q2
