proposition: Lemma exclude10 : excluded_arity 10.
proof: Proof. Presentation red. Pcase L0_1: s[10] > 5. Pcase L1_1: s[9] > 5. Pcase L2_1: s[8] > 5. Pcase L3_1: s[7] > 5. Pcase L4_1: s[6] > 5. Pcase L5_1: s[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Pcase: s[1] > 5. Similar to L5_1[1]. Pcase L5_2: s[4] > 5. Pcase: s[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: s[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Pcase: s[2] > 5. Similar to *L5_2[5]. Pcase: s[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7,8]<=6 $[9,10]<=7 $. Pcase: s[1] > 5. Similar to L4_1[1]. Pcase L4_2: s[5] > 5. Pcase L5_1: s[4] > 5. Pcase: s[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Pcase: s[3] > 5. Pcase: s[2] > 5. Similar to *L5_1[4]. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=5 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Pcase: s[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=5 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[5]<=5 $[6]<=3 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Pcase: s[2] > 5. Similar to *L4_2[4]. Pcase L4_3: s[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[10]<=4 $[3,4]<=9 $[8,9]<=6 $. Pcase: s[3] > 5. Similar to *L4_3[4]. Pcase: s[7] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7,8]<=5 $[9,10]<=7 $. Pcase: s[8] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=3 $[8]<=4 $[9,10]<=5 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[8]<=2 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7,8]<=7 $[9,10]<=5 $. Pcase: h[7] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7,8]<=5 $[9,10]<=7 $. Pcase: f1[7] <= 5. Reducible. Pcase: h[8] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=3 $[8]<=2 $[9,10]<=7 $. Pcase: h[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[8]<=2 $[9]<=2 $[10]<=4 $. Pcase: h[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[10]<=3 $[8,9]<=5 $. Pcase: h[1] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7,8]<=7 $[9,10]<=5 $. Pcase: f1[10] <= 5. Reducible. Pcase: h[9] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[10]<=4 $[8,9]<=4 $. Pcase L4_4: h[2] > 5. Pcase: h[2] <= 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: h[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7,8]<=7 $[9,10]<=6 $. Pcase: h[4] <= 6. Reducible. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[5]<=5 $[6]<=4 $[7,8]<=7 $[9,10]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7,8]<=6 $[9,10]<=6 $. Pcase: h[6] > 5. Similar to *L4_4[4]. Pcase: h[3] <= 6. Reducible. Pcase: h[5] <= 6. Reducible. Pcase: h[7] <= 5. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: f1[8] <= 5. Reducible. Pcase: f1[9] <= 5. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[8]<=2 $[9]<=2 $[10]<=4 $. Pcase: s[1] > 5. Similar to L3_1[1]. Pcase L3_2: s[6] > 5. Pcase L4_1: s[5] > 5. Pcase: s[4] > 5. Pcase: s[3] > 5. Similar to L3_1[6]. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: s[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: s[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[7]<=4 $[8]<=4 $[5,6]<=8 $[9,10]<=7 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $[5,6]<=6 $. Pcase: s[4] > 5. Pcase: s[3] > 5. Pcase: s[2] > 5. Similar to L4_1[4]. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[6]<=5 $[8]<=4 $[5,7]<=7 $[9,10]<=7 $. Pcase: s[2] > 5. Hubcap $[2]<=5 $[4]<=5 $[6]<=5 $[8]<=4 $[1,3]<=7 $[5,7]<=7 $[9,10]<=7 $. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: s[6] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[6]<=4 $[7]<=3 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[8] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=3 $[8]<=4 $[9]<=2 $[10]<=4 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=3 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=5 $. Pcase: h[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[6]<=5 $[8]<=4 $[5,7]<=7 $[9,10]<=6 $. Pcase: h[3] <= 6. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: h[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5,7]<=7 $[6,8]<=8 $[9,10]<=7 $. Pcase: s[3] > 5. Pcase: s[2] > 5. Similar to *L4_1[3]. Hubcap $[1]<=4 $[2]<=4 $[4]<=4 $[5]<=4 $[7]<=4 $[8]<=4 $[3,6]<=9 $[9,10]<=7 $. Pcase: s[2] > 5. Hubcap $[3]<=4 $[4]<=5 $[5]<=4 $[8]<=4 $[1,6]<=8 $[2,7]<=8 $[9,10]<=7 $. Pcase: s[6] <= 6. Reducible. Pcase: s[6] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[6]<=2 $[7]<=3 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[8] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=2 $[8]<=4 $[9]<=2 $[10]<=4 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=3 $[8]<=3 $[9]<=4 $[10]<=3 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=3 $[8]<=4 $[9]<=2 $[10]<=4 $. Pcase: h[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=3 $[8]<=4 $[9,10]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[4]<=5 $[6]<=4 $[7]<=3 $[8]<=4 $[3,5]<=8 $[9,10]<=7 $. Pcase: s[2] > 5. Similar to *L3_2[3]. Pcase L3_3: s[5] > 5. Pcase: s[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[4,5]<=8 $[9,10]<=7 $. Pcase: s[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=3 $[5]<=5 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: s[5] <= 6. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[3] > 5. Similar to *L3_3[3]. Pcase: s[4] <= 5. Reducible. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=1 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[8] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=5 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=3 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=5 $. Pcase: h[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=3 $[9]<=2 $[10]<=4 $. Pcase: h[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=2 $[10]<=3 $. Pcase: f1[8] <= 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=2 $[9,10]<=7 $. Pcase: h[8] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=3 $[9,10]<=6 $. Pcase L3_4: h[7] > 5. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[10]<=4 $[8,9]<=6 $. Pcase: h[3] <= 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[5]<=4 $[7]<=4 $[8]<=4 $[4,6]<=9 $[9,10]<=6 $. Pcase: h[2] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: h[3] <= 6. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: h[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[5] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: h[5] <= 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: f1[4] <= 6. Reducible. Pcase: h[6] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: h[7] <= 6. Reducible. Pcase: h[8] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=3 $[8]<=3 $[9]<=3 $[10]<=4 $. Pcase: h[9] <= 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8,9]<=6 $[8,10]<=7 $[9,10]<=6 $. Pcase: h[10] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=3 $[9]<=3 $[10]<=3 $. Pcase: h[1] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[10]<=3 $[8,9]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[10]<=4 $[8,9]<=5 $. Pcase: h[2] > 5. Similar to *L3_4[3]. Pcase: h[3] <= 6. Reducible. Pcase: h[6] <= 6. Reducible. Pcase: h[8] <= 5. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: f1[9] <= 5. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: s[1] > 5. Similar to L2_1[1]. Pcase L2_2: s[6] > 5. Pcase L3_1: s[5] > 5. Pcase: s[4] > 5. Similar to L2_1[6]. Pcase: s[7] > 5. Similar to L2_1[7]. Pcase L4_1: s[3] > 5. Pcase: s[2] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=4 $[4]<=4 $[7]<=4 $[8]<=4 $[5,6]<=8 $[9,10]<=8 $. Hubcap $[1]<=4 $[2]<=4 $[7]<=4 $[8]<=4 $[3,6]<=9 $[4,5]<=7 $[9,10]<=8 $. Pcase: s[2] > 5. Similar to *L4_1[6]. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: s[3] > 5. Pcase: s[4] > 5. Similar to L3_1[4]. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=4 $. Pcase: s[3] > 7. Hubcap $[1]<=4 $[2]<=4 $[3]<=1 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=5 $. Pcase: s[6] > 7. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=1 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=5 $. Pcase: s[7] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=3 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=5 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: h[9] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: f1[9] <= 5. Reducible. Pcase: h[10] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=3 $[10]<=3 $. Pcase: h[1] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: f1[10] <= 5. Reducible. Pcase L4_1: h[4] <= 5. Pcase: h[5] <= 6. Reducible. Pcase: s[2] > 5. Hubcap $[1]<=4 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[2,3]<=7 $[9,10]<=8 $. Pcase: s[3] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=4 $[4]<=3 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: f1[3] <= 5. Reducible. Pcase: s[6] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[8]<=4 $[6,7]<=7 $[9,10]<=8 $. Pcase: h[6] <= 5. Similar to *L4_1[2]. Pcase: s[3] > 6. Hubcap $[1]<=4 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[2,3]<=7 $[9,10]<=8 $. Pcase: s[6] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=5 $[4]<=4 $[5]<=4 $[8]<=4 $[6,7]<=7 $[9,10]<=8 $. Pcase L4_2: s[2] > 5. Pcase: s[7] > 5. Similar to L3_1[7]. Pcase: h[7] <= 5. Similar to L4_1[3]. Pcase: h[9] <= 5. Similar to *L4_1[9]. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=3 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=3 $. Pcase: f1[2] <= 5. Reducible. Pcase: h[3] > 6. Hubcap $[1]<=4 $[2]<=3 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=4 $. Pcase: h[4] > 6. Hubcap $[1]<=4 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: f1[3] <= 5. Reducible. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=4 $[4]<=3 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=4 $. Hubcap $[1]<=4 $[4]<=4 $[5]<=4 $[8]<=4 $[2,3]<=8 $[6,7]<=8 $[9,10]<=8 $. Pcase: s[7] > 5. Similar to L4_2[7]. Reducible. Pcase L3_2: s[2] > 5. Pcase: s[2] > 7. Hubcap $[1]<=3 $[2]<=2 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=4 $. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: s[6] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=2 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: s[7] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=3 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=4 $. Pcase: s[9] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=0 $[10]<=3 $. Pcase: s[10] > 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: s[9] > 6. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=3 $. Pcase: s[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[4]<=5 $[6]<=5 $[7]<=4 $[8]<=4 $[3,5]<=7 $[9,10]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[8]<=4 $[6,7]<=8 $[9,10]<=6 $. Pcase: s[6] > 6. Hubcap $[4]<=5 $[6]<=4 $[7]<=4 $[8]<=4 $[1,3]<=7 $[2,5]<=8 $[9,10]<=8 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=7 $. Pcase: h[6] > 6. Hubcap $[4]<=5 $[6]<=4 $[7]<=4 $[8]<=4 $[1,3]<=7 $[2,5]<=8 $[9,10]<=8 $. Pcase: f1[6] <= 5. Reducible. Pcase: h[9] > 6. Hubcap $[2]<=5 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[1,3]<=7 $[9,10]<=6 $. Pcase: f1[9] <= 5. Reducible. Pcase: h[10] > 6. Hubcap $[2]<=5 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=3 $[10]<=3 $[1,3]<=7 $. Pcase: h[1] > 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: f1[10] <= 5. Reducible. Pcase: h[1] > 5. Pcase: s[2] > 6. Hubcap $[1]<=2 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: f1[2] <= 5. Reducible. Pcase: s[4] > 5. Hubcap $[1]<=3 $[2]<=5 $[4]<=5 $[6]<=5 $[7]<=4 $[8]<=4 $[3,5]<=7 $[9,10]<=7 $. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[8]<=4 $[6,7]<=8 $[9,10]<=7 $. Pcase: s[2] > 6. Hubcap $[1]<=3 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[2,3]<=7 $[9,10]<=8 $. Pcase: s[4] <= 5. Reducible. Pcase: f1[2] <= 5. Reducible. Pcase: s[7] > 5. Hubcap $[1]<=4 $[3]<=3 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $[2,4]<=9 $. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[6] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=5 $[10]<=4 $. Pcase: h[7] > 5. Hubcap $[1]<=4 $[3]<=3 $[5]<=4 $[8]<=4 $[2,4]<=9 $[6,7]<=8 $[9,10]<=8 $. Hubcap $[1]<=4 $[3]<=3 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[2,4]<=9 $[9,10]<=7 $. Pcase: s[4] > 5. Pcase: s[7] > 5. Similar to *L3_2[5]. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=2 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: s[6] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[6]<=2 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=6 $. Pcase: h[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[5]<=3 $[7]<=4 $[8]<=4 $[4,6]<=9 $[9,10]<=7 $. Pcase: h[3] <= 6. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=4 $[9,10]<=8 $. Pcase: s[6] <= 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: h[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=5 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[8]<=4 $[6,7]<=7 $[9,10]<=8 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=4 $[8]<=4 $[6,7]<=6 $[9,10]<=6 $. Pcase: s[3] > 5. Similar to *L2_2[2]. Pcase L2_3: s[4] > 5. Pcase: s[5] > 5. Pcase L4_1: s[2] > 5. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=8 $. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=8 $. Pcase: s[5] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[7]<=5 $[8]<=4 $[5,6]<=7 $[9,10]<=8 $. Pcase: s[7] > 5. Hubcap $[2]<=5 $[4]<=4 $[5]<=4 $[7]<=5 $[9]<=4 $[10]<=4 $[1,3]<=7 $[6,8]<=7 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[6]<=4 $[7]<=5 $[5,8]<=8 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=6 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=4 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=7 $. Pcase: f1[2] <= 5. Reducible. Pcase: h[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=3 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=5 $[10]<=4 $[4,5]<=7 $. Pcase: f1[2] <= 6. Reducible. Pcase: h[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=7 $[9,10]<=8 $. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=8 $[9,10]<=7 $. Pcase: s[7] > 5. Similar to L4_1[5]. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=6 $[9,10]<=8 $. Pcase: s[5] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[7]<=5 $[8]<=4 $[5,6]<=7 $[9,10]<=8 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=8 $[9,10]<=6 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=8 $[9,10]<=6 $. Pcase: h[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=6 $[9,10]<=8 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[5] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[5]<=3 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=8 $. Pcase: h[6] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=6 $[9,10]<=8 $. Pcase: f1[5] <= 5. Reducible. Pcase: h[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=8 $[9,10]<=6 $. Pcase: f1[9] <= 5. Reducible. Pcase: h[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=3 $[10]<=3 $[4,5]<=8 $. Pcase: h[1] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=8 $[9,10]<=6 $. Pcase: f1[10] <= 5. Reducible. Pcase L4_2: h[2] > 5. Pcase: h[2] <= 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=4 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=7 $. Pcase: h[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=7 $[9,10]<=7 $. Pcase: h[4] <= 5. Reducible. Pcase: h[6] <= 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[4,5]<=7 $[9,10]<=7 $. Pcase: h[7] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=3 $[6]<=3 $[7]<=5 $[8]<=4 $[9,10]<=7 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=6 $. Pcase: h[3] > 5. Similar to *L4_2[7]. Pcase: h[7] > 5. Similar to L4_2[5]. Pcase: h[8] > 5. Similar to *L4_2[2]. Reducible. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=5 $[10]<=4 $[8,9]<=7 $. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=2 $[5]<=4 $[6]<=5 $[7,10]<=9 $[8,9]<=7 $. Pcase: s[7] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=2 $[8]<=3 $[9]<=4 $[10]<=5 $. Pcase: s[9] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=5 $[8]<=4 $[9]<=0 $[10]<=3 $. Pcase: s[10] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[7]<=5 $[8]<=4 $[9]<=3 $[10]<=0 $. Pcase: s[7] <= 5. Pcase: s[2] > 5. Hubcap $[1]<=4 $[3]<=3 $[5]<=4 $[6]<=5 $[7]<=5 $[8]<=4 $[2,4]<=9 $[9,10]<=6 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=2 $[5]<=4 $[6]<=5 $[7]<=5 $[8]<=4 $[9,10]<=6 $. Pcase: s[9] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=3 $[9,10]<=6 $. Pcase: s[2] > 5. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=5 $[10]<=4 $[8,9]<=7 $. Pcase: s[7] > 6. Hubcap $[2]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=4 $[1,3]<=7 $. Hubcap $[2]<=5 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=5 $[1,3]<=7 $[8,9]<=7 $[8,10]<=7 $[9,10]<=7 $. Pcase: s[10] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[5]<=4 $[6]<=4 $[8]<=4 $[4,7]<=9 $[9,10]<=6 $. Pcase: s[7] <= 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=3 $[9,10]<=7 $. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=3 $[9,10]<=8 $. Pcase: h[2] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=3 $[9,10]<=7 $. Pcase: h[3] <= 6. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: h[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=5 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[5] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=5 $. Pcase: h[5] <= 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=3 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=5 $. Pcase: f1[4] <= 6. Reducible. Pcase: h[6] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=3 $[6]<=3 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=5 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7,8]<=6 $[9,10]<=8 $. Pcase: s[5] > 5. Similar to *L2_3[2]. Pcase L2_4: s[2] > 5. Pcase: s[2] > 7. Hubcap $[1]<=3 $[2]<=2 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=5 $[7]<=5 $[10]<=4 $[8,9]<=7 $. Pcase: s[7] > 7. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=2 $[8]<=3 $[9]<=4 $[10]<=4 $. Pcase: s[9] > 7. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=5 $[7]<=5 $[8]<=4 $[9]<=0 $[10]<=3 $. Pcase: s[10] > 6. Hubcap $[3]<=4 $[4]<=5 $[5]<=5 $[7]<=5 $[1,6]<=7 $[2,8]<=8 $[9,10]<=6 $. Pcase L3_1: s[2] > 6. Pcase: s[7] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=4 $[8]<=3 $[9]<=4 $[10]<=4 $. Pcase: s[9] <= 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=3 $[9,10]<=7 $. Pcase: s[7] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=3 $[9]<=4 $[10]<=3 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=3 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=5 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=2 $. Pcase: h[3] > 5. Hubcap $[1]<=3 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=5 $[7]<=5 $[2,10]<=6 $[8,9]<=7 $. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=5 $[5]<=5 $[6]<=5 $[7]<=5 $[8]<=4 $[9,10]<=6 $. Pcase: s[7] > 6. Similar to *L3_1[2]. Pcase: s[7] <= 5. Reducible. Pcase: h[1] <= 5. Reducible. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=5 $[8]<=3 $[9,10]<=6 $. Pcase: s[7] > 5. Similar to *L2_4[2]. Reducible. Pcase: s[1] > 5. Similar to L1_1[1]. Pcase L1_2: s[7] > 5. Pcase: s[6] > 5. Similar to L1_1[7]. Pcase: s[8] > 5. Similar to L1_1[8]. Pcase L2_1: s[4] > 5. Pcase: s[3] > 5. Similar to L1_1[4]. Pcase: s[5] > 5. Similar to L1_1[5]. Pcase: s[2] > 5. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=5 $[5]<=4 $[6]<=4 $[8]<=4 $[9]<=4 $[7,10]<=9 $. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=2 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: s[7] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=1 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: s[7] <= 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[10] > 7. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=2 $. Pcase: h[6] <= 5. Hubcap $[5]<=4 $[6]<=4 $[9]<=4 $[10]<=5 $[1,3]<=7 $[2,4]<=9 $[7,8]<=7 $. Pcase: s[10] > 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=3 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=4 $. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=3 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=3 $[7]<=4 $[8]<=4 $[9]<=4 $[10]<=5 $. Hubcap $[2]<=5 $[4]<=5 $[5]<=4 $[6]<=3 $[7]<=4 $[9]<=4 $[1,3]<=7 $[8,10]<=8 $. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=1 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: s[7] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=1 $[8]<=4 $[9]<=4 $[10]<=5 $. Pcase: s[10] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=1 $. Pcase: s[7] <= 6. Pcase: s[4] <= 6. Reducible. Pcase: s[10] <= 6. Reducible. Pcase: h[2] <= 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9,10]<=7 $. Pcase: h[3] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=4 $. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[6]<=4 $[7]<=5 $[8]<=4 $[9]<=4 $[10]<=4 $[4,5]<=7 $. Pcase: h[5] <= 5. Hubcap $[2]<=5 $[3]<=4 $[6]<=3 $[7]<=4 $[8]<=4 $[9]<=4 $[1,4]<=8 $[5,10]<=8 $. Pcase: h[6] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[5]<=3 $[6]<=3 $[8]<=4 $[9]<=4 $[10]<=5 $[4,7]<=8 $. Pcase: h[7] <= 5. Reducible. Pcase: s[10] <= 6. Hubcap $[1]<=4 $[2]<=5 $[5]<=4 $[6]<=4 $[9]<=4 $[10]<=5 $[3,4]<=7 $[7,8]<=7 $. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=4 $[6]<=4 $[9]<=4 $[10]<=4 $[7,8]<=7 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[9]<=4 $[10]<=4 $[7,8]<=7 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=4 $[7,8]<=7 $[9,10]<=7 $. Pcase: s[3] > 5. Similar to L2_1[3]. Pcase L2_2: s[2] > 5. Pcase: s[2] > 7. Hubcap $[1]<=3 $[2]<=2 $[3]<=4 $[4]<=5 $[5]<=5 $[8]<=4 $[9]<=4 $[10]<=5 $[6,7]<=8 $. Pcase: s[5] > 5. Hubcap $[1]<=3 $[3]<=4 $[4]<=4 $[6]<=3 $[8]<=4 $[9]<=4 $[2,10]<=9 $[5,7]<=9 $. Hubcap $[1]<=3 $[3]<=4 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=2 $[8]<=4 $[9]<=4 $[2,10]<=9 $. Pcase: s[5] > 5. Similar to *L2_2[4]. Pcase: s[7] <= 6. Reducible. Pcase: s[10] <= 6. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=5 $[5]<=5 $[6]<=4 $[7]<=2 $[8]<=4 $[9]<=4 $[10]<=2 $. Pcase: s[3] > 5. Similar to L1_2[3]. Pcase: s[5] > 5. Pcase: s[2] > 5. Similar to L1_2[5]. Pcase: s[4] > 5. Similar to L1_1[5]. Pcase: s[6] > 5. Similar to L1_1[6]. Pcase: s[8] > 5. Similar to L1_2[8]. Pcase: s[5] <= 6. Reducible. Pcase: s[10] <= 6. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=5 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=5 $[8]<=5 $[9]<=4 $[10]<=2 $. Pcase L1_3: s[4] > 5. Pcase L2_1: s[2] > 5. Pcase: s[2] > 7. Hubcap $[1]<=3 $[2]<=2 $[3]<=3 $[4]<=5 $[5]<=4 $[6]<=5 $[8]<=5 $[9]<=4 $[7,10]<=9 $. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[6]<=5 $[8]<=5 $[9]<=4 $[4,5]<=5 $[7,10]<=9 $. Pcase: s[6] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[8]<=5 $[9]<=4 $[10]<=5 $[6,7]<=5 $. Pcase: s[8] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=4 $[6]<=5 $[9]<=3 $[10]<=5 $[7,8]<=5 $. Pcase: s[10] > 7. Hubcap $[1]<=3 $[2]<=5 $[3]<=4 $[5]<=4 $[6]<=5 $[8]<=5 $[4,7]<=9 $[9,10]<=5 $. Pcase L3_1: h[4] > 5. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[3]<=2 $[4]<=4 $[5]<=4 $[6]<=5 $[8]<=5 $[9]<=4 $[7,10]<=9 $. Pcase L4_1: s[6] > 6. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=3 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $. Pcase: s[8] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=3 $[8]<=5 $[9]<=4 $[10]<=5 $. Pcase: s[10] > 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $. Pcase: f1[2] <= 5. Reducible. Pcase: h[3] > 5. Hubcap $[1]<=4 $[2]<=4 $[3]<=2 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $. Pcase: f1[2] <= 6. Reducible. Pcase: h[4] <= 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $[5,6]<=6 $. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=3 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[8]<=5 $[9]<=4 $[10]<=5 $[6,7]<=7 $. Pcase: s[4] > 6. Hubcap $[2]<=5 $[3]<=3 $[6]<=5 $[8]<=5 $[1,9]<=7 $[4,5]<=6 $[7,10]<=9 $. Pcase: h[2] > 6. Hubcap $[1]<=3 $[2]<=3 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $. Pcase: f1[2] <= 5. Reducible. Pcase: h[3] > 5. Hubcap $[2]<=4 $[3]<=2 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=5 $[10]<=5 $[1,9]<=7 $. Pcase: f1[2] <= 6. Reducible. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[10]<=5 $[4,7]<=7 $[5,8]<=8 $[6,9]<=8 $. Pcase: f1[4] <= 5. Reducible. Pcase L4_2: s[8] > 5. Pcase: s[6] > 5. Hubcap $[1]<=4 $[3]<=3 $[4]<=4 $[10]<=5 $[2,9]<=8 $[5,7]<=7 $[6,8]<=9 $. Pcase: s[8] <= 6. Reducible. Pcase: h[6] <= 6. Reducible. Pcase: h[1] > 5. Similar to *L4_1[7]. Pcase: s[10] > 6. Hubcap $[1]<=3 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=2 $[10]<=4 $. Pcase: f1[10] <= 5. Reducible. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=4 $[9]<=3 $[10]<=5 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[10]<=5 $[8,9]<=6 $. Pcase: s[6] <= 5. Reducible. Pcase: s[10] <= 6. Reducible. Pcase: h[6] > 5. Similar to L4_2[2]. Pcase: h[1] > 5. Similar to *L4_2[7]. Pcase: h[4] <= 6. Reducible. Pcase: f1[6] <= 5. Reducible. Pcase: h[2] > 5. Hubcap $[1]<=2 $[2]<=4 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Hubcap $[1]<=3 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=4 $[8]<=5 $[9,10]<=7 $. Pcase: h[1] > 5. Similar to *L3_1[7]. Pcase L3_2: s[6] <= 5. Pcase: s[2] > 6. Hubcap $[1]<=3 $[2]<=4 $[5]<=4 $[6]<=5 $[3,8]<=7 $[4,9]<=8 $[7,10]<=9 $. Pcase: s[8] <= 5. Hubcap $[2]<=4 $[4]<=4 $[5]<=4 $[6]<=5 $[7]<=5 $[8]<=5 $[9]<=4 $[10]<=4 $[1,3]<=5 $. Pcase: h[2] > 5. Similar to L3_1[8]. Pcase: h[9] > 5. Similar to *L3_1[9]. Pcase: h[3] <= 6. Reducible. Pcase: f1[2] <= 5. Reducible. Hubcap $[1]<=4 $[2]<=4 $[3]<=3 $[5]<=4 $[6]<=5 $[8]<=5 $[9]<=3 $[10]<=4 $[4,7]<=8 $. Pcase: s[8] <= 5. Similar to L3_2[2]. Pcase: h[2] > 5. Similar to L3_1[8]. Pcase: h[3] > 5. Similar to *L3_1[5]. Pcase: h[5] > 5. Similar to *L3_1[3]. Pcase: h[6] > 5. Similar to L3_1[2]. Pcase: h[7] > 5. Similar to *L3_1[1]. Pcase: h[8] > 5. Similar to L3_1[4]. Pcase: h[9] > 5. Similar to *L3_1[9]. Pcase: h[10] > 5. Similar to L3_1[6]. Pcase: s[2] <= 6. Reducible. Pcase: s[4] <= 6. Reducible. Pcase: s[6] <= 6. Reducible. Pcase: s[8] <= 6. Reducible. Pcase: s[10] <= 6. Reducible. Pcase: f1[2] <= 5. Reducible. Pcase: f1[4] <= 5. Reducible. Pcase: f1[6] <= 5. Reducible. Pcase: f1[8] <= 5. Reducible. Pcase: f1[10] <= 5. Reducible. Pcase: f2[2] <= 5. Reducible. Pcase: f2[4] <= 5. Reducible. Pcase: f2[6] <= 5. Reducible. Pcase: f2[8] <= 5. Reducible. Pcase: f2[10] <= 5. Reducible. Hubcap $[1]<=2 $[2]<=4 $[3]<=2 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=2 $[8]<=4 $[9]<=2 $[10]<=4 $. Pcase L2_2: s[6] > 5. Pcase: s[8] > 5. Similar to L2_1[6]. Pcase: s[4] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=2 $[5]<=3 $[7]<=4 $[8]<=5 $[9]<=4 $[6,10]<=9 $. Pcase: s[6] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[8]<=5 $[9]<=4 $[10]<=5 $[6,7]<=5 $. Pcase: s[10] > 7. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[6]<=5 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=1 $. Pcase: h[3] <= 5. Hubcap $[2]<=5 $[3]<=4 $[8]<=5 $[9]<=4 $[1,5]<=6 $[4,6]<=8 $[7,10]<=8 $. Pcase: s[10] <= 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=5 $. Pcase L3_1: s[6] > 6. Pcase: s[4] > 6. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Pcase: h[2] > 5. Hubcap $[1]<=3 $[2]<=4 $[3]<=4 $[4]<=5 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Pcase: h[3] <= 6. Reducible. Pcase: h[1] <= 5. Reducible. Pcase: h[4] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=3 $[4]<=4 $[5]<=3 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Pcase: f1[4] <= 5. Reducible. Pcase: h[5] > 5. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=4 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=5 $[5]<=3 $[8]<=5 $[6,7]<=7 $[9,10]<=7 $. Pcase: s[4] > 6. Similar to *L3_1[1]. Pcase: h[5] <= 5. Reducible. Pcase: h[6] <= 5. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=3 $[5]<=2 $[6]<=4 $[7]<=4 $[8]<=5 $[9]<=4 $[10]<=4 $. Pcase: s[8] > 5. Similar to L2_2[4]. Pcase: s[4] <= 6. Reducible. Pcase: s[10] <= 6. Reducible. Hubcap $[1]<=4 $[2]<=5 $[3]<=4 $[4]<=2 $[5]<=4 $[6]<=5 $[7]<=5 $[8]<=5 $[9]<=4 $[10]<=2 $. Pcase: s[6] > 5. Similar to L1_3[6]. Pcase: s[2] <= 6. Reducible. Pcase: s[8] <= 6. Reducible. Similar to L1_3[8]. Pcase: s[1] > 5. Similar to L0_1[1]. Pcase: s[2] > 5. Similar to L0_1[2]. Pcase: s[3] > 5. Similar to L0_1[3]. Pcase: s[4] > 5. Similar to L0_1[4]. Pcase: s[5] > 5. Similar to L0_1[5]. Pcase: s[6] > 5. Similar to L0_1[6]. Pcase: s[7] > 5. Similar to L0_1[7]. Pcase: s[8] > 5. Similar to L0_1[8]. Pcase: s[9] > 5. Similar to L0_1[9]. Reducible. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat ssrint) fourcolor(part hubcap present)