(7steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
delete
k
:
,
j
:
k
,
m
:
.
m
=
k
-1
({
i
:
k
|
i
=
j
} ~
m
)
By:
Auto
Generated subgoal:
1
1.
k
:
2.
j
:
k
3.
m
:
4.
m
=
k
-1
{
i
:
k
|
i
=
j
} ~
m
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
k:
, j:k, m:. m = k-1 
({i:k| 
i = j } ~ m) k:, j:k, m:. m = k-1 ({i:k| i = j } ~ m)
k
{i:k| i = j } ~ m
