(9steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
mul
a
,
b
,
c
:
.
a
b
=
c
((
a
b
) ~
c
)
By:
NatInd Concl
Generated subgoals:
1
1.
b
:
2.
c
:
3. 0
b
=
c
(
0
b
) ~
c
3
steps
2
1.
a
:
2. 0<
a
3.
b
,
c
:
. (
a
-1)
b
=
c
((
(
a
-1)
b
) ~
c
)
4.
b
:
5.
c
:
6.
a
b
=
c
(
a
b
) ~
c
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
a,b,c:
. a
b = c 
((a
b) ~ c) a,b,c:. ab = c ((ab) ~ c)
b = c
(0b) ~ c
b,c:. (a-1)b = c (((a-1)b) ~ c)
b = c
(ab) ~ c
