```
(def-constant dudek
"lambda(x:rr,
if(x < 0, x+1,
x >= 0 and x <= 4, (x-2)*(x-3) - 3,
x > 4, -1,
?rr))"
(theory h-o-real-arithmetic))
```

```
(def-theorem thm1
"forall(x:rr, x > 5 implies dudek(x) < 0)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally dudek)
simplify
)))
```

```
(def-theorem thm2a
"forsome(x:rr, dudek(x) > 1)"
(theory h-o-real-arithmetic)
(proof
(
(instantiate-existential ("[1/3]"))
(unfold-single-defined-constant-globally dudek)
simplify
)))
```

```
(def-theorem thm2b
"forall(x:rr, dudek(x) <=3)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally dudek)
(raise-conditional (0))
(raise-conditional (0))
simplify
direct-and-antecedent-inference-strategy
(force-substitution "x^2<=5*x" "x^2+(-5)*x+0<=0" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises
(cut-with-single-formula "nth%root(2,25)=5")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises
iota-free-characterization-of-nth%root)
simplify))
(block
(script-comment "`force-substitution' at (1)")
(weaken (1 0))
simplify)
)))
```

```
(def-theorem thm3
"forall(x:rr, x > 1 implies dudek(x) >= -(3+[25/100]))"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally dudek)
(raise-conditional (0))
(raise-conditional (0))
simplify
direct-and-antecedent-inference-strategy
(force-substitution
"5*x<=[25/4]+x^2"
"0<=x^2 +(-5)*x + [25/4]" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises