# Expr is the function of n in terms of its side lengths.
import math
from sympy import symbols, expand
u_1,u_2,u_3,u_4,u_5,u_6,t_1,t_2,t_3,t_4,t_5,t_6=symbols('u_1,u_2,u_3,u_4,u_5,u_6,t_1,t_2,t_3,t_4,t_5,t_6')
expr1=(t_2+2*t_3+t_4+u_3+u_4+1)*(t_1+2*t_2+t_3+u_2+u_3+1)
expr2=(t_2+t_3+u_3+1)*(t_2+t_3+u_3)+(t_5+t_6+u_6+1)*(t_5+t_6+u_6)
expr3=(t_1+1)*t_1+(t_2+1)*t_2+(t_3+1)*t_3+(t_4+1)*t_4+(t_5+1)*t_5+(t_6+1)*t_6
expr=expr1-(1/2)*(expr2+expr3)
 
# A function that generates a list of the side lengths of all 12-gons with n vertices, 
# that have less than b boundary edges, and every boundary vertex has an interior angle of at least 90 degrees.
def case_compute(n,b):
    cases=[]
    # Computes parameters ui and ti (that correspond to u_i and t_i) whose sum is less than b.
    for u1 in range(0,b):
        for u2 in range(0,b-u1):
            for u3 in range(0,b-u1-u2):
                for u4 in range(0,b-u1-u2-u3):
                    for u5 in range(0,b-u1-u2-u3-u4):
                        for u6 in range(0,b-u1-u2-u3-u4-u5):
                            for t1 in range(0,b-u1-u2-u3-u4-u5-u6):
                                for t2 in range(0,b-u1-u2-u3-u4-u5-u6-t1):
                                    for t3 in range(0,b-u1-u2-u3-u4-u5-u6-t1-t2):
                                        for t4 in range(0,b-u1-u2-u3-u4-u5-u6-t1-t2-t3):
                                            for t5 in range(0,b-u1-u2-u3-u4-u5-u6-t1-t2-t3-t4):
                                                for t6 in range(0,b-u1-u2-u3-u4-u5-u6-t1-t2-t3-t4-t5):
                                                    # Checks parameters form a 12-gon.
                                                    if u1-u4+t1-t4-t2+t5-u3+u6-2*t3+2*t6==0 and t1-t4+u2-u5+2*t2-2*t5+u3-u6+t3-t6==0:
                                                        # Computes number of vertices this 12-gon has.
                                                        verts=expand(expr.subs([(u_1,u1),(u_2,u2),(u_3,u3),(u_4,u4),(u_5,u5),(u_6,u6),
                                                                               (t_1,t1),(t_2,t2),(t_3,t3),(t_4,t4),(t_5,t5),(t_6,t6)]))
                                                        # Checks that the 12-gon has n vertices.
                                                        if verts==n:
                                                            # Reorders parameters to check interior angle condition.
                                                            lis=[u1,t1,u2,t2,u3,t3,u4,t4,u5,t5,u6,t6]
                                                            val=True
                                                            # Checks all boundary vertices have an interior angle of at least 90 degrees.
                                                            for i in range(0,12):
                                                                if lis[i]==0 and lis[(i+1)%12]==0 and lis[(i+2)%12]==0:
                                                                    val=False
                                                            if val==True:
                                                                cases.append((u1,u2,u3,u4,u5,u6,t1,t2,t3,t4,t5,t6))
    return(cases)
 
# List of which number of vertices we need to check.
vertex_cases=[8,9,11,13,15,20]
# Initalising a list for any case that has an edge boundary less than EB_bound.
counter_cases=[]
for n in vertex_cases:
    # Need to show in every case the edge boundary is at least this big.
    EB_bound=2*math.ceil((96*n-63)**(0.5))
    # If b is large we are done.
    b_bound=math.ceil((EB_bound-12)/6)
    # Generates list of all all n-vertex 12 gons that need to be checked.
    side_length_cases=case_compute(n,b_bound)
    # For each case we compute the edge boundary and verify it is at least EB_bound.
    for case in side_length_cases:
        EB=12
        for i in range(6):
            EB+=6*case[i]+10*case[i+6]
        # We append the case to counter_cases if the edge boundary is less than EB_bound.
        if EB<EB_bound:
            counter_cases.append(case)
if len(counter_cases)==0:
    print('All n-vertex 12-gons, for n= 8, 9, 11, 13, 15, 20, have an edge boundary greater than EB_bound.')
else:
    print(cases)