; An abstraction that takes two terms representing arbitrary, positive
; or negative, integers and returns the result of their division (the
; quotient).
; See lambda-arihtm-neg.scm for more details.

(L a (L b ((((a (L _ (((b (L _ (L c (L sign c)))) (L _ (L m (L sign (L
f (L x (sign ((m f) x)))))))) (L _ (L x (L y x)))))) (L _ (((b (L _ (L
m (L sign (L f (L x (sign ((m f) x)))))))) (L _ (L c (L sign c)))) (L
_ (L x (L y x)))))) (L _ (L sign (L f (L x x))))) (((((a (L x x)) (L u
((((u (L x (L y y))) (L x (L y x))) u) (((((((u (L x (L y x))) (L _
((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f)
x))))))) (L sign (L f (L x x)))) (L _ (L sign (L f (L x (sign ((((u (L
x (L y x))) (L x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign
(((b (L x x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) f)
x)))))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) (L a (((a (L _ (((((a
(L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g73 (L x (L
f (L x x))))) (L _ (L sign (L f (L x (sign (((((a (L x x)) (L z ((z (L
x x)) (L f (L x (f ((z f) x))))))) (L g74 (L x (L f (L x x))))) f)
x))))))) (L sign (L f (L x x)))))) (L _ (L sign (L f (L x (f (((a (L x
x)) f) x))))))) (L sign (L f f))))) (u (L x (L y x)))))) (u (L x (L y
x)))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L _ ((((u (L x (L y x))) (L x
x)) (L a (((a (L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z
f) x))))))) (L g73 (L x (L f (L x x))))) (L _ (L sign (L f (L x (sign
(((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g74
(L x (L f (L x x))))) f) x))))))) (L sign (L f (L x x)))))) (L _ (L
sign (L f (L x (f (((a (L x x)) f) x))))))) (L sign (L f f))))) (((b
(L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f) x))))))) (L
sign (L f (L x x))))))) (L _ (L sign (L f (L x ((((u (L x (L y x))) (L
x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x))
f) x))))))) (L sign (L f (L x x)))) (L x x)) f) x))))))) (u (L x (L y
x)))))) (((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f)
x))))))) (L sign (L f (L x x))))) (L _ (L p ((p ((((u (L x (L y x)))
(L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f)
x))))))) (L sign (L f (L x x)))) (L _ (L sign (L f (L x (sign ((((u (L
x (L y x))) (L x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign
(((b (L x x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) f)
x)))))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) (L a (((a (L _ (((((a
(L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g73 (L x (L
f (L x x))))) (L _ (L sign (L f (L x (sign (((((a (L x x)) (L z ((z (L
x x)) (L f (L x (f ((z f) x))))))) (L g74 (L x (L f (L x x))))) f)
x))))))) (L sign (L f (L x x)))))) (L _ (L sign (L f (L x (f (((a (L x
x)) f) x))))))) (L sign (L f f))))) (u (L x (L y x)))))) (u (L x (L y
x)))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L _ ((((u (L x (L y x))) (L x
x)) (L a (((a (L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z
f) x))))))) (L g73 (L x (L f (L x x))))) (L _ (L sign (L f (L x (sign
(((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g74
(L x (L f (L x x))))) f) x))))))) (L sign (L f (L x x)))))) (L _ (L
sign (L f (L x (f (((a (L x x)) f) x))))))) (L sign (L f f))))) (((b
(L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f) x))))))) (L
sign (L f (L x x))))))) (L _ (L sign (L f (L x ((((u (L x (L y x))) (L
x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x))
f) x))))))) (L sign (L f (L x x)))) (L x x)) f) x))))))) (u (L x (L y
x)))))) (((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f)
x))))))) (L sign (L f (L x x)))))) (L p ((p (L x (L y x))) ((u (L x (L
y y))) (L x (L y y))))))))) (L _ (L p ((p ((((u (L x (L y x))) (L _
((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f)
x))))))) (L sign (L f (L x x)))) (L _ (L sign (L f (L x (sign ((((u (L
x (L y x))) (L x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign
(((b (L x x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) f)
x)))))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) (L a (((a (L _ (((((a
(L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g73 (L x (L
f (L x x))))) (L _ (L sign (L f (L x (sign (((((a (L x x)) (L z ((z (L
x x)) (L f (L x (f ((z f) x))))))) (L g74 (L x (L f (L x x))))) f)
x))))))) (L sign (L f (L x x)))))) (L _ (L sign (L f (L x (f (((a (L x
x)) f) x))))))) (L sign (L f f))))) (u (L x (L y x)))))) (u (L x (L y
x)))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L _ ((((u (L x (L y x))) (L x
x)) (L a (((a (L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z
f) x))))))) (L g73 (L x (L f (L x x))))) (L _ (L sign (L f (L x (sign
(((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g74
(L x (L f (L x x))))) f) x))))))) (L sign (L f (L x x)))))) (L _ (L
sign (L f (L x (f (((a (L x x)) f) x))))))) (L sign (L f f))))) (((b
(L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f) x))))))) (L
sign (L f (L x x))))))) (L _ (L sign (L f (L x ((((u (L x (L y x))) (L
x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x))
f) x))))))) (L sign (L f (L x x)))) (L x x)) f) x))))))) (u (L x (L y
x)))))) (((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f)
x))))))) (L sign (L f (L x x)))))) (L p ((p (L x (L y y))) (L f (L x
(f ((((u (L x (L y y))) (L x (L y y))) f) x)))))))))) (L p ((p ((((u
(L x (L y x))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b
(L x x)) f) x))))))) (L sign (L f (L x x)))) (L _ (L sign (L f (L x
(sign ((((u (L x (L y x))) (L x x)) f) ((((((b (L x x)) (L _ (L sign
(L f (L x (sign (((b (L x x)) f) x))))))) (L sign (L f (L x x)))) (L x
x)) f) x)))))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign
(((b (L x x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) (L a (((a
(L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L
g73 (L x (L f (L x x))))) (L _ (L sign (L f (L x (sign (((((a (L x x))
(L z ((z (L x x)) (L f (L x (f ((z f) x))))))) (L g74 (L x (L f (L x
x))))) f) x))))))) (L sign (L f (L x x)))))) (L _ (L sign (L f (L x (f
(((a (L x x)) f) x))))))) (L sign (L f f))))) (u (L x (L y x)))))) (u
(L x (L y x)))))) (L _ ((((((b (L x x)) (L _ (L sign (L f (L x (sign
(((b (L x x)) f) x))))))) (L sign (L f (L x x)))) (L _ ((((u (L x (L y
x))) (L x x)) (L a (((a (L _ (((((a (L x x)) (L z ((z (L x x)) (L f (L
x (f ((z f) x))))))) (L g73 (L x (L f (L x x))))) (L _ (L sign (L f (L
x (sign (((((a (L x x)) (L z ((z (L x x)) (L f (L x (f ((z f) x)))))))
(L g74 (L x (L f (L x x))))) f) x))))))) (L sign (L f (L x x)))))) (L
_ (L sign (L f (L x (f (((a (L x x)) f) x))))))) (L sign (L f f)))))
(((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x)) f) x)))))))
(L sign (L f (L x x))))))) (L _ (L sign (L f (L x ((((u (L x (L y x)))
(L x x)) f) ((((((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x
x)) f) x))))))) (L sign (L f (L x x)))) (L x x)) f) x))))))) (u (L x
(L y x)))))) (((b (L x x)) (L _ (L sign (L f (L x (sign (((b (L x x))
f) x))))))) (L sign (L f (L x x)))))) (L p ((p (L x (L y x))) (L f (L
x (f ((((u (L x (L y y))) (L x (L y y))) f) x)))))))))))) (L p ((p (L
sign (a (L x x)))) (L p ((p (L x (L y y))) (L f (L x x))))))) (L x (L
y y))) (L x (L y y))))))