proof (prove)
goal (1 subgoal):
 1. ⋀(x::real) xa xb xc xd xe xf xg xh xi xj xk xl
       xm xn xo xp xq xr xs xt xu xv xw xx xy
       xz ya yb yc yd ye yf yg yh yi yj yk yl
       ym yn yo yp yq yr ys yt yu yv yw yx yy
       yz za zb zc zd ze zf zg zh zi zj zk zl
       zm zn zo zp zq zr zs zt zu zv zw zx zy
       zz aaa aab aac aad aae aaf aag aah aai
       aaj aak aal aam aan aao aap aaq aar
       aas aat aau aav aaw aax aay aaz aba
       abb abc abd abe abf abg abh abi abj
       abk abl abm abn abo abp abq abr abs
       abt abu abv abw abx aby abz aca acb
       acc acd ace acf acg ach aci acj ack
       acl acm acn aco acp acq acr acs act
       acu acv acw acx acy acz ada adb adc
       add ade adf adg adh adi adj adk adl
       adm adn ado adp adq adr ads adt adu
       adv adw adx ady adz aea aeb aec aed
       aee.
       0 ≤ x ⟹
       0 ≤ xa ⟹
       0 ≤ xb ⟹
       0 ≤ xc ⟹
       0 ≤ xd ⟹
       0 ≤ xe ⟹
       0 ≤ xf ⟹
       0 ≤ xg ⟹
       0 ≤ xh ⟹
       0 ≤ xi ⟹
       0 ≤ xj ⟹
       0 ≤ xk ⟹
       0 ≤ xl ⟹
       0 ≤ xm ⟹
       0 ≤ xn ⟹
       0 ≤ xo ⟹
       0 ≤ xp ⟹
       0 ≤ xq ⟹
       0 ≤ xr ⟹
       0 ≤ xs ⟹
       0 ≤ xt ⟹
       0 ≤ xu ⟹
       0 ≤ xv ⟹
       0 ≤ xw ⟹
       0 ≤ xx ⟹
       0 ≤ xy ⟹
       0 ≤ xz ⟹
       0 ≤ ya ⟹
       0 ≤ yb ⟹
       0 ≤ yc ⟹
       0 ≤ yd ⟹
       0 ≤ ye ⟹
       0 ≤ yf ⟹
       0 ≤ yg ⟹
       0 ≤ yh ⟹
       0 ≤ yi ⟹
       0 ≤ yj ⟹
       0 ≤ yk ⟹
       0 ≤ yl ⟹
       0 ≤ ym ⟹
       0 ≤ yn ⟹
       0 ≤ yo ⟹
       0 ≤ yp ⟹
       0 ≤ yq ⟹
       0 ≤ yr ⟹
       0 ≤ ys ⟹
       0 ≤ yt ⟹
       0 ≤ yu ⟹
       0 ≤ yv ⟹
       0 ≤ yw ⟹
       0 ≤ yx ⟹
       0 ≤ yy ⟹
       0 ≤ yz ⟹
       0 ≤ za ⟹
       0 ≤ zb ⟹
       0 ≤ zc ⟹
       0 ≤ zd ⟹
       0 ≤ ze ⟹
       0 ≤ zf ⟹
       0 ≤ zg ⟹
       0 ≤ zh ⟹
       0 ≤ zi ⟹
       0 ≤ zj ⟹
       0 ≤ zk ⟹
       0 ≤ zl ⟹
       0 ≤ zm ⟹
       0 ≤ zn ⟹
       0 ≤ zo ⟹
       0 ≤ zp ⟹
       0 ≤ zq ⟹
       0 ≤ zr ⟹
       0 ≤ zs ⟹
       0 ≤ zt ⟹
       0 ≤ zu ⟹
       0 ≤ zv ⟹
       0 ≤ zw ⟹
       0 ≤ zx ⟹
       0 ≤ zy ⟹
       0 ≤ zz ⟹
       0 ≤ aaa ⟹
       0 ≤ aab ⟹
       0 ≤ aac ⟹
       0 ≤ aad ⟹
       0 ≤ aae ⟹
       0 ≤ aaf ⟹
       0 ≤ aag ⟹
       0 ≤ aah ⟹
       0 ≤ aai ⟹
       0 ≤ aaj ⟹
       0 ≤ aak ⟹
       0 ≤ aal ⟹
       0 ≤ aam ⟹
       0 ≤ aan ⟹
       0 ≤ aao ⟹
       0 ≤ aap ⟹
       0 ≤ aaq ⟹
       0 ≤ aar ⟹
       0 ≤ aas ⟹
       0 ≤ aat ⟹
       0 ≤ aau ⟹
       0 ≤ aav ⟹
       0 ≤ aaw ⟹
       0 ≤ aax ⟹
       0 ≤ aay ⟹
       0 ≤ aaz ⟹
       0 ≤ aba ⟹
       0 ≤ abb ⟹
       0 ≤ abc ⟹
       0 ≤ abd ⟹
       0 ≤ abe ⟹
       0 ≤ abf ⟹
       0 ≤ abg ⟹
       0 ≤ abh ⟹
       0 ≤ abi ⟹
       0 ≤ abj ⟹
       0 ≤ abk ⟹
       0 ≤ abl ⟹
       0 ≤ abm ⟹
       0 ≤ abn ⟹
       0 ≤ abo ⟹
       0 ≤ abp ⟹
       0 ≤ abq ⟹
       0 ≤ abr ⟹
       0 ≤ abs ⟹
       0 ≤ abt ⟹
       0 ≤ abu ⟹
       0 ≤ abv ⟹
       0 ≤ abw ⟹
       0 ≤ abx ⟹
       0 ≤ aby ⟹
       0 ≤ abz ⟹
       0 ≤ aca ⟹
       0 ≤ acb ⟹
       0 ≤ acc ⟹
       0 ≤ acd ⟹
       0 ≤ ace ⟹
       0 ≤ acf ⟹
       0 ≤ acg ⟹
       0 ≤ ach ⟹
       0 ≤ aci ⟹
       0 ≤ acj ⟹
       0 ≤ ack ⟹
       0 ≤ acl ⟹
       0 ≤ acm ⟹
       0 ≤ acn ⟹
       0 ≤ aco ⟹
       0 ≤ acp ⟹
       0 ≤ acq ⟹
       0 ≤ acr ⟹
       0 ≤ acs ⟹
       0 ≤ act ⟹
       0 ≤ acu ⟹
       0 ≤ acv ⟹
       0 ≤ acw ⟹
       0 ≤ acx ⟹
       0 ≤ acy ⟹
       0 ≤ acz ⟹
       0 ≤ ada ⟹
       0 ≤ adb ⟹
       0 ≤ adc ⟹
       0 ≤ add ⟹
       0 ≤ ade ⟹
       0 ≤ adf ⟹
       0 ≤ adg ⟹
       0 ≤ adh ⟹
       0 ≤ adi ⟹
       0 ≤ adj ⟹
       0 ≤ adk ⟹
       0 ≤ adl ⟹
       0 ≤ adm ⟹
       0 ≤ adn ⟹
       0 ≤ ado ⟹
       0 ≤ adp ⟹
       0 ≤ adq ⟹
       0 ≤ adr ⟹
       0 ≤ ads ⟹
       0 ≤ adt ⟹
       0 ≤ adu ⟹
       0 ≤ adv ⟹
       0 ≤ adw ⟹
       0 ≤ adx ⟹
       0 ≤ ady ⟹
       0 ≤ adz ⟹
       0 ≤ aea ⟹
       0 ≤ aeb ⟹
       0 ≤ aec ⟹
       0 ≤ aed ⟹
       0 ≤ aee ⟹
       0 ≤ yc ∧
       0 ≤ yd ∧ 0 ≤ yb ∧ 0 ≤ ya ⟹
       0 ≤ yf ∧
       0 ≤ xh ∧ 0 ≤ ye ∧ 0 ≤ yg ⟹
       0 ≤ yw ∧
       0 ≤ yv ∧ 0 ≤ xs ∧ 0 ≤ yu ⟹
       0 ≤ aea ∧
       0 ≤ adz ∧ 0 ≤ aee ∧ 0 ≤ aed ⟹
       0 ≤ zy ∧
       0 ≤ zx ∧ 0 ≤ xz ∧ 0 ≤ zw ⟹
       0 ≤ zb ∧
       0 ≤ za ∧ 0 ≤ yy ∧ 0 ≤ yz ⟹
       0 ≤ zp ∧
       0 ≤ xq ∧ 0 ≤ zo ∧ 0 ≤ yq ⟹
       0 ≤ adp ∧
       0 ≤ ado ∧ 0 ≤ aeb ∧ 0 ≤ aec ⟹
       0 ≤ acm ∧
       0 ≤ aau ∧ 0 ≤ aco ∧ 0 ≤ acn ⟹
       0 ≤ abl ∧
       0 ≤ zv ∧ 0 ≤ abm ∧ 0 ≤ abn ⟹
       0 ≤ zr ∧
       0 ≤ abi ∧ 0 ≤ zq ∧ 0 ≤ abh ⟹
       0 ≤ abq ∧
       0 ≤ abp ∧ 0 ≤ zd ∧ 0 ≤ abo ⟹
       0 ≤ acd ∧
       0 ≤ acc ∧ 0 ≤ xi ∧ 0 ≤ acb ⟹
       0 ≤ acp ∧
       0 ≤ acl ∧ 0 ≤ acr ∧ 0 ≤ acq ⟹
       0 ≤ xw ∧
       0 ≤ xr ∧ 0 ≤ xv ∧ 0 ≤ xu ⟹
       0 ≤ zc ∧
       0 ≤ xj ∧ 0 ≤ acg ∧ 0 ≤ ach ⟹
       0 ≤ zt ∧
       0 ≤ xx ∧ 0 ≤ zs ∧ 0 ≤ xy ⟹
       0 ≤ ady ∧
       0 ≤ adx ∧ 0 ≤ adw ∧ 0 ≤ zg ⟹
       0 ≤ abd ∧
       0 ≤ abc ∧ 0 ≤ yr ∧ 0 ≤ abb ⟹
       0 ≤ adi ∧
       0 ≤ x ∧ 0 ≤ adh ∧ 0 ≤ xa ⟹
       0 ≤ aak ∧
       0 ≤ aaj ∧ 0 ≤ aai ∧ 0 ≤ aad ⟹
       0 ≤ aba ∧
       0 ≤ aaz ∧ 0 ≤ zh ∧ 0 ≤ aay ⟹
       0 ≤ abg ∧
       0 ≤ abf ∧ 0 ≤ ys ∧ 0 ≤ abe ⟹
       0 ≤ abs ∧
       0 ≤ yt ∧ 0 ≤ abr ∧ 0 ≤ zu ⟹
       0 ≤ abv ∧
       0 ≤ zn ∧ 0 ≤ abw ∧ 0 ≤ zm ⟹
       0 ≤ adl ∧
       0 ≤ xk ∧ 0 ≤ adm ∧ 0 ≤ adn ⟹
       0 ≤ acf ∧
       0 ≤ ace ∧ 0 ≤ xp ∧ 0 ≤ aca ⟹
       0 ≤ ads ∧
       0 ≤ adt ∧ 0 ≤ aap ∧ 0 ≤ aaq ⟹
       0 ≤ ada ∧
       0 ≤ aax ∧ 0 ≤ acz ∧ 0 ≤ acy ⟹
       0 ≤ aaf ∧
       0 ≤ aae ∧ 0 ≤ aac ∧ 0 ≤ aag ⟹
       0 ≤ aal ∧
       0 ≤ acu ∧ 0 ≤ acs ∧ 0 ≤ act ⟹
       0 ≤ aas ∧
       0 ≤ aar ∧ 0 ≤ xb ∧ 0 ≤ aat ⟹
       0 ≤ zk ∧
       0 ≤ zl ∧ 0 ≤ zj ∧ 0 ≤ zi ⟹
       0 ≤ ack ∧
       0 ≤ acj ∧ 0 ≤ xc ∧ 0 ≤ aci ⟹
       0 ≤ aav ∧
       0 ≤ aaw ∧ 0 ≤ aah ∧ 0 ≤ xd ⟹
       0 ≤ abt ∧
       0 ≤ xo ∧ 0 ≤ abu ∧ 0 ≤ xn ⟹
       0 ≤ adc ∧
       0 ≤ abz ∧ 0 ≤ add ∧ 0 ≤ ade ⟹
       0 ≤ xt ∧
       0 ≤ zz ∧ 0 ≤ aab ∧ 0 ≤ aaa ⟹
       0 ≤ adq ∧
       0 ≤ xl ∧ 0 ≤ adr ∧ 0 ≤ adb ⟹
       0 ≤ zf ∧
       0 ≤ ze ∧ 0 ≤ yh ∧ 0 ≤ yi ⟹
       0 ≤ aao ∧
       0 ≤ aan ∧ 0 ≤ aam ∧ 0 ≤ xe ⟹
       0 ≤ abk ∧
       0 ≤ aby ∧ 0 ≤ abj ∧ 0 ≤ abx ⟹
       0 ≤ yp ∧
       0 ≤ yo ∧ 0 ≤ xm ∧ 0 ≤ yn ⟹
       0 ≤ yl ∧
       0 ≤ yk ∧ 0 ≤ yj ∧ 0 ≤ ym ⟹
       0 ≤ acw ∧
       0 ≤ acv ∧ 0 ≤ acx ∧ 0 ≤ xg ⟹
       0 ≤ adk ∧
       0 ≤ adg ∧ 0 ≤ adj ∧ 0 ≤ adf ⟹
       0 ≤ adv ∧
       0 ≤ yx ∧ 0 ≤ xf ∧ 0 ≤ adu ⟹
       yc + yd + yb + ya = 1 ⟹
       yf + xh + ye + yg = 1 ⟹
       yw + yv + xs + yu = 1 ⟹
       aea + adz + aee + aed = 1 ⟹
       zy + zx + xz + zw = 1 ⟹
       zb + za + yy + yz = 1 ⟹
       zp + xq + zo + yq = 1 ⟹
       adp + ado + aeb + aec = 1 ⟹
       acm + aau + aco + acn = 1 ⟹
       abl + zv + abm + abn = 1 ⟹
       zr + abi + zq + abh = 1 ⟹
       abq + abp + zd + abo = 1 ⟹
       acd + acc + xi + acb = 1 ⟹
       acp + acl + acr + acq = 1 ⟹
       xw + xr + xv + xu = 1 ⟹
       zc + xj + acg + ach = 1 ⟹
       zt + xx + zs + xy = 1 ⟹
       ady + adx + adw + zg = 1 ⟹
       abd + abc + yr + abb = 1 ⟹
       adi + x + adh + xa = 1 ⟹
       aak + aaj + aai + aad = 1 ⟹
       aba + aaz + zh + aay = 1 ⟹
       abg + abf + ys + abe = 1 ⟹
       abs + yt + abr + zu = 1 ⟹
       abv + zn + abw + zm = 1 ⟹
       adl + xk + adm + adn = 1 ⟹
       acf + ace + xp + aca = 1 ⟹
       ads + adt + aap + aaq = 1 ⟹
       ada + aax + acz + acy = 1 ⟹
       aaf + aae + aac + aag = 1 ⟹
       aal + acu + acs + act = 1 ⟹
       aas + aar + xb + aat = 1 ⟹
       zk + zl + zj + zi = 1 ⟹
       ack + acj + xc + aci = 1 ⟹
       aav + aaw + aah + xd = 1 ⟹
       abt + xo + abu + xn = 1 ⟹
       adc + abz + add + ade = 1 ⟹
       xt + zz + aab + aaa = 1 ⟹
       adq + xl + adr + adb = 1 ⟹
       zf + ze + yh + yi = 1 ⟹
       aao + aan + aam + xe = 1 ⟹
       abk + aby + abj + abx = 1 ⟹
       yp + yo + xm + yn = 1 ⟹
       yl + yk + yj + ym = 1 ⟹
       acw + acv + acx + xg = 1 ⟹
       adk + adg + adj + adf = 1 ⟹
       adv + yx + xf + adu = 1 ⟹
       abn = abl ⟹
       abm = zv ⟹
       adm = xk ⟹
       xp = ace ⟹
       adt = aap ⟹
       aax = acz ⟹
       acy = ada ⟹
       ade = abz ⟹
       add = adc ⟹
       yn = yp ⟹
       xm = yo ⟹
       acx = acw ⟹
       xg = acw ⟹
       acv = acw ⟹
       yd = 0 ∨ yb = 0 ⟹
       xh = 0 ∨ ye = 0 ⟹
       yv = 0 ⟹
       adz = 0 ⟹
       zx = 0 ⟹
       yy = 0 ∨ za = 0 ⟹
       xq = 0 ⟹
       ado = 0 ⟹
       aau = 0 ⟹
       abm = 0 ∨ zv = 0 ⟹
       abi = 0 ⟹
       abp = 0 ⟹
       acc = 0 ∨ xi = 0 ⟹
       acl = 0 ⟹
       xv = 0 ∨ xr = 0 ⟹
       xj = 0 ⟹
       xx = 0 ⟹
       adx = 0 ⟹
       yr = 0 ∨ abc = 0 ⟹
       aaj = 0 ⟹
       aaz = 0 ⟹
       abf = 0 ⟹
       zn = 0 ∨ abw = 0 ⟹
       adm = 0 ∨ xk = 0 ⟹
       xp = 0 ∨ ace = 0 ⟹
       adt = 0 ∨ aap = 0 ⟹
       aax = 0 ∨ acz = 0 ⟹
       aae = 0 ⟹
       aar = 0 ⟹
       zl = 0 ⟹
       aaw = 0 ⟹
       xo = 0 ∨ abu = 0 ⟹
       xl = 0 ∨ adr = 0 ⟹
       ze = 0 ⟹
       aan = 0 ⟹
       xm = 0 ⟹
       yo = 0 ⟹
       yk = 0 ⟹
       yx = 0 ⟹
       (yr + abd < abm + abl ∨
        yr + (abd + abb)
        < abm + (abl + abn)) ∨
       yr + abd = abm + abl ∧
       yr + (abd + abb) =
       abm + (abl + abn) ⟹
       adb + adr < xn + abu ∨
       adb + adr = xn + abu ⟹
       (abl < abt ∨ abl + zv < abt + xo) ∨
       abl = abt ∧ abl + zv = abt + xo ⟹
       yd + yc < abc + abd ∨
       yd + yc = abc + abd ⟹
       aca + xp < abb + yr ∨
       aca + xp = abb + yr ⟹
       acb + acc < xu + xv ∨
       acb + acc = xu + xv ⟹
       (yq + xq < xu + xr ∨
        yq + (xq + zp) < xu + (xr + xw)) ∨
       yq + xq = xu + xr ∧
       yq + (xq + zp) = xu + (xr + xw) ⟹
       (zw < xw ∨
        zw + zx < xw + xv ∨
        zw + (zx + zy) < xw + (xv + xu)) ∨
       zw = xw ∧
       zw + zx = xw + xv ∧
       zw + (zx + zy) = xw + (xv + xu) ⟹
       xs + yw < zs + zt ∨
       xs + yw = zs + zt ⟹
       aab + xt < ye + yf ∨
       aab + xt = ye + yf ⟹
       (ya + yb < yg + ye ∨
        ya + (yb + yc) < yg + (ye + yf)) ∨
       ya + yb = yg + ye ∧
       ya + (yb + yc) = yg + (ye + yf) ⟹
       (xu + xv < acb + acc ∨
        xu + (xv + xw) < acb + (acc + acd)) ∨
       xu + xv = acb + acc ∧
       xu + (xv + xw) = acb + (acc + acd) ⟹
       (zs + xx < xz + zy ∨
        zs + (xx + xy) < xz + (zy + zw)) ∨
       zs + xx = xz + zy ∧
       zs + (xx + xy) = xz + (zy + zw) ⟹
       (zs + zt < xz + zy ∨
        zs + (zt + xy) < xz + (zy + zw)) ∨
       zs + zt = xz + zy ∧
       zs + (zt + xy) = xz + (zy + zw) ⟹
       yg + ye < ya + yb ∨
       yg + ye = ya + yb ⟹
       (abd < yc ∨ abd + abc < yc + yd) ∨
       abd = yc ∧ abd + abc = yc + yd ⟹
       (ye + yf < adr + adq ∨
        ye + (yf + yg) < adr + (adq + adb)) ∨
       ye + yf = adr + adq ∧
       ye + (yf + yg) = adr + (adq + adb) ⟹
       yh + yi < ym + yj ∨
       yh + yi = ym + yj ⟹
       (abp + abq < yk + yl ∨
        abp + (abq + abo) < yk + (yl + ym)) ∨
       abp + abq = yk + yl ∧
       abp + (abq + abo) = yk + (yl + ym) ⟹
       (yn < zp ∨
        yn + yo < zp + zo ∨
        yn + (yo + yp) < zp + (zo + yq)) ∨
       yn = zp ∧
       yn + yo = zp + zo ∧
       yn + (yo + yp) = zp + (zo + yq) ⟹
       (abb + yr < aca + ace ∨
        abb + (yr + abd)
        < aca + (ace + acf)) ∨
       abb + yr = aca + ace ∧
       abb + (yr + abd) =
       aca + (ace + acf) ⟹
       adw + zg < abe + ys ∨
       adw + zg = abe + ys ⟹
       zd + abq < ys + abg ∨
       zd + abq = ys + abg ⟹
       yt + abs < aby + abk ∨
       yt + abs = aby + abk ⟹
       (yu < abx ∨
        yu + yv < abx + aby ∨
        yu + (yv + yw) < abx + (aby + abk)) ∨
       yu = abx ∧
       yu + yv = abx + aby ∧
       yu + (yv + yw) = abx + (aby + abk) ⟹
       aae + aaf < yx + adv ∨
       aae + aaf = yx + adv ⟹
       abj + abk < yy + zb ∨
       abj + abk = yy + zb ⟹
       (abb < yz ∨
        abb + abc < yz + za ∨
        abb + (abc + abd) < yz + (za + zb)) ∨
       abb = yz ∧
       abb + abc = yz + za ∧
       abb + (abc + abd) = yz + (za + zb) ⟹
       (acg + zc < zd + abq ∨
        acg + (zc + ach)
        < zd + (abq + abo)) ∨
       acg + zc = zd + abq ∧
       acg + (zc + ach) =
       zd + (abq + abo) ⟹
       ze + zf < aau + acm ∨
       ze + zf = aau + acm ⟹
       (zg + ady < acn + acm ∨
        zg + (ady + adw)
        < acn + (acm + aco)) ∨
       zg + ady = acn + acm ∧
       zg + (ady + adw) =
       acn + (acm + aco) ⟹
       aay + zh < zi + zj ∨
       aay + zh = zi + zj ⟹
       (zy < zk ∨ zy + zx < zk + zl) ∨
       zy = zk ∧ zy + zx = zk + zl ⟹
       (adn + adm < zm + zn ∨
        adn + (adm + adl)
        < zm + (zn + abv)) ∨
       adn + adm = zm + zn ∧
       adn + (adm + adl) =
       zm + (zn + abv) ⟹
       zo + zp < zs + zt ∨
       zo + zp = zs + zt ⟹
       zq + zr < zs + zt ∨
       zq + zr = zs + zt ⟹
       (aai < adi ∨ aai + aaj < adi + adh) ∨
       aai = adi ∧ aai + aaj = adi + adh ⟹
       (abr < acj ∨
        abr + (abs + zu)
        < acj + (aci + ack)) ∨
       abr = acj ∧
       abr + (abs + zu) =
       acj + (aci + ack) ⟹
       (abn < zw ∨
        abn + (zv + abl) < zw + (zx + zy)) ∨
       abn = zw ∧
       abn + (zv + abl) = zw + (zx + zy) ⟹
       (zz + aaa < act + acu ∨
        zz + (aaa + aab)
        < act + (acu + aal)) ∨
       zz + aaa = act + acu ∧
       zz + (aaa + aab) =
       act + (acu + aal) ⟹
       (aam < aac ∨
        aam + (aan + aao)
        < aac + (aae + aaf)) ∨
       aam = aac ∧
       aam + (aan + aao) =
       aac + (aae + aaf) ⟹
       (aaj + aak < aae + aaf ∨
        aaj + (aak + aad)
        < aae + (aaf + aag)) ∨
       aaj + aak = aae + aaf ∧
       aaj + (aak + aad) =
       aae + (aaf + aag) ⟹
       (aah < aai ∨
        aah + (aaw + aav)
        < aai + (aaj + aak)) ∨
       aah = aai ∧
       aah + (aaw + aav) =
       aai + (aaj + aak) ⟹
       act + (acu + aal)
       < aam + (aan + aao) ∨
       act + (acu + aal) =
       aam + (aan + aao) ⟹
       (ads < aat ∨
        ads + (aap + aaq)
        < aat + (aar + aas)) ∨
       ads = aat ∧
       ads + (aap + aaq) =
       aat + (aar + aas) ⟹
       (aaz + aba < aar + aas ∨
        aaz + (aba + aay)
        < aar + (aas + aat)) ∨
       aaz + aba = aar + aas ∧
       aaz + (aba + aay) =
       aar + (aas + aat) ⟹
       (acm < aav ∨ acm + aau < aav + aaw) ∨
       acm = aav ∧ acm + aau = aav + aaw ⟹
       (acy < aay ∨
        acy + (aax + ada)
        < aay + (aaz + aba)) ∨
       acy = aay ∧
       acy + (aax + ada) =
       aay + (aaz + aba) ⟹
       abb + (abc + abd)
       < abe + (abf + abg) ∨
       abb + (abc + abd) =
       abe + (abf + abg) ⟹
       (abh < abj ∨ abh + abi < abj + abk) ∨
       abh = abj ∧ abh + abi = abj + abk ⟹
       abl + (abm + abn)
       < abo + (abp + abq) ∨
       abl + (abm + abn) =
       abo + (abp + abq) ⟹
       (acj < abr ∨ acj + aci < abr + abs) ∨
       acj = abr ∧ acj + aci = abr + abs ⟹
       (abt < abv ∨ abt + abu < abv + abw) ∨
       abt = abv ∧ abt + abu = abv + abw ⟹
       (abx < adc ∨ abx + aby < adc + abz) ∨
       abx = adc ∧ abx + aby = adc + abz ⟹
       (acf < acd ∨
        acf + ace < acd + acc ∨
        acf + (ace + aca)
        < acd + (acc + acb)) ∨
       acf = acd ∧
       acf + ace = acd + acc ∧
       acf + (ace + aca) =
       acd + (acc + acb) ⟹
       acc + acd < ace + acf ∨
       acc + acd = ace + acf ⟹
       (acg < acq ∨ acg + ach < acq + acr) ∨
       acg = acq ∧ acg + ach = acq + acr ⟹
       aci + (acj + ack)
       < acr + (acl + acp) ∨
       aci + (acj + ack) =
       acr + (acl + acp) ⟹
       (acm < acp ∨
        acm + acn < acp + acq ∨
        acm + (acn + aco)
        < acp + (acq + acr)) ∨
       acm = acp ∧
       acm + acn = acp + acq ∧
       acm + (acn + aco) =
       acp + (acq + acr) ⟹
       (acs + act < acv + acw ∨
        acs + (act + acu)
        < acv + (acw + acx)) ∨
       acs + act = acv + acw ∧
       acs + (act + acu) =
       acv + (acw + acx) ⟹
       (acy + acz < adb + adr ∨
        acy + (acz + ada)
        < adb + (adr + adq)) ∨
       acy + acz = adb + adr ∧
       acy + (acz + ada) =
       adb + (adr + adq) ⟹
       (adc + add < adf + adg ∨
        adc + (add + ade)
        < adf + (adg + adk)) ∨
       adc + add = adf + adg ∧
       adc + (add + ade) =
       adf + (adg + adk) ⟹
       adh + adi < adj + adk ∨
       adh + adi = adj + adk ⟹
       (adl < aec ∨
        adl + (adm + adn)
        < aec + (ado + adp)) ∨
       adl = aec ∧
       adl + (adm + adn) =
       aec + (ado + adp) ⟹
       (adq < ads ∨ adq + adr < ads + adt) ∨
       adq = ads ∧ adq + adr = ads + adt ⟹
       adu + adv < aed + aea ∨
       adu + adv = aed + aea ⟹
       (adw < aee ∨
        adw + (adx + ady)
        < aee + (adz + aea)) ∨
       adw = aee ∧
       adw + (adx + ady) =
       aee + (adz + aea) ⟹
       (aeb < aed ∨ aeb + aec < aed + aee) ∨
       aeb = aed ∧ aeb + aec = aed + aee ⟹
       False