open-axiom repository from github
\begin{patch}{BinaryExpansionXmpPagePatch1}
\begin{paste}{BinaryExpansionXmpPageFull1}{BinaryExpansionXmpPageEmpty1}
\pastebutton{BinaryExpansionXmpPageFull1}{\hidepaste}
\tab{5}\spadcommand{r := binary(22/7)\bound{r }}
\indentrel{3}\begin{verbatim}
___
(1) 11.001
Type: BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty1}
\begin{paste}{BinaryExpansionXmpPageEmpty1}{BinaryExpansionXmpPagePatch1}
\pastebutton{BinaryExpansionXmpPageEmpty1}{\showpaste}
\tab{5}\spadcommand{r := binary(22/7)\bound{r }}
\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPagePatch2}
\begin{paste}{BinaryExpansionXmpPageFull2}{BinaryExpansionXmpPageEmpty2}
\pastebutton{BinaryExpansionXmpPageFull2}{\hidepaste}
\tab{5}\spadcommand{r + binary(6/7)\free{r }}
\indentrel{3}\begin{verbatim}
(2) 100
Type: BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty2}
\begin{paste}{BinaryExpansionXmpPageEmpty2}{BinaryExpansionXmpPagePatch2}
\pastebutton{BinaryExpansionXmpPageEmpty2}{\showpaste}
\tab{5}\spadcommand{r + binary(6/7)\free{r }}
\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPagePatch3}
\begin{paste}{BinaryExpansionXmpPageFull3}{BinaryExpansionXmpPageEmpty3}
\pastebutton{BinaryExpansionXmpPageFull3}{\hidepaste}
\tab{5}\spadcommand{[binary(1/i) for i in 102..106]}
\indentrel{3}\begin{verbatim}
(3)
________
[0.000000101,
___________________________________________________
0.000000100111110001000101100101111001110010010101001,
____________ ____________
0.000000100111011, 0.000000100111,
0.0
OVERBAR
00000100110101001000011100111110110010101101111
00011
]
Type: List BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty3}
\begin{paste}{BinaryExpansionXmpPageEmpty3}{BinaryExpansionXmpPagePatch3}
\pastebutton{BinaryExpansionXmpPageEmpty3}{\showpaste}
\tab{5}\spadcommand{[binary(1/i) for i in 102..106]}
\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPagePatch4}
\begin{paste}{BinaryExpansionXmpPageFull4}{BinaryExpansionXmpPageEmpty4}
\pastebutton{BinaryExpansionXmpPageFull4}{\hidepaste}
\tab{5}\spadcommand{binary(1/1007)}
\indentrel{3}\begin{verbatim}
(4)
0.
OVERBAR
0000000001000001000101001001011110000011111100001
01111110010110001111101000100111001001100110001
10010010101011110110100110000000011000011001111
01110001101000101111010010001111011000010101110
11100111010101110011001010010111000000011100011
11001000000100100100110111001010100111010001101
11011010111000100100000110010110110000001011001
01111100010100000101010101101011000001101101110
10010101111111010111010100110010000101001101100
0100110001000100001000011000111010011110001
Type: BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty4}
\begin{paste}{BinaryExpansionXmpPageEmpty4}{BinaryExpansionXmpPagePatch4}
\pastebutton{BinaryExpansionXmpPageEmpty4}{\showpaste}
\tab{5}\spadcommand{binary(1/1007)}
\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPagePatch5}
\begin{paste}{BinaryExpansionXmpPageFull5}{BinaryExpansionXmpPageEmpty5}
\pastebutton{BinaryExpansionXmpPageFull5}{\hidepaste}
\tab{5}\spadcommand{p := binary(1/4)*x**2 + binary(2/3)*x + binary(4/9)\bound{p }}
\indentrel{3}\begin{verbatim}
2 __ ______
(5) 0.01x + 0.10x + 0.011100
Type: Polynomial BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty5}
\begin{paste}{BinaryExpansionXmpPageEmpty5}{BinaryExpansionXmpPagePatch5}
\pastebutton{BinaryExpansionXmpPageEmpty5}{\showpaste}
\tab{5}\spadcommand{p := binary(1/4)*x**2 + binary(2/3)*x + binary(4/9)\bound{p }}
\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPagePatch6}
\begin{paste}{BinaryExpansionXmpPageFull6}{BinaryExpansionXmpPageEmpty6}
\pastebutton{BinaryExpansionXmpPageFull6}{\hidepaste}
\tab{5}\spadcommand{q := D(p, x)\free{p }\bound{q }}
\indentrel{3}\begin{verbatim}
__
(6) 0.1x + 0.10
Type: Polynomial BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty6}
\begin{paste}{BinaryExpansionXmpPageEmpty6}{BinaryExpansionXmpPagePatch6}
\pastebutton{BinaryExpansionXmpPageEmpty6}{\showpaste}
\tab{5}\spadcommand{q := D(p, x)\free{p }\bound{q }}
\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPagePatch7}
\begin{paste}{BinaryExpansionXmpPageFull7}{BinaryExpansionXmpPageEmpty7}
\pastebutton{BinaryExpansionXmpPageFull7}{\hidepaste}
\tab{5}\spadcommand{g := gcd(p, q)\free{p q }\bound{g }}
\indentrel{3}\begin{verbatim}
__
(7) x + 1.01
Type: Polynomial BinaryExpansion
\end{verbatim}
\indentrel{-3}\end{paste}\end{patch}
\begin{patch}{BinaryExpansionXmpPageEmpty7}
\begin{paste}{BinaryExpansionXmpPageEmpty7}{BinaryExpansionXmpPagePatch7}
\pastebutton{BinaryExpansionXmpPageEmpty7}{\showpaste}
\tab{5}\spadcommand{g := gcd(p, q)\free{p q }\bound{g }}
\end{paste}\end{patch}