(and


(ite (= 2 {^ x 1|2}) (= 16 {^ x 2}) (not (= x 4)))
(ite (= 4|6 {^ x 1|2}) (= 16|81 {* {^ x 5|2} {^ {^ x -1|4} 2}}) (not (= x 4|9)))


(ite 
    (= {* {^ x 2} y z} {* {^ w -1} {^ v 3}}) 
    (= {* x {^ w 1|2}} {* {^ z -1|2} {^ y -1|2} {^ v 3|2}})
    true)




(ite p
    (= y {* (ite p 1 2) y})
    (= {* 2 y} {* (ite p 1 2) y}))


(= 
    {* {+ 1 {* 5 (ite p x y)}} {+ 3 {* 4 (ite q 2 4)}}}
    (ite
        p
	(ite 
            q
            {+ 11 {* 55 x}}
            {+ 19 {* 95 x}})
	(ite
            q
            {+ 11 {* 55 y}}
            {+ 19 {* 95 y}}))))