304 lines
7.5 KiB
Common Lisp
304 lines
7.5 KiB
Common Lisp
|
; December 7, 2001
|
||
|
|
||
|
; See the paper "Solutions of the Robbins Problem" by William McCune.
|
||
|
|
||
|
; Robbins equation (7)
|
||
|
|
||
|
(setq E7 (eq (n (sum (n (sum (n x) y)) (n (sum x y)))) y))
|
||
|
|
||
|
; From this derive the following:
|
||
|
|
||
|
; n(n(3x)+x)+2x = 2x
|
||
|
|
||
|
; STEP 10 ---------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x be n(x)+y and y be n(x+y)
|
||
|
|
||
|
(setq E10 (subst Y y E7))
|
||
|
|
||
|
(setq E10 (subst (sum (n x) y) x E10))
|
||
|
|
||
|
(setq E10 (eval (subst (n (sum x y)) Y E10)))
|
||
|
|
||
|
; simplify with (7)
|
||
|
|
||
|
(setq E10 (eval (subst (caddr E7) (cadr E7) E10)))
|
||
|
|
||
|
; n(n(n(x+y)+n(x)+y)+y) = n(x+y) ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum (n (sum x y)) (n x) y)) y)) (n (sum x y))))
|
||
|
|
||
|
(equal E10 tmp)
|
||
|
|
||
|
; STEP 11 ---------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let y be n(n(x)+y) and x be x+y
|
||
|
|
||
|
(setq E11 (subst X x E7))
|
||
|
|
||
|
(setq E11 (subst (n (sum (n x) y)) y E11))
|
||
|
|
||
|
(setq E11 (eval (subst (sum x y) X E11)))
|
||
|
|
||
|
; simplify with (7)
|
||
|
|
||
|
(setq E11 (eval (subst (caddr E7) (cadr E7) E11)))
|
||
|
|
||
|
; n(n(n(n(x)+y)+x+y)+y) = n(n(x)+y) ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum (n (sum (n x) y)) x y)) y)) (n (sum (n x) y))))
|
||
|
|
||
|
(equal E11 tmp)
|
||
|
|
||
|
; STEP 29 ---------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x be n(n(x)+y)+x+y and y be y
|
||
|
|
||
|
(setq E29 (eval (subst (sum (n (sum (n x) y)) x y) x E7)))
|
||
|
|
||
|
; simplify with (11)
|
||
|
|
||
|
(setq E29 (eval (subst (caddr E11) (cadr E11) E29)))
|
||
|
|
||
|
; n(n(n(n(x)+y)+x+2y)+n(n(x)+y)) = y ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum (n (sum (n x) y)) x y y)) (n (sum (n x) y)))) y))
|
||
|
|
||
|
(equal E29 tmp)
|
||
|
|
||
|
; STEP 54 ---------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x be n(n(n(x)+y)+x+2y)+n(n(x)+y) and y be z
|
||
|
|
||
|
(setq E54 (subst z y E7))
|
||
|
|
||
|
(setq tmp (sum (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y (n x)))))
|
||
|
|
||
|
(setq E54 (eval (subst tmp x E54)))
|
||
|
|
||
|
; simplify with (29)
|
||
|
|
||
|
(setq E54 (eval (subst (caddr E29) (cadr E29) E54)))
|
||
|
|
||
|
; n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+z)+n(y+z)) = z ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum y z)) (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y (n x))))))) z))
|
||
|
|
||
|
(equal E54 tmp)
|
||
|
|
||
|
; STEP 217 --------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x be n(n(n(x)+y)+x+2y)+n(n(x)+y)+z and y be n(y+z)
|
||
|
|
||
|
(setq E217 (subst Y y E7))
|
||
|
|
||
|
(setq tmp (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y (n x)))))
|
||
|
|
||
|
(setq E217 (subst tmp x E217))
|
||
|
|
||
|
(setq E217 (eval (subst (n (sum y z)) Y E217)))
|
||
|
|
||
|
; simplify with E54
|
||
|
|
||
|
(setq E217 (eval (subst (caddr E54) (cadr E54) E217)))
|
||
|
|
||
|
; n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z) = n(y+z) ?
|
||
|
|
||
|
(setq tmp (eq (n (sum z (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y z)) (n (sum y (n x))))))) (n (sum y z))))
|
||
|
|
||
|
(equal E217 tmp)
|
||
|
|
||
|
; STEP 674 --------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let y be u and x be n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z
|
||
|
|
||
|
(setq E674 (subst u y E7))
|
||
|
|
||
|
(setq tmp (sum z (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y z)) (n (sum y (n x)))))))
|
||
|
|
||
|
(setq E674 (eval (subst tmp x E674)))
|
||
|
|
||
|
; simplify with E217
|
||
|
|
||
|
(setq E674 (eval (subst (caddr E217) (cadr E217) E674)))
|
||
|
|
||
|
; n(n(n(n(n(n(x)+y)+x+2y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u)) = u ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum u z (n (sum z (n (sum x (n (sum y (n x))) (product 2 y))) (n (sum y z)) (n (sum y (n x))))))) (n (sum u (n (sum y z)))))) u))
|
||
|
|
||
|
(equal E674 tmp)
|
||
|
|
||
|
; STEP 6736 -------------------------------------------------------------------
|
||
|
|
||
|
; with (10), let x be 3v and y be n(n(3v)+v)+2v
|
||
|
|
||
|
(setq E10p (subst (product 3 v) x E10))
|
||
|
|
||
|
(setq tmp (sum (n (sum v (n (product 3 v)))) (product 2 v)))
|
||
|
|
||
|
(setq E10p (eval (subst tmp y E10p)))
|
||
|
|
||
|
; with (674), let x be 3v, y be v, z be 2v, and u be n(n(3v)+v)
|
||
|
|
||
|
(setq E674p (subst (product 3 v) x E674))
|
||
|
|
||
|
(setq E674p (subst v y E674p))
|
||
|
|
||
|
(setq E674p (subst (product 2 v) z E674p))
|
||
|
|
||
|
(setq tmp (n (sum v (n (product 3 v)))))
|
||
|
|
||
|
(setq E674p (eval (subst tmp u E674p)))
|
||
|
|
||
|
; simplify with (10')
|
||
|
|
||
|
(setq E6736 (eval (subst (caddr E10p) (cadr E10p) E674p)))
|
||
|
|
||
|
; replace v with x
|
||
|
|
||
|
(setq E6736 (eval (subst x v E6736)))
|
||
|
|
||
|
; n(n(n(n(3x)+x)+n(3x))+n(n(n(3x)+x)+5x)) = n(n(3x)+x) ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))))) (n (sum (n (sum x (n (product 3 x)))) (product 5 x))))) (n (sum x (n (product 3 x))))))
|
||
|
|
||
|
(equal E6736 tmp)
|
||
|
|
||
|
; STEP 8855 -------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x be n(n(3x)+x)+n(3x) and y be n(n(n(3x)+x)+5x)
|
||
|
|
||
|
(setq E8855 (subst Y y E7))
|
||
|
|
||
|
(setq tmp (sum (n (product 3 x)) (n (sum x (n (product 3 x))))))
|
||
|
|
||
|
(setq E8855 (subst tmp x E8855))
|
||
|
|
||
|
(setq tmp (n (sum (n (sum x (n (product 3 x)))) (product 5 x))))
|
||
|
|
||
|
(setq E8855 (eval (subst tmp Y E8855)))
|
||
|
|
||
|
; simplify with (6736)
|
||
|
|
||
|
(setq E8855 (eval (subst (caddr E6736) (cadr E6736) E8855)))
|
||
|
|
||
|
; n(n(n(3x)+x)+n(n(n(3x)+x)+n(3x)+n(n(n(3x)+x)+5x))) = n(n(n(3x)+x)+5x) ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum x (n (product 3 x)))) (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))) (n (sum (n (sum x (n (product 3 x)))) (product 5 x))))))) (n (sum (n (sum x (n (product 3 x)))) (product 5 x)))))
|
||
|
|
||
|
(equal E8855 tmp)
|
||
|
|
||
|
; with (54), let x be 3x, z be n(3x), and y be x
|
||
|
|
||
|
(setq tmp (subst (product 3 x) x E54))
|
||
|
|
||
|
(setq tmp (subst (n (product 3 x)) z tmp))
|
||
|
|
||
|
(setq tmp (eval (subst x y tmp)))
|
||
|
|
||
|
; simplify
|
||
|
|
||
|
(setq E8855 (subst (caddr tmp) (cadr tmp) E8855))
|
||
|
|
||
|
; flip
|
||
|
|
||
|
(setq E8855 (eq (caddr E8855) (cadr E8855)))
|
||
|
|
||
|
; n(n(n(3x)+x)+5x) = n(3x) ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum x (n (product 3 x)))) (product 5 x))) (n (product 3 x))))
|
||
|
|
||
|
(equal E8855 tmp)
|
||
|
|
||
|
; STEP 8865 -------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let y be n(n(3x)+x)+2x and x be 3x
|
||
|
|
||
|
(setq E8865 (subst X x E7))
|
||
|
|
||
|
(setq tmp (sum (n (sum x (n (product 3 x)))) (product 2 x)))
|
||
|
|
||
|
(setq E8865 (subst tmp y E8865))
|
||
|
|
||
|
(setq E8865 (eval (subst (product 3 x) X E8865)))
|
||
|
|
||
|
; simplify with (8855)
|
||
|
|
||
|
(setq E8865 (subst (caddr E8855) (cadr E8855) E8865))
|
||
|
|
||
|
(setq E8865 (eval E8865))
|
||
|
|
||
|
; n(n(n(n(3x)+x)+n(3x)+2x)+n(3x)) = n(n(3x)+x)+2x ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (product 3 x)) (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))) (product 2 x))))) (sum (n (sum x (n (product 3 x)))) (product 2 x))))
|
||
|
|
||
|
(equal E8865 tmp)
|
||
|
|
||
|
; STEP 8866 -------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x be n(n(3x)+x)+4x and y be x
|
||
|
|
||
|
(setq tmp (sum (n (sum x (n (product 3 x)))) (product 4 x)))
|
||
|
|
||
|
(setq A2 (subst tmp x E7))
|
||
|
|
||
|
(setq A2 (eval (subst x y A2)))
|
||
|
|
||
|
; simplify with (8855)
|
||
|
|
||
|
(setq A2 (eval (subst (caddr E8855) (cadr E8855) A2)))
|
||
|
|
||
|
; with (11), let x be 3x and y be x
|
||
|
|
||
|
(setq A3 (subst (product 3 x) x E11))
|
||
|
|
||
|
(setq A3 (eval (subst x y A3)))
|
||
|
|
||
|
; simplify A2 with A3
|
||
|
|
||
|
(setq E8866 (eval (subst (caddr A3) (cadr A3) A2)))
|
||
|
|
||
|
; n(n(n(3x)+x)+n(3x)) = x ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (product 3 x)) (n (sum x (n (product 3 x)))))) x))
|
||
|
|
||
|
(equal E8866 tmp)
|
||
|
|
||
|
; STEP 8870 -------------------------------------------------------------------
|
||
|
|
||
|
; with (7), let x = n(n(3x)+x)+n(3x)
|
||
|
|
||
|
(setq tmp (sum (n (product 3 x)) (n (sum x (n (product 3 x))))))
|
||
|
|
||
|
(setq E8870 (eval (subst tmp x E7)))
|
||
|
|
||
|
; simplify with (8866)
|
||
|
|
||
|
(setq E8870 (eval (subst (caddr E8866) (cadr E8866) E8870)))
|
||
|
|
||
|
; n(n(n(n(3x)+x)+n(3x)+y)+n(x+y)) = y ?
|
||
|
|
||
|
(setq tmp (eq (n (sum (n (sum x y)) (n (sum y (n (product 3 x)) (n (sum x (n (product 3 x)))))))) y))
|
||
|
|
||
|
(equal E8870 tmp)
|
||
|
|
||
|
; STEP 8871 -------------------------------------------------------------------
|
||
|
|
||
|
; with (8870), let y be 2x
|
||
|
|
||
|
(setq tmp (eval (subst (product 2 x) y E8870)))
|
||
|
|
||
|
; use to simplify (8865)
|
||
|
|
||
|
(setq E8871 (eval (subst (caddr tmp) (cadr tmp) E8865)))
|
||
|
|
||
|
; flip
|
||
|
|
||
|
(setq E8871 (eq (caddr E8871) (cadr E8871)))
|
||
|
|
||
|
; n(n(3x)+x)+2x = 2x ?
|
||
|
|
||
|
(setq tmp (eq (sum (n (sum x (n (product 3 x)))) (product 2 x)) (product 2 x)))
|
||
|
|
||
|
(equal E8871 tmp)
|