(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 
              solve-quadratic-equation-or-inequality)
            (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 
              solve-quadratic-equation-or-inequality)
            simplify)
        (block 
            (script-comment "`force-substitution' at (1)") 
            (weaken (1 0)) 
            simplify)
        )))