gomu/ext/garside/check

#*******************
#* Artin of type A *
#*******************

# Garside element

ArtinA.garside_element(0)==a0
Delta1=ArtinA.garside_element(1)
Delta2=ArtinA.garside_element(2)
Delta3=ArtinA.garside_element(3)
Delta4=ArtinA.garside_element(4)
Delta1==a1
Delta2==a1*a2*Delta1
Delta3==a1*a2*a3*Delta2
Delta4==a1*a2*a3*a4*Delta3


#******************
#* Dual of type A *
#******************

# Left complement

DualA.left_complement(a12,a12)==a00
DualA.left_complement(a12,a23)==a13
DualA.left_complement(a12,a34)==a34
DualA.left_complement(a12,a24)==a14
DualA.left_complement(a12,a14)==a14
DualA.left_complement(a23,a12)==a12
DualA.left_complement(a23,a23)==a00
DualA.left_complement(a23,a13)==a12
DualA.left_complement(a23,a34)==a24
DualA.left_complement(a23,a24)==a24
DualA.left_complement(a23,a14)==a14
DualA.left_complement(a13,a12)==a23
DualA.left_complement(a13,a23)==a23
DualA.left_complement(a13,a13)==a00
DualA.left_complement(a13,a34)==a14
DualA.left_complement(a13,a24)==a23*a14
DualA.left_complement(a13,a14)==a14
DualA.left_complement(a34,a12)==a12
DualA.left_complement(a34,a23)==a23
DualA.left_complement(a34,a13)==a13
DualA.left_complement(a34,a34)==a00
DualA.left_complement(a34,a24)==a23
DualA.left_complement(a34,a14)==a13
DualA.left_complement(a24,a12)==a12
DualA.left_complement(a24,a23)==a34
DualA.left_complement(a24,a13)==a34*a12
DualA.left_complement(a24,a34)==a34
DualA.left_complement(a24,a24)==a00
DualA.left_complement(a24,a14)==a12
DualA.left_complement(a14,a12)==a24
DualA.left_complement(a14,a23)==a23
DualA.left_complement(a14,a13)==a34
DualA.left_complement(a14,a34)==a34
DualA.left_complement(a14,a24)==a24
DualA.left_complement(a14,a14)==a00

# Right complement

DualA.right_complement(a12,a12)==a00
DualA.right_complement(a12,a23)==a23
DualA.right_complement(a12,a13)==a23
DualA.right_complement(a12,a34)==a34
DualA.right_complement(a12,a24)==a24
DualA.right_complement(a12,a14)==a24
DualA.right_complement(a23,a12)==a13
DualA.right_complement(a23,a23)==a00
DualA.right_complement(a23,a13)==a13
DualA.right_complement(a23,a34)==a34
DualA.right_complement(a23,a24)==a34
DualA.right_complement(a23,a14)==a14
DualA.right_complement(a13,a12)==a12
DualA.right_complement(a13,a23)==a12
DualA.right_complement(a13,a13)==a00
DualA.right_complement(a13,a34)==a34
DualA.right_complement(a13,a24)==a34*a12
DualA.right_complement(a13,a14)==a34
DualA.right_complement(a34,a12)==a12
DualA.right_complement(a34,a23)==a24
DualA.right_complement(a34,a13)==a14
DualA.right_complement(a34,a34)==a00
DualA.right_complement(a34,a24)==a24
DualA.right_complement(a34,a14)==a14
DualA.right_complement(a24,a12)==a14
DualA.right_complement(a24,a23)==a23
DualA.right_complement(a24,a13)==a23*a14
DualA.right_complement(a24,a34)==a23
DualA.right_complement(a24,a24)==a00
DualA.right_complement(a24,a14)==a14
DualA.right_complement(a14,a12)==a12
DualA.right_complement(a14,a23)==a23
DualA.right_complement(a14,a13)==a13
DualA.right_complement(a14,a34)==a13
DualA.right_complement(a14,a24)==a12
DualA.right_complement(a14,a14)==a00

# Garside structure

DualA.left_lcm_complement(a12,a23)==a13
DualA.left_lcm_complement(a12,a12*a23)==a13
DualA.left_lcm_complement(a12,a23*a12)==a23

DualA.left_lcm(a12,a23)==a13*a12
DualA.left_lcm(a12,a12*a23)==a13*a12
DualA.left_lcm(a12,a23*a12)==a23*a12

DualA.right_lcm_complement(a12,a23)==a23
DualA.right_lcm_complement(a12,a12*a23)==a23
DualA.right_lcm_complement(a12,a23*a12)==a23*a12

DualA.right_lcm(a12,a23)==a12*a23
DualA.right_lcm(a12,a12*a23)==a12*a23
DualA.right_lcm(a12,a23*a12)==a12*a23*a12

DualA.left_gcd(a12,a12*a23)==a12
DualA.left_gcd(a12,a23*a12)==a00
DualA.left_gcd(a12*a23,a12*a12*a23)==a12*a23

DualA.right_gcd(a12,a12*a23)==a12
DualA.right_gcd(a12,a23*a12)==a12
DualA.right_gcd(a12*a23,a12*a12*a23)==a12*a23

DualA.left_gcd_x(a12*a23*a34,a12*a23*a12)==(a12*a23,a34)
DualA.left_gcd_x(a12*a23*a12,a12*a23*a34)==(a12*a23,a12)

DualA.right_gcd_x(a12*a23*a34,a12*a23*a12)==(a12*a23,a14)
DualA.right_gcd_x(a12*a23*a12,a12*a23*a34)==(a13*a12,a23)

DualA.is_left_divisible(a12*a23,a12)
DualA.is_left_divisible(a12*a23,a23)
DualA.is_left_divisible(a12*a23,a13)
DualA.is_left_divisible(a12*a23,a14)==false
DualA.is_left_divisible(a12*a23,a12*a12)==false

DualA.is_right_divisible(a12*a23,a12)
DualA.is_right_divisible(a12*a23,a23)
DualA.is_right_divisible(a12*a23,a13)
DualA.is_right_divisible(a12*a23,a14)==false
DualA.is_right_divisible(a12*a23,a12*a12)==false

DualA.is_left_divisible_x(a12*a23,a12)==(true,a23)
DualA.is_left_divisible_x(a12*a23,a23)==(true,a13)
DualA.is_left_divisible_x(a12*a23,a13)==(true,a12)
DualA.is_left_divisible_x(a12*a23,a14)==(false,a00)
DualA.is_left_divisible_x(a12*a23,a12*a12)==(false,a00)

DualA.is_right_divisible_x(a12*a23,a12)==(true,a13)
DualA.is_right_divisible_x(a12*a23,a23)==(true,a12)
DualA.is_right_divisible_x(a12*a23,a13)==(true,a23)
DualA.is_right_divisible_x(a12*a23,a14)==(false,a00)
DualA.is_right_divisible_x(a12*a23,a12*a12)==(false,a00)

# Garise automorphism
DualA.phi(2,a12)==a23
DualA.phi(2,a23)==a13
DualA.phi(2,a13)==a12
DualA.phi(2,a12,2)==a13
DualA.phi(2,a23,2)==a12
DualA.phi(2,a13,2)==a23
DualA.phi(2,a12,-1)==a13
DualA.phi(2,a23,-1)==a12
DualA.phi(2,a13,-1)==a23
DualA.phi(2,a12,-4)==a13
DualA.phi(2,a23,-4)==a12
DualA.phi(2,a13,-4)==a23
DualA.phi(2,A12)==A23
DualA.phi(2,A23)==A13
DualA.phi(2,A13)==A12
DualA.phi(2,a12*A13)==a23*A12

# Garside element

DualA.garside_element(0)==a00
delta1=DualA.garside_element(1)
delta2=DualA.garside_element(2)
delta3=DualA.garside_element(3)
delta4=DualA.garside_element(4)
delta1==a12
delta2==delta1*a23
delta3==delta2*a34
delta4==delta3*a45

# phi-tail
DualA.phi_tail(1,delta2)==delta1
DualA.phi_tail(2,delta3)==delta2
DualA.phi_tail(3,delta4)==delta3
DualA.phi_tail(1,delta2*delta2)==delta1*delta1
DualA.phi_tail(2,delta3*delta3)===delta2*delta2
DualA.phi_tail(3,delta4*delta4)===delta3*delta3

# phi-splitting
DualA.phi_splitting(1,delta2)==[a12,a00,delta1]
DualA.phi_splitting(1,delta2*delta2)==[a12,a12,a00,delta1*delta1]
DualA.phi_splitting(2,a12)==[a12]
DualA.phi_splitting(2,a23)==[a23]
DualA.phi_splitting(2,a13)==[a13]
DualA.phi_splitting(2,a34)==[a23,a00]
DualA.phi_splitting(2,a24)==[a13,a00]
DualA.phi_splitting(2,a14)==[a23,a00,a00]
DualA.phi_splitting(2,delta3)==[a23,a00,delta2]

# phi-normal-form
DualA.phi_normal_form(delta3*delta3)==a12*a14*a12*a13*a12*a12