Initial program 60.7
\[1 - \log \left(1 - \frac{x - y}{1 - y}\right)
\]
Taylor expanded in y around inf 0.4
\[\leadsto 1 - \log \color{blue}{\left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)}
\]
Applied *-un-lft-identity_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{\color{blue}{1 \cdot {y}^{2}}}\right)\right)\right)
\]
Applied *-un-lft-identity_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{\color{blue}{1 \cdot 1}}{1 \cdot {y}^{2}}\right)\right)\right)
\]
Applied times-frac_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \color{blue}{\frac{1}{1} \cdot \frac{1}{{y}^{2}}}\right)\right)\right)
\]
Applied *-un-lft-identity_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\frac{1}{\color{blue}{1 \cdot {y}^{3}}} + \frac{1}{1} \cdot \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied *-un-lft-identity_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\frac{\color{blue}{1 \cdot 1}}{1 \cdot {y}^{3}} + \frac{1}{1} \cdot \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied times-frac_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \left(\color{blue}{\frac{1}{1} \cdot \frac{1}{{y}^{3}}} + \frac{1}{1} \cdot \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied distribute-lft-out_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{y} + \color{blue}{\frac{1}{1} \cdot \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)}\right)\right)
\]
Applied *-un-lft-identity_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{1}{\color{blue}{1 \cdot y}} + \frac{1}{1} \cdot \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied *-un-lft-identity_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\frac{\color{blue}{1 \cdot 1}}{1 \cdot y} + \frac{1}{1} \cdot \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied times-frac_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \left(\color{blue}{\frac{1}{1} \cdot \frac{1}{y}} + \frac{1}{1} \cdot \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied distribute-lft-out_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \frac{x}{{y}^{2}}\right)\right) - \color{blue}{\frac{1}{1} \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)}\right)
\]
Applied div-inv_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\frac{x}{{y}^{3}} + \color{blue}{x \cdot \frac{1}{{y}^{2}}}\right)\right) - \frac{1}{1} \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied div-inv_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \left(\color{blue}{x \cdot \frac{1}{{y}^{3}}} + x \cdot \frac{1}{{y}^{2}}\right)\right) - \frac{1}{1} \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied distribute-lft-out_binary640.4
\[\leadsto 1 - \log \left(\left(\frac{x}{y} + \color{blue}{x \cdot \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)}\right) - \frac{1}{1} \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied div-inv_binary640.4
\[\leadsto 1 - \log \left(\left(\color{blue}{x \cdot \frac{1}{y}} + x \cdot \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right) - \frac{1}{1} \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied distribute-lft-out_binary640.4
\[\leadsto 1 - \log \left(\color{blue}{x \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)} - \frac{1}{1} \cdot \left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right)\right)
\]
Applied distribute-rgt-out--_binary640.4
\[\leadsto 1 - \log \color{blue}{\left(\left(\frac{1}{y} + \left(\frac{1}{{y}^{3}} + \frac{1}{{y}^{2}}\right)\right) \cdot \left(x - \frac{1}{1}\right)\right)}
\]