PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
rem
quo
unique
1
2
2
1
1
1.
n:
2.
r1:
n
3.
r2:
n
4.
q1:
5.
q2:
6.
q1
n+r2 = q2
n+r2
7.
r1 = r2
q1 = q2
By:
Inst
Thm*
a,b,n:
. a+n = b+n
a = b [q1
n;q2
n;r2]
Generated subgoal:
1
8.
q1
n = q2
n
q1 = q2
About:
n = q2n
q1 = q2
nnn+r2 = q2n+r2 q1 = q2
a,b,n:
. a+n = b+n 
a = b
[q1n;q2n;r2]n = q2n q1 = q2
