PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
rem
quo
unique
n:
, r1,r2:
n, q1,q2:
. r1+q1
n = r2+q2
n
r1 = r2 & q1 = q2
By:
UnivCD
Generated subgoal:
1
1.
n:
2.
r1:
n
3.
r2:
n
4.
q1:
5.
q2:
6.
r1+q1
n = r2+q2
n
r1 = r2 & q1 = q2
About:
nn
n = r2+q2n
r1 = r2 & q1 = q2 
n:, r1,r2:n, q1,q2:. r1+q1n = r2+q2n 
r1 = r2 & q1 = q2nnn = r2+q2n r1 = r2 & q1 = q2
