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