# [isabelle] Solving big quantifier-free linear real arithmetic goals

```Hallo,

```
I am currently working on some Social Choice Theory. The proof basically works by deriving a number of equalities and inequalities over real numbers and then showing that they are inconsistent.
```
```
I have already derived these conditions and now need to show that they are actually inconsistent. This is goal1 in the attachment. Here, pmf is from HOL-Probability and sds, R1, R2, a, b, c, d etc. are constants/fixed locale variables whose properties are irrelevant for this goal. To emphasise this: I can restate the goal by generalising it a bit, introducing real variables for all the expressions (see goal2). If one simplifies this a bit and eliminates redundant variables, one obtains goal3.
```
I tried the following things:
```
â smt (i.e. Z3) is able to solve goal1 within .3 seconds; proof reconstruction takes another 12 seconds. â smt solves goal2 within .5 seconds; proof reconstruction seems to take longer than my patience will permit though.
```â smt solves goal3 within .3 seconds; proof reconstruction takes 67 seconds.
```
â Both goals should be solvable by linarith in theory. I tried it and gave up after an hour or so.
```
This raises the following questions:
â Why is this trivial for Z3 but impossible for linarith?
â Is there any hope of tweaking linarith to get this proof through?
```
â Why does proof reconstruction take so much longer on goal2 and goal3, even though they are arguably âsimplerâ?
```
```
I know that proofs using smt are not allowed in the AFP, so the prospect that I can only prove this with smt is a bit troubling.
```

```
Incidentally, another question: Is there any easy way to turn something like goal1 into something like goal2, i.e. generalise all real non-literals in a term to real variables? I wrote my own very ad-hoc tactic for this, but it seems like quite a common use case.
```

Cheers,

Manuel

```
```proof (prove)
using this:
0 â pmf (sds R1) a â
0 â pmf (sds R1) b â
0 â pmf (sds R1) c â 0 â pmf (sds R1) d
0 â pmf (sds R2) a â
0 â pmf (sds R2) b â
0 â pmf (sds R2) c â 0 â pmf (sds R2) d
0 â pmf (sds R3) a â
0 â pmf (sds R3) b â
0 â pmf (sds R3) c â 0 â pmf (sds R3) d
0 â pmf (sds R4) a â
0 â pmf (sds R4) b â
0 â pmf (sds R4) c â 0 â pmf (sds R4) d
0 â pmf (sds R5) a â
0 â pmf (sds R5) b â
0 â pmf (sds R5) c â 0 â pmf (sds R5) d
0 â pmf (sds R6) a â
0 â pmf (sds R6) b â
0 â pmf (sds R6) c â 0 â pmf (sds R6) d
0 â pmf (sds R7) a â
0 â pmf (sds R7) b â
0 â pmf (sds R7) c â 0 â pmf (sds R7) d
0 â pmf (sds R8) a â
0 â pmf (sds R8) b â
0 â pmf (sds R8) c â 0 â pmf (sds R8) d
0 â pmf (sds R9) a â
0 â pmf (sds R9) b â
0 â pmf (sds R9) c â 0 â pmf (sds R9) d
0 â pmf (sds R10) a â
0 â pmf (sds R10) b â
0 â pmf (sds R10) c â
0 â pmf (sds R10) d
0 â pmf (sds R11) a â
0 â pmf (sds R11) b â
0 â pmf (sds R11) c â
0 â pmf (sds R11) d
0 â pmf (sds R12) a â
0 â pmf (sds R12) b â
0 â pmf (sds R12) c â
0 â pmf (sds R12) d
0 â pmf (sds R13) a â
0 â pmf (sds R13) b â
0 â pmf (sds R13) c â
0 â pmf (sds R13) d
0 â pmf (sds R14) a â
0 â pmf (sds R14) b â
0 â pmf (sds R14) c â
0 â pmf (sds R14) d
0 â pmf (sds R15) a â
0 â pmf (sds R15) b â
0 â pmf (sds R15) c â
0 â pmf (sds R15) d
0 â pmf (sds R16) a â
0 â pmf (sds R16) b â
0 â pmf (sds R16) c â
0 â pmf (sds R16) d
0 â pmf (sds R17) a â
0 â pmf (sds R17) b â
0 â pmf (sds R17) c â
0 â pmf (sds R17) d
0 â pmf (sds R18) a â
0 â pmf (sds R18) b â
0 â pmf (sds R18) c â
0 â pmf (sds R18) d
0 â pmf (sds R19) a â
0 â pmf (sds R19) b â
0 â pmf (sds R19) c â
0 â pmf (sds R19) d
0 â pmf (sds R20) a â
0 â pmf (sds R20) b â
0 â pmf (sds R20) c â
0 â pmf (sds R20) d
0 â pmf (sds R21) a â
0 â pmf (sds R21) b â
0 â pmf (sds R21) c â
0 â pmf (sds R21) d
0 â pmf (sds R22) a â
0 â pmf (sds R22) b â
0 â pmf (sds R22) c â
0 â pmf (sds R22) d
0 â pmf (sds R23) a â
0 â pmf (sds R23) b â
0 â pmf (sds R23) c â
0 â pmf (sds R23) d
0 â pmf (sds R24) a â
0 â pmf (sds R24) b â
0 â pmf (sds R24) c â
0 â pmf (sds R24) d
0 â pmf (sds R25) a â
0 â pmf (sds R25) b â
0 â pmf (sds R25) c â
0 â pmf (sds R25) d
0 â pmf (sds R26) a â
0 â pmf (sds R26) b â
0 â pmf (sds R26) c â
0 â pmf (sds R26) d
0 â pmf (sds R27) a â
0 â pmf (sds R27) b â
0 â pmf (sds R27) c â
0 â pmf (sds R27) d
0 â pmf (sds R28) a â
0 â pmf (sds R28) b â
0 â pmf (sds R28) c â
0 â pmf (sds R28) d
0 â pmf (sds R29) a â
0 â pmf (sds R29) b â
0 â pmf (sds R29) c â
0 â pmf (sds R29) d
0 â pmf (sds R30) a â
0 â pmf (sds R30) b â
0 â pmf (sds R30) c â
0 â pmf (sds R30) d
0 â pmf (sds R31) a â
0 â pmf (sds R31) b â
0 â pmf (sds R31) c â
0 â pmf (sds R31) d
0 â pmf (sds R32) a â
0 â pmf (sds R32) b â
0 â pmf (sds R32) c â
0 â pmf (sds R32) d
0 â pmf (sds R33) a â
0 â pmf (sds R33) b â
0 â pmf (sds R33) c â
0 â pmf (sds R33) d
0 â pmf (sds R34) a â
0 â pmf (sds R34) b â
0 â pmf (sds R34) c â
0 â pmf (sds R34) d
0 â pmf (sds R35) a â
0 â pmf (sds R35) b â
0 â pmf (sds R35) c â
0 â pmf (sds R35) d
0 â pmf (sds R36) a â
0 â pmf (sds R36) b â
0 â pmf (sds R36) c â
0 â pmf (sds R36) d
0 â pmf (sds R37) a â
0 â pmf (sds R37) b â
0 â pmf (sds R37) c â
0 â pmf (sds R37) d
0 â pmf (sds R38) a â
0 â pmf (sds R38) b â
0 â pmf (sds R38) c â
0 â pmf (sds R38) d
0 â pmf (sds R39) a â
0 â pmf (sds R39) b â
0 â pmf (sds R39) c â
0 â pmf (sds R39) d
0 â pmf (sds R40) a â
0 â pmf (sds R40) b â
0 â pmf (sds R40) c â
0 â pmf (sds R40) d
0 â pmf (sds R41) a â
0 â pmf (sds R41) b â
0 â pmf (sds R41) c â
0 â pmf (sds R41) d
0 â pmf (sds R42) a â
0 â pmf (sds R42) b â
0 â pmf (sds R42) c â
0 â pmf (sds R42) d
0 â pmf (sds R43) a â
0 â pmf (sds R43) b â
0 â pmf (sds R43) c â
0 â pmf (sds R43) d
0 â pmf (sds R44) a â
0 â pmf (sds R44) b â
0 â pmf (sds R44) c â
0 â pmf (sds R44) d
0 â pmf (sds R45) a â
0 â pmf (sds R45) b â
0 â pmf (sds R45) c â
0 â pmf (sds R45) d
0 â pmf (sds R46) a â
0 â pmf (sds R46) b â
0 â pmf (sds R46) c â
0 â pmf (sds R46) d
0 â pmf (sds R47) a â
0 â pmf (sds R47) b â
0 â pmf (sds R47) c â
0 â pmf (sds R47) d
pmf (sds R1) a + pmf (sds R1) b +
pmf (sds R1) c +
pmf (sds R1) d =
1
pmf (sds R2) a + pmf (sds R2) b +
pmf (sds R2) c +
pmf (sds R2) d =
1
pmf (sds R3) a + pmf (sds R3) b +
pmf (sds R3) c +
pmf (sds R3) d =
1
pmf (sds R4) a + pmf (sds R4) b +
pmf (sds R4) c +
pmf (sds R4) d =
1
pmf (sds R5) a + pmf (sds R5) b +
pmf (sds R5) c +
pmf (sds R5) d =
1
pmf (sds R6) a + pmf (sds R6) b +
pmf (sds R6) c +
pmf (sds R6) d =
1
pmf (sds R7) a + pmf (sds R7) b +
pmf (sds R7) c +
pmf (sds R7) d =
1
pmf (sds R8) a + pmf (sds R8) b +
pmf (sds R8) c +
pmf (sds R8) d =
1
pmf (sds R9) a + pmf (sds R9) b +
pmf (sds R9) c +
pmf (sds R9) d =
1
pmf (sds R10) a + pmf (sds R10) b +
pmf (sds R10) c +
pmf (sds R10) d =
1
pmf (sds R11) a + pmf (sds R11) b +
pmf (sds R11) c +
pmf (sds R11) d =
1
pmf (sds R12) a + pmf (sds R12) b +
pmf (sds R12) c +
pmf (sds R12) d =
1
pmf (sds R13) a + pmf (sds R13) b +
pmf (sds R13) c +
pmf (sds R13) d =
1
pmf (sds R14) a + pmf (sds R14) b +
pmf (sds R14) c +
pmf (sds R14) d =
1
pmf (sds R15) a + pmf (sds R15) b +
pmf (sds R15) c +
pmf (sds R15) d =
1
pmf (sds R16) a + pmf (sds R16) b +
pmf (sds R16) c +
pmf (sds R16) d =
1
pmf (sds R17) a + pmf (sds R17) b +
pmf (sds R17) c +
pmf (sds R17) d =
1
pmf (sds R18) a + pmf (sds R18) b +
pmf (sds R18) c +
pmf (sds R18) d =
1
pmf (sds R19) a + pmf (sds R19) b +
pmf (sds R19) c +
pmf (sds R19) d =
1
pmf (sds R20) a + pmf (sds R20) b +
pmf (sds R20) c +
pmf (sds R20) d =
1
pmf (sds R21) a + pmf (sds R21) b +
pmf (sds R21) c +
pmf (sds R21) d =
1
pmf (sds R22) a + pmf (sds R22) b +
pmf (sds R22) c +
pmf (sds R22) d =
1
pmf (sds R23) a + pmf (sds R23) b +
pmf (sds R23) c +
pmf (sds R23) d =
1
pmf (sds R24) a + pmf (sds R24) b +
pmf (sds R24) c +
pmf (sds R24) d =
1
pmf (sds R25) a + pmf (sds R25) b +
pmf (sds R25) c +
pmf (sds R25) d =
1
pmf (sds R26) a + pmf (sds R26) b +
pmf (sds R26) c +
pmf (sds R26) d =
1
pmf (sds R27) a + pmf (sds R27) b +
pmf (sds R27) c +
pmf (sds R27) d =
1
pmf (sds R28) a + pmf (sds R28) b +
pmf (sds R28) c +
pmf (sds R28) d =
1
pmf (sds R29) a + pmf (sds R29) b +
pmf (sds R29) c +
pmf (sds R29) d =
1
pmf (sds R30) a + pmf (sds R30) b +
pmf (sds R30) c +
pmf (sds R30) d =
1
pmf (sds R31) a + pmf (sds R31) b +
pmf (sds R31) c +
pmf (sds R31) d =
1
pmf (sds R32) a + pmf (sds R32) b +
pmf (sds R32) c +
pmf (sds R32) d =
1
pmf (sds R33) a + pmf (sds R33) b +
pmf (sds R33) c +
pmf (sds R33) d =
1
pmf (sds R34) a + pmf (sds R34) b +
pmf (sds R34) c +
pmf (sds R34) d =
1
pmf (sds R35) a + pmf (sds R35) b +
pmf (sds R35) c +
pmf (sds R35) d =
1
pmf (sds R36) a + pmf (sds R36) b +
pmf (sds R36) c +
pmf (sds R36) d =
1
pmf (sds R37) a + pmf (sds R37) b +
pmf (sds R37) c +
pmf (sds R37) d =
1
pmf (sds R38) a + pmf (sds R38) b +
pmf (sds R38) c +
pmf (sds R38) d =
1
pmf (sds R39) a + pmf (sds R39) b +
pmf (sds R39) c +
pmf (sds R39) d =
1
pmf (sds R40) a + pmf (sds R40) b +
pmf (sds R40) c +
pmf (sds R40) d =
1
pmf (sds R41) a + pmf (sds R41) b +
pmf (sds R41) c +
pmf (sds R41) d =
1
pmf (sds R42) a + pmf (sds R42) b +
pmf (sds R42) c +
pmf (sds R42) d =
1
pmf (sds R43) a + pmf (sds R43) b +
pmf (sds R43) c +
pmf (sds R43) d =
1
pmf (sds R44) a + pmf (sds R44) b +
pmf (sds R44) c +
pmf (sds R44) d =
1
pmf (sds R45) a + pmf (sds R45) b +
pmf (sds R45) c +
pmf (sds R45) d =
1
pmf (sds R46) a + pmf (sds R46) b +
pmf (sds R46) c +
pmf (sds R46) d =
1
pmf (sds R47) a + pmf (sds R47) b +
pmf (sds R47) c +
pmf (sds R47) d =
1
pmf (sds R10) d = pmf (sds R10) a
pmf (sds R10) c = pmf (sds R10) b
pmf (sds R26) c = pmf (sds R26) b
pmf (sds R27) c = pmf (sds R27) b
pmf (sds R28) b = pmf (sds R28) c
pmf (sds R29) b = pmf (sds R29) c
pmf (sds R29) d = pmf (sds R29) a
pmf (sds R37) d = pmf (sds R37) b
pmf (sds R37) c = pmf (sds R37) a
pmf (sds R43) d = pmf (sds R43) a
pmf (sds R43) c = pmf (sds R43) b
pmf (sds R45) c = pmf (sds R45) a
pmf (sds R45) d = pmf (sds R45) a
pmf (sds R45) b = pmf (sds R45) a
pmf (sds R1) b = 0 â pmf (sds R1) c = 0
pmf (sds R2) b = 0 â pmf (sds R2) c = 0
pmf (sds R3) b = 0
pmf (sds R4) b = 0
pmf (sds R5) b = 0
pmf (sds R6) c = 0 â pmf (sds R6) b = 0
pmf (sds R7) b = 0
pmf (sds R8) b = 0
pmf (sds R9) b = 0
pmf (sds R10) c = 0 â pmf (sds R10) b = 0
pmf (sds R11) b = 0
pmf (sds R12) b = 0
pmf (sds R13) b = 0 â pmf (sds R13) c = 0
pmf (sds R14) b = 0
pmf (sds R15) c = 0 â pmf (sds R15) b = 0
pmf (sds R16) b = 0
pmf (sds R17) b = 0
pmf (sds R18) b = 0
pmf (sds R19) c = 0 â pmf (sds R19) b = 0
pmf (sds R21) b = 0
pmf (sds R22) b = 0
pmf (sds R23) b = 0
pmf (sds R25) b = 0 â pmf (sds R25) c = 0
pmf (sds R26) c = 0 â pmf (sds R26) b = 0
pmf (sds R27) c = 0 â pmf (sds R27) b = 0
pmf (sds R28) b = 0 â pmf (sds R28) c = 0
pmf (sds R29) b = 0 â pmf (sds R29) c = 0
pmf (sds R30) b = 0
pmf (sds R32) b = 0
pmf (sds R33) b = 0
pmf (sds R35) b = 0
pmf (sds R36) b = 0 â pmf (sds R36) c = 0
pmf (sds R39) b = 0 â pmf (sds R39) c = 0
pmf (sds R40) b = 0
pmf (sds R41) b = 0
pmf (sds R43) c = 0
pmf (sds R43) b = 0
pmf (sds R44) b = 0
pmf (sds R47) b = 0
(pmf (sds R19) c + pmf (sds R19) a
< pmf (sds R10) c + pmf (sds R10) a â
pmf (sds R19) c +
(pmf (sds R19) a + pmf (sds R19) d)
< pmf (sds R10) c +
(pmf (sds R10) a + pmf (sds R10) d)) â
pmf (sds R19) c + pmf (sds R19) a =
pmf (sds R10) c + pmf (sds R10) a â
pmf (sds R19) c +
(pmf (sds R19) a + pmf (sds R19) d) =
pmf (sds R10) c +
(pmf (sds R10) a + pmf (sds R10) d)
pmf (sds R39) d + pmf (sds R39) c
< pmf (sds R36) d + pmf (sds R36) c â
pmf (sds R39) d + pmf (sds R39) c =
pmf (sds R36) d + pmf (sds R36) c
(pmf (sds R10) a < pmf (sds R36) a â
pmf (sds R10) a + pmf (sds R10) b
< pmf (sds R36) a + pmf (sds R36) b) â
pmf (sds R10) a = pmf (sds R36) a â
pmf (sds R10) a + pmf (sds R10) b =
pmf (sds R36) a + pmf (sds R36) b
pmf (sds R1) b + pmf (sds R1) a
< pmf (sds R19) b + pmf (sds R19) a â
pmf (sds R1) b + pmf (sds R1) a =
pmf (sds R19) b + pmf (sds R19) a
pmf (sds R27) d + pmf (sds R27) c
< pmf (sds R19) d + pmf (sds R19) c â
pmf (sds R27) d + pmf (sds R27) c =
pmf (sds R19) d + pmf (sds R19) c
pmf (sds R13) d + pmf (sds R13) b
< pmf (sds R15) d + pmf (sds R15) c â
pmf (sds R13) d + pmf (sds R13) b =
pmf (sds R15) d + pmf (sds R15) c
(pmf (sds R7) d + pmf (sds R7) b
< pmf (sds R15) d + pmf (sds R15) b â
pmf (sds R7) d +
(pmf (sds R7) b + pmf (sds R7) a)
< pmf (sds R15) d +
(pmf (sds R15) b + pmf (sds R15) a)) â
pmf (sds R7) d + pmf (sds R7) b =
pmf (sds R15) d + pmf (sds R15) b â
pmf (sds R7) d +
(pmf (sds R7) b + pmf (sds R7) a) =
pmf (sds R15) d +
(pmf (sds R15) b + pmf (sds R15) a)
(pmf (sds R5) d < pmf (sds R15) a â
pmf (sds R5) d + pmf (sds R5) b
< pmf (sds R15) a + pmf (sds R15) c â
pmf (sds R5) d +
(pmf (sds R5) b + pmf (sds R5) a)
< pmf (sds R15) a +
(pmf (sds R15) c + pmf (sds R15) d)) â
pmf (sds R5) d = pmf (sds R15) a â
pmf (sds R5) d + pmf (sds R5) b =
pmf (sds R15) a + pmf (sds R15) c â
pmf (sds R5) d +
(pmf (sds R5) b + pmf (sds R5) a) =
pmf (sds R15) a +
(pmf (sds R15) c + pmf (sds R15) d)
pmf (sds R3) c + pmf (sds R3) a
< pmf (sds R17) c + pmf (sds R17) a â
pmf (sds R3) c + pmf (sds R3) a =
pmf (sds R17) c + pmf (sds R17) a
pmf (sds R38) c + pmf (sds R38) a
< pmf (sds R2) c + pmf (sds R2) a â
pmf (sds R38) c + pmf (sds R38) a =
pmf (sds R2) c + pmf (sds R2) a
(pmf (sds R1) d + pmf (sds R1) c
< pmf (sds R2) d + pmf (sds R2) c â
pmf (sds R1) d +
(pmf (sds R1) c + pmf (sds R1) a)
< pmf (sds R2) d +
(pmf (sds R2) c + pmf (sds R2) a)) â
pmf (sds R1) d + pmf (sds R1) c =
pmf (sds R2) d + pmf (sds R2) c â
pmf (sds R1) d +
(pmf (sds R1) c + pmf (sds R1) a) =
pmf (sds R2) d +
(pmf (sds R2) c + pmf (sds R2) a)
(pmf (sds R15) d + pmf (sds R15) c
< pmf (sds R13) d + pmf (sds R13) b â
pmf (sds R15) d +
(pmf (sds R15) c + pmf (sds R15) a)
< pmf (sds R13) d +
(pmf (sds R13) b + pmf (sds R13) a)) â
pmf (sds R15) d + pmf (sds R15) c =
pmf (sds R13) d + pmf (sds R13) b â
pmf (sds R15) d +
(pmf (sds R15) c + pmf (sds R15) a) =
pmf (sds R13) d +
(pmf (sds R13) b + pmf (sds R13) a)
(pmf (sds R17) c + pmf (sds R17) b
< pmf (sds R5) c + pmf (sds R5) a â
pmf (sds R17) c +
(pmf (sds R17) b + pmf (sds R17) d)
< pmf (sds R5) c +
(pmf (sds R5) a + pmf (sds R5) d)) â
pmf (sds R17) c + pmf (sds R17) b =
pmf (sds R5) c + pmf (sds R5) a â
pmf (sds R17) c +
(pmf (sds R17) b + pmf (sds R17) d) =
pmf (sds R5) c +
(pmf (sds R5) a + pmf (sds R5) d)
(pmf (sds R17) c + pmf (sds R17) a
< pmf (sds R5) c + pmf (sds R5) a â
pmf (sds R17) c +
(pmf (sds R17) a + pmf (sds R17) d)
< pmf (sds R5) c +
(pmf (sds R5) a + pmf (sds R5) d)) â
pmf (sds R17) c + pmf (sds R17) a =
pmf (sds R5) c + pmf (sds R5) a â
pmf (sds R17) c +
(pmf (sds R17) a + pmf (sds R17) d) =
pmf (sds R5) c +
(pmf (sds R5) a + pmf (sds R5) d)
pmf (sds R2) d + pmf (sds R2) c
< pmf (sds R1) d + pmf (sds R1) c â
pmf (sds R2) d + pmf (sds R2) c =
pmf (sds R1) d + pmf (sds R1) c
(pmf (sds R19) a < pmf (sds R1) a â
pmf (sds R19) a + pmf (sds R19) b
< pmf (sds R1) a + pmf (sds R1) b) â
pmf (sds R19) a = pmf (sds R1) a â
pmf (sds R19) a + pmf (sds R19) b =
pmf (sds R1) a + pmf (sds R1) b
(pmf (sds R2) c + pmf (sds R2) a
< pmf (sds R39) c + pmf (sds R39) a â
pmf (sds R2) c +
(pmf (sds R2) a + pmf (sds R2) d)
< pmf (sds R39) c +
(pmf (sds R39) a + pmf (sds R39) d)) â
pmf (sds R2) c + pmf (sds R2) a =
pmf (sds R39) c + pmf (sds R39) a â
pmf (sds R2) c +
(pmf (sds R2) a + pmf (sds R2) d) =
pmf (sds R39) c +
(pmf (sds R39) a + pmf (sds R39) d)
pmf (sds R40) c + pmf (sds R40) d
< pmf (sds R44) d + pmf (sds R44) c â
pmf (sds R40) c + pmf (sds R40) d =
pmf (sds R44) d + pmf (sds R44) c
(pmf (sds R12) b + pmf (sds R12) a
< pmf (sds R44) b + pmf (sds R44) a â
pmf (sds R12) b +
(pmf (sds R12) a + pmf (sds R12) d)
< pmf (sds R44) b +
(pmf (sds R44) a + pmf (sds R44) d)) â
pmf (sds R12) b + pmf (sds R12) a =
pmf (sds R44) b + pmf (sds R44) a â
pmf (sds R12) b +
(pmf (sds R12) a + pmf (sds R12) d) =
pmf (sds R44) b +
(pmf (sds R44) a + pmf (sds R44) d)
(pmf (sds R43) d < pmf (sds R7) a â
pmf (sds R43) d + pmf (sds R43) b
< pmf (sds R7) a + pmf (sds R7) c â
pmf (sds R43) d +
(pmf (sds R43) b + pmf (sds R43) a)
< pmf (sds R7) a +
(pmf (sds R7) c + pmf (sds R7) d)) â
pmf (sds R43) d = pmf (sds R7) a â
pmf (sds R43) d + pmf (sds R43) b =
pmf (sds R7) a + pmf (sds R7) c â
pmf (sds R43) d +
(pmf (sds R43) b + pmf (sds R43) a) =
pmf (sds R7) a +
(pmf (sds R7) c + pmf (sds R7) d)
(pmf (sds R19) d + pmf (sds R19) c
< pmf (sds R27) d + pmf (sds R27) b â
pmf (sds R19) d +
(pmf (sds R19) c + pmf (sds R19) a)
< pmf (sds R27) d +
(pmf (sds R27) b + pmf (sds R27) a)) â
pmf (sds R19) d + pmf (sds R19) c =
pmf (sds R27) d + pmf (sds R27) b â
pmf (sds R19) d +
(pmf (sds R19) c + pmf (sds R19) a) =
pmf (sds R27) d +
(pmf (sds R27) b + pmf (sds R27) a)
pmf (sds R18) c + pmf (sds R18) d
< pmf (sds R23) d + pmf (sds R23) c â
pmf (sds R18) c + pmf (sds R18) d =
pmf (sds R23) d + pmf (sds R23) c
pmf (sds R12) c + pmf (sds R12) a
< pmf (sds R23) c + pmf (sds R23) a â
pmf (sds R12) c + pmf (sds R12) a =
pmf (sds R23) c + pmf (sds R23) a
pmf (sds R24) b + pmf (sds R24) a
< pmf (sds R42) b + pmf (sds R42) a â
pmf (sds R24) b + pmf (sds R24) a =
pmf (sds R42) b + pmf (sds R42) a
(pmf (sds R3) d < pmf (sds R42) d â
pmf (sds R3) d + pmf (sds R3) b
< pmf (sds R42) d + pmf (sds R42) b â
pmf (sds R3) d +
(pmf (sds R3) b + pmf (sds R3) a)
< pmf (sds R42) d +
(pmf (sds R42) b + pmf (sds R42) a)) â
pmf (sds R3) d = pmf (sds R42) d â
pmf (sds R3) d + pmf (sds R3) b =
pmf (sds R42) d + pmf (sds R42) b â
pmf (sds R3) d +
(pmf (sds R3) b + pmf (sds R3) a) =
pmf (sds R42) d +
(pmf (sds R42) b + pmf (sds R42) a)
pmf (sds R30) b + pmf (sds R30) a
< pmf (sds R47) b + pmf (sds R47) a â
pmf (sds R30) b + pmf (sds R30) a =
pmf (sds R47) b + pmf (sds R47) a
pmf (sds R42) c + pmf (sds R42) a
< pmf (sds R6) c + pmf (sds R6) a â
pmf (sds R42) c + pmf (sds R42) a =
pmf (sds R6) c + pmf (sds R6) a
(pmf (sds R19) d < pmf (sds R6) d â
pmf (sds R19) d + pmf (sds R19) b
< pmf (sds R6) d + pmf (sds R6) b â
pmf (sds R19) d +
(pmf (sds R19) b + pmf (sds R19) a)
< pmf (sds R6) d +
(pmf (sds R6) b + pmf (sds R6) a)) â
pmf (sds R19) d = pmf (sds R6) d â
pmf (sds R19) d + pmf (sds R19) b =
pmf (sds R6) d + pmf (sds R6) b â
pmf (sds R19) d +
(pmf (sds R19) b + pmf (sds R19) a) =
pmf (sds R6) d +
(pmf (sds R6) b + pmf (sds R6) a)
(pmf (sds R16) c + pmf (sds R16) a
< pmf (sds R12) c + pmf (sds R12) a â
pmf (sds R16) c +
(pmf (sds R16) a + pmf (sds R16) d)
< pmf (sds R12) c +
(pmf (sds R12) a + pmf (sds R12) d)) â
pmf (sds R16) c + pmf (sds R16) a =
pmf (sds R12) c + pmf (sds R12) a â
pmf (sds R16) c +
(pmf (sds R16) a + pmf (sds R16) d) =
pmf (sds R12) c +
(pmf (sds R12) a + pmf (sds R12) d)
pmf (sds R40) b + pmf (sds R40) a
< pmf (sds R9) b + pmf (sds R9) a â
pmf (sds R40) b + pmf (sds R40) a =
pmf (sds R9) b + pmf (sds R9) a
(pmf (sds R18) d + pmf (sds R18) a
< pmf (sds R9) d + pmf (sds R9) a â
pmf (sds R18) d +
(pmf (sds R18) a + pmf (sds R18) c)
< pmf (sds R9) d +
(pmf (sds R9) a + pmf (sds R9) c)) â
pmf (sds R18) d + pmf (sds R18) a =
pmf (sds R9) d + pmf (sds R9) a â
pmf (sds R18) d +
(pmf (sds R18) a + pmf (sds R18) c) =
pmf (sds R9) d +
(pmf (sds R9) a + pmf (sds R9) c)
pmf (sds R22) d + pmf (sds R22) c
< pmf (sds R33) d + pmf (sds R33) c â
pmf (sds R22) d + pmf (sds R22) c =
pmf (sds R33) d + pmf (sds R33) c
(pmf (sds R5) a < pmf (sds R33) a â
pmf (sds R5) a + pmf (sds R5) b
< pmf (sds R33) a + pmf (sds R33) b) â
pmf (sds R5) a = pmf (sds R33) a â
pmf (sds R5) a + pmf (sds R5) b =
pmf (sds R33) a + pmf (sds R33) b
(pmf (sds R26) d + pmf (sds R26) c
< pmf (sds R25) d + pmf (sds R25) b â
pmf (sds R26) d +
(pmf (sds R26) c + pmf (sds R26) a)
< pmf (sds R25) d +
(pmf (sds R25) b + pmf (sds R25) a)) â
pmf (sds R26) d + pmf (sds R26) c =
pmf (sds R25) d + pmf (sds R25) b â
pmf (sds R26) d +
(pmf (sds R26) c + pmf (sds R26) a) =
pmf (sds R25) d +
(pmf (sds R25) b + pmf (sds R25) a)
pmf (sds R7) c + pmf (sds R7) a
< pmf (sds R17) c + pmf (sds R17) a â
pmf (sds R7) c + pmf (sds R7) a =
pmf (sds R17) c + pmf (sds R17) a
pmf (sds R11) c + pmf (sds R11) a
< pmf (sds R17) c + pmf (sds R17) a â
pmf (sds R11) c + pmf (sds R11) a =
pmf (sds R17) c + pmf (sds R17) a
(pmf (sds R21) c < pmf (sds R20) a â
pmf (sds R21) c + pmf (sds R21) b
< pmf (sds R20) a + pmf (sds R20) c) â
pmf (sds R21) c = pmf (sds R20) a â
pmf (sds R21) c + pmf (sds R21) b =
pmf (sds R20) a + pmf (sds R20) c
(pmf (sds R24) c < pmf (sds R34) b â
pmf (sds R24) c +
(pmf (sds R24) a + pmf (sds R24) d)
< pmf (sds R34) b +
(pmf (sds R34) d + pmf (sds R34) a)) â
pmf (sds R24) c = pmf (sds R34) b â
pmf (sds R24) c +
(pmf (sds R24) a + pmf (sds R24) d) =
pmf (sds R34) b +
(pmf (sds R34) d + pmf (sds R34) a)
(pmf (sds R10) d < pmf (sds R5) d â
pmf (sds R10) d +
(pmf (sds R10) b + pmf (sds R10) a)
< pmf (sds R5) d +
(pmf (sds R5) b + pmf (sds R5) a)) â
pmf (sds R10) d = pmf (sds R5) d â
pmf (sds R10) d +
(pmf (sds R10) b + pmf (sds R10) a) =
pmf (sds R5) d +
(pmf (sds R5) b + pmf (sds R5) a)
(pmf (sds R38) b + pmf (sds R38) d
< pmf (sds R31) d + pmf (sds R31) b â
pmf (sds R38) b +
(pmf (sds R38) d + pmf (sds R38) c)
< pmf (sds R31) d +
(pmf (sds R31) b + pmf (sds R31) a)) â
pmf (sds R38) b + pmf (sds R38) d =
pmf (sds R31) d + pmf (sds R31) b â
pmf (sds R38) b +
(pmf (sds R38) d + pmf (sds R38) c) =
pmf (sds R31) d +
(pmf (sds R31) b + pmf (sds R31) a)
(pmf (sds R41) c < pmf (sds R30) c â
pmf (sds R41) c +
(pmf (sds R41) b + pmf (sds R41) a)
< pmf (sds R30) c +
(pmf (sds R30) b + pmf (sds R30) a)) â
pmf (sds R41) c = pmf (sds R30) c â
pmf (sds R41) c +
(pmf (sds R41) b + pmf (sds R41) a) =
pmf (sds R30) c +
(pmf (sds R30) b + pmf (sds R30) a)
(pmf (sds R21) b + pmf (sds R21) a
< pmf (sds R30) b + pmf (sds R30) a â
pmf (sds R21) b +
(pmf (sds R21) a + pmf (sds R21) d)
< pmf (sds R30) b +
(pmf (sds R30) a + pmf (sds R30) d)) â
pmf (sds R21) b + pmf (sds R21) a =
pmf (sds R30) b + pmf (sds R30) a â
pmf (sds R21) b +
(pmf (sds R21) a + pmf (sds R21) d) =
pmf (sds R30) b +
(pmf (sds R30) a + pmf (sds R30) d)
(pmf (sds R35) c < pmf (sds R21) c â
pmf (sds R35) c +
(pmf (sds R35) b + pmf (sds R35) a)
< pmf (sds R21) c +
(pmf (sds R21) b + pmf (sds R21) a)) â
pmf (sds R35) c = pmf (sds R21) c â
pmf (sds R35) c +
(pmf (sds R35) b + pmf (sds R35) a) =
pmf (sds R21) c +
(pmf (sds R21) b + pmf (sds R21) a)
pmf (sds R31) d +
(pmf (sds R31) b + pmf (sds R31) a)
< pmf (sds R41) c +
(pmf (sds R41) b + pmf (sds R41) a) â
pmf (sds R31) d +
(pmf (sds R31) b + pmf (sds R31) a) =
pmf (sds R41) c +
(pmf (sds R41) b + pmf (sds R41) a)
(pmf (sds R28) a < pmf (sds R32) d â
pmf (sds R28) a +
(pmf (sds R28) c + pmf (sds R28) d)
< pmf (sds R32) d +
(pmf (sds R32) b + pmf (sds R32) a)) â
pmf (sds R28) a = pmf (sds R32) d â
pmf (sds R28) a +
(pmf (sds R28) c + pmf (sds R28) d) =
pmf (sds R32) d +
(pmf (sds R32) b + pmf (sds R32) a)
(pmf (sds R22) b + pmf (sds R22) a
< pmf (sds R32) b + pmf (sds R32) a â
pmf (sds R22) b +
(pmf (sds R22) a + pmf (sds R22) d)
< pmf (sds R32) b +
(pmf (sds R32) a + pmf (sds R32) d)) â
pmf (sds R22) b + pmf (sds R22) a =
pmf (sds R32) b + pmf (sds R32) a â
pmf (sds R22) b +
(pmf (sds R22) a + pmf (sds R22) d) =
pmf (sds R32) b +
(pmf (sds R32) a + pmf (sds R32) d)
(pmf (sds R9) a < pmf (sds R35) a â
pmf (sds R9) a + pmf (sds R9) b
< pmf (sds R35) a + pmf (sds R35) b) â
pmf (sds R9) a = pmf (sds R35) a â
pmf (sds R9) a + pmf (sds R9) b =
pmf (sds R35) a + pmf (sds R35) b
(pmf (sds R29) d < pmf (sds R22) d â
pmf (sds R29) d +
(pmf (sds R29) b + pmf (sds R29) a)
< pmf (sds R22) d +
(pmf (sds R22) b + pmf (sds R22) a)) â
pmf (sds R29) d = pmf (sds R22) d â
pmf (sds R29) d +
(pmf (sds R29) b + pmf (sds R29) a) =
pmf (sds R22) d +
(pmf (sds R22) b + pmf (sds R22) a)
pmf (sds R19) d +
(pmf (sds R19) b + pmf (sds R19) a)
< pmf (sds R23) d +
(pmf (sds R23) b + pmf (sds R23) a) â
pmf (sds R19) d +
(pmf (sds R19) b + pmf (sds R19) a) =
pmf (sds R23) d +
(pmf (sds R23) b + pmf (sds R23) a)
(pmf (sds R11) d < pmf (sds R42) c â
pmf (sds R11) d + pmf (sds R11) b
< pmf (sds R42) c + pmf (sds R42) a) â
pmf (sds R11) d = pmf (sds R42) c â
pmf (sds R11) d + pmf (sds R11) b =
pmf (sds R42) c + pmf (sds R42) a
pmf (sds R10) a +
(pmf (sds R10) c + pmf (sds R10) d)
< pmf (sds R12) d +
(pmf (sds R12) b + pmf (sds R12) a) â
pmf (sds R10) a +
(pmf (sds R10) c + pmf (sds R10) d) =
pmf (sds R12) d +
(pmf (sds R12) b + pmf (sds R12) a)
(pmf (sds R34) b < pmf (sds R24) c â
pmf (sds R34) b + pmf (sds R34) d
< pmf (sds R24) c + pmf (sds R24) a) â
pmf (sds R34) b = pmf (sds R24) c â
pmf (sds R34) b + pmf (sds R34) d =
pmf (sds R24) c + pmf (sds R24) a
(pmf (sds R36) a < pmf (sds R25) a â
pmf (sds R36) a + pmf (sds R36) c
< pmf (sds R25) a + pmf (sds R25) c) â
pmf (sds R36) a = pmf (sds R25) a â
pmf (sds R36) a + pmf (sds R36) c =
pmf (sds R25) a + pmf (sds R25) c
(pmf (sds R42) d < pmf (sds R37) a â
pmf (sds R42) d + pmf (sds R42) b
< pmf (sds R37) a + pmf (sds R37) b) â
pmf (sds R42) d = pmf (sds R37) a â
pmf (sds R42) d + pmf (sds R42) b =
pmf (sds R37) a + pmf (sds R37) b
(pmf (sds R27) a < pmf (sds R13) a â
pmf (sds R27) a + pmf (sds R27) b
< pmf (sds R13) a + pmf (sds R13) b â
pmf (sds R27) a +
(pmf (sds R27) b + pmf (sds R27) d)
< pmf (sds R13) a +
(pmf (sds R13) b + pmf (sds R13) d)) â
pmf (sds R27) a = pmf (sds R13) a â
pmf (sds R27) a + pmf (sds R27) b =
pmf (sds R13) a + pmf (sds R13) b â
pmf (sds R27) a +
(pmf (sds R27) b + pmf (sds R27) d) =
pmf (sds R13) a +
(pmf (sds R13) b + pmf (sds R13) d)
pmf (sds R13) b + pmf (sds R13) a
< pmf (sds R27) b + pmf (sds R27) a â
pmf (sds R13) b + pmf (sds R13) a =
pmf (sds R27) b + pmf (sds R27) a
(pmf (sds R16) c < pmf (sds R14) d â
pmf (sds R16) c + pmf (sds R16) d
< pmf (sds R14) d + pmf (sds R14) c) â
pmf (sds R16) c = pmf (sds R14) d â
pmf (sds R16) c + pmf (sds R16) d =
pmf (sds R14) d + pmf (sds R14) c
pmf (sds R34) d +
(pmf (sds R34) b + pmf (sds R34) a)
< pmf (sds R14) c +
(pmf (sds R14) b + pmf (sds R14) a) â
pmf (sds R34) d +
(pmf (sds R34) b + pmf (sds R34) a) =
pmf (sds R14) c +
(pmf (sds R14) b + pmf (sds R14) a)
(pmf (sds R9) a < pmf (sds R14) a â
pmf (sds R9) a + pmf (sds R9) d
< pmf (sds R14) a + pmf (sds R14) d â
pmf (sds R9) a +
(pmf (sds R9) d + pmf (sds R9) c)
< pmf (sds R14) a +
(pmf (sds R14) d + pmf (sds R14) c)) â
pmf (sds R9) a = pmf (sds R14) a â
pmf (sds R9) a + pmf (sds R9) d =
pmf (sds R14) a + pmf (sds R14) d â
pmf (sds R9) a +
(pmf (sds R9) d + pmf (sds R9) c) =
pmf (sds R14) a +
(pmf (sds R14) d + pmf (sds R14) c)
(pmf (sds R31) c + pmf (sds R31) d
< pmf (sds R45) b + pmf (sds R45) a â
pmf (sds R31) c +
(pmf (sds R31) d + pmf (sds R31) b)
< pmf (sds R45) b +
(pmf (sds R45) a + pmf (sds R45) c)) â
pmf (sds R31) c + pmf (sds R31) d =
pmf (sds R45) b + pmf (sds R45) a â
pmf (sds R31) c +
(pmf (sds R31) d + pmf (sds R31) b) =
pmf (sds R45) b +
(pmf (sds R45) a + pmf (sds R45) c)
(pmf (sds R29) d + pmf (sds R29) c
< pmf (sds R39) d + pmf (sds R39) c â
pmf (sds R29) d +
(pmf (sds R29) c + pmf (sds R29) a)
< pmf (sds R39) d +
(pmf (sds R39) c + pmf (sds R39) a)) â
pmf (sds R29) d + pmf (sds R29) c =
pmf (sds R39) d + pmf (sds R39) c â
pmf (sds R29) d +
(pmf (sds R29) c + pmf (sds R29) a) =
pmf (sds R39) d +
(pmf (sds R39) c + pmf (sds R39) a)
(pmf (sds R37) a + pmf (sds R37) c
< pmf (sds R46) d + pmf (sds R46) b â
pmf (sds R37) a +
(pmf (sds R37) c + pmf (sds R37) d)
< pmf (sds R46) d +
(pmf (sds R46) b + pmf (sds R46) a)) â
pmf (sds R37) a + pmf (sds R37) c =
pmf (sds R46) d + pmf (sds R46) b â
pmf (sds R37) a +
(pmf (sds R37) c + pmf (sds R37) d) =
pmf (sds R46) d +
(pmf (sds R46) b + pmf (sds R46) a)
pmf (sds R20) c + pmf (sds R20) a
< pmf (sds R46) c + pmf (sds R46) a â
pmf (sds R20) c + pmf (sds R20) a =
pmf (sds R46) c + pmf (sds R46) a
(pmf (sds R26) a < pmf (sds R8) d â
pmf (sds R26) a +
(pmf (sds R26) c + pmf (sds R26) d)
< pmf (sds R8) d +
(pmf (sds R8) b + pmf (sds R8) a)) â
pmf (sds R26) a = pmf (sds R8) d â
pmf (sds R26) a +
(pmf (sds R26) c + pmf (sds R26) d) =
pmf (sds R8) d +
(pmf (sds R8) b + pmf (sds R8) a)
(pmf (sds R39) a < pmf (sds R28) a â
pmf (sds R39) a + pmf (sds R39) c
< pmf (sds R28) a + pmf (sds R28) b) â
pmf (sds R39) a = pmf (sds R28) a â
pmf (sds R39) a + pmf (sds R39) c =
pmf (sds R28) a + pmf (sds R28) b
pmf (sds R47) d + pmf (sds R47) a
< pmf (sds R4) d + pmf (sds R4) a â
pmf (sds R47) d + pmf (sds R47) a =
pmf (sds R4) d + pmf (sds R4) a
(pmf (sds R18) c < pmf (sds R4) c â
pmf (sds R18) c +
(pmf (sds R18) b + pmf (sds R18) a)
< pmf (sds R4) c +
(pmf (sds R4) b + pmf (sds R4) a)) â
pmf (sds R18) c = pmf (sds R4) c â
pmf (sds R18) c +
(pmf (sds R18) b + pmf (sds R18) a) =
pmf (sds R4) c +
(pmf (sds R4) b + pmf (sds R4) a)
(pmf (sds R8) c < pmf (sds R4) d â
pmf (sds R8) c + pmf (sds R8) d
< pmf (sds R4) d + pmf (sds R4) c) â
pmf (sds R8) c = pmf (sds R4) d â
pmf (sds R8) c + pmf (sds R8) d =
pmf (sds R4) d + pmf (sds R4) c

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