5th-root-of-unity.egi

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

def z := rtu 5

def a11 := z ^ 1 + z ^ 4

def a12 := z ^ 2 + z ^ 3

def b10 := a11 + a12

def b11 := a11 - a12

def b12 := a12 - a11

assertEqual "b10" b10 (-1)

def b10' := b10

def b11' := sqrt (b11 ^ 2)

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

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

def a21 := z ^ 1 - z ^ 4

def a22 := z ^ 2 - z ^ 3

def b20 := a21 + a22

def b21 := a21 - a22

def b22 := a22 - a21

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

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

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

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

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

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


z1'^5