(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
1
1.
a
:
2.
b
:
3.
a'
:
4.
b'
:
5.
b
-
a
=
b'
-
a'
6.
x
: {
a
..
b
}
(
x
.
x
+
a
-
a'
)((
x
.
x
+
a'
-
a
)(
x
)) =
x
By:
Compute (
x
.
x
+
a
-
a'
)((
x
.
x
+
a'
-
a
)(
x
)) *
(
x
.
x
+
a'
-
a
)(
x
)+
a
-
a'
*
x
+
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')((
(
*
