5th-root-of-unity.egi

--
-- This file has been auto-generated by egison-translator.
--

def z : MathExpr := rtu 5

def a11 : MathExpr := z ^ 1 + z ^ 4

def a12 : MathExpr := z ^ 2 + z ^ 3

def b10 : MathExpr := a11 + a12

def b11 : MathExpr := a11 - a12

def b12 : MathExpr := a12 - a11

assertEqual "b10" b10 (-1)

def b10' : MathExpr := b10

def b11' : MathExpr := sqrt (b11 ^ 2)

def a11' : MathExpr := (b10' + b11') / 2

def a12' : MathExpr := (b10' - b11') / 2

def a21 : MathExpr := z ^ 1 - z ^ 4

def a22 : MathExpr := z ^ 2 - z ^ 3

def b20 : MathExpr := a21 + a22

def b21 : MathExpr := a21 - a22

def b22 : MathExpr := a22 - a21

def b20' : MathExpr := sqrt ((-3) + 4 * a12')

def b21' : MathExpr := sqrt ((-3) + 4 * a11')

def a21' : MathExpr := (b20' + b21') / 2

def a22' : MathExpr := (b20' - b21') / 2

def z1' : MathExpr := (a11' + a21') / 2

assertEqual
  "5th-root-of-unity"
   z1'
  ((-1 + sqrt 5 + sqrt (-5 - 2 * sqrt 5) + sqrt (-5 + 2 * sqrt 5)) / 4)

--assertEqual "z1'^5 = 1"
--  (z1'^5)
--  1