PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
rem
quo
unique
1
2
2
1
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.
n
q1 = n
q2
q1 = q2
By:
Inst
Thm*
a,b:
, n:
. n
a = n
b
a = b [q1;q2;n]
Generated subgoals:
None
About:
nn
n+r2 = q2n+r2q1 = nq2
q1 = q2
a,b:
, n:
. na = nb 
a = b
[q1;q2;n]
