(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
addition
1
1
1
1
2
1.
i:
2.
j:
3.
n:
0
(i
n)+(j
n)
By:
Inst
Thm*
a:
, n:
. 0
(a
n) [i;n]
THEN
Inst
Thm*
a:
, n:
. 0
(a
n) [j;n]
Generated subgoal:
1
4.
0
(i
n)
5.
0
(j
n)
0
(i
n)+(j
n)
About:
(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(i 
n)(j n)
0(i n)+(j n)
0(i n)+(j n)
a:, n:. 0(a n)
[i;n]
a:, n:. 0(a n)
[j;n](i n)(j n) 0(i n)+(j n)
