(7steps total)
PrintForm
Definitions
Lemmas
rat
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
qadd
functionality
1
1
1.
p
:
2.
q
:
3.
r
:
4.
s
:
p
.num
q
.den =
q
.num
p
.den
r
.num
s
.den =
s
.num
r
.den
p
+q
r
.num
q
+q
s
.den =
q
+q
s
.num
p
+q
r
.den
By:
OnHyps [4;3;2;1] RatHD THEN RW (SweepDnC qnd_evalC) 0
Generated subgoal:
1
1.
p1
:
2.
p2
:
3.
q1
:
4.
q2
:
5.
r1
:
6.
r2
:
7.
s1
:
8.
s2
:
p1
q2
=
q1
p2
r1
s2
=
s1
r2
p1
/
p2
+q
r1
/
r2
.num
q1
/
q2
+q
s1
/
s2
.den =
q1
/
q2
+q
s1
/
s2
.num
p1
/
p2
+q
r1
/
r2
.den
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
rat
1
Sections
StandardLIB
Doc