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