(4steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
intseg
shift
1
2
1.
a
:
2.
b
:
3.
a'
:
4.
b'
:
5.
b
-
a
=
b'
-
a'
6.
y
: {
a'
..
b'
}
(
x
.
x
+
a'
-
a
)((
x
.
x
+
a
-
a'
)(
y
)) =
y
By:
Compute (
x
.
x
+
a'
-
a
)((
x
.
x
+
a
-
a'
)(
y
)) *
(
x
.
x
+
a
-
a'
)(
y
)+
a'
-
a
*
y
+
a
-
a'
+
a'
-
a
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
}
(
x.x+a'-a)((
(
*
