← suite examples

radicals

Case set df65d778fc5c

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-eq-abs-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-abs-02 falsefalse ✓false ✓no verdictno verdictno verdictno verdictno verdictno verdict
demo-eq-sqrt-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-sqrt-02 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-sqrt-03 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓
demo-eq-sqrt-04 falsefalse ✓no verdictfalse ✓false ✓false ✓false ✓false ✓false ✓

demo-eq-abs-01

Given
\(x \in \mathbb{R},\quad x < 0\)
Claim
\(\displaystyle \left|x\right| = -x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-abs-01 (category radicals)
  (var x real)
  (assume (negative x))
  (ask (= (abs x) (- x)))
  (expect true))

demo-eq-abs-02

Given
\(x \in \mathbb{R},\quad x < 0\)
Claim
\(\displaystyle \left|x\right| \neq x\)
Expected
false unequal at every admissible point (e.g. at \(x = -1\))

the two sides differ at every admissible point

witness (false): \(x = -1\)

(case demo-eq-abs-02 (category radicals)
  (var x real)
  (assume (negative x))
  (ask (= (abs x) x))
  (expect false)
  (witness false (x -1)))

demo-eq-sqrt-01

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \sqrt{x^{2}} = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-sqrt-01 (category radicals)
  (var x real)
  (assume (positive x))
  (ask (= (sqrt (pow x 2)) x))
  (expect true))

demo-eq-sqrt-02

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sqrt{x^{2}} = \left|x\right|\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-sqrt-02 (category radicals)
  (var x real)
  (ask (= (sqrt (pow x 2)) (abs x)))
  (expect true))

demo-eq-sqrt-03

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sqrt{x^{2}} \overset{?}{=} x\)
Expected
contingent true at \(x = 1\); false at \(x = -1\)

equal at some admissible points, different at others

witness (true): \(x = 1\)

witness (false): \(x = -1\)

Without a sign assumption sqrt(x^2) = x holds only for x >= 0.

(case demo-eq-sqrt-03 (category radicals)
  (note "Without a sign assumption sqrt(x^2) = x holds only for x >= 0.")
  (var x real)
  (ask (= (sqrt (pow x 2)) x))
  (expect contingent)
  (witness true (x 1))
  (witness false (x -1)))

demo-eq-sqrt-04

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \sqrt{x^{2}} + 1 \neq x\)
Expected
false unequal at every admissible point (e.g. at \(x = 1\))

the two sides differ at every admissible point

witness (false): \(x = 1\)

sqrt(x^2) = x for x > 0, so the difference is the constant 1.

(case demo-eq-sqrt-04 (category radicals)
  (note "sqrt(x^2) = x for x > 0, so the difference is the constant 1.")
  (var x real)
  (assume (positive x))
  (ask (= (+ (sqrt (pow x 2)) 1) x))
  (expect false)
  (witness false (x 1)))

Case set 03f5149718d0

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-eq-abs-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-abs-02 falsefalse ✓false ✓no verdictno verdictno verdictno verdictno verdictno verdict
demo-eq-sqrt-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-sqrt-02 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-sqrt-03 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
demo-eq-sqrt-04 falsefalse ✓no verdictfalse ✓false ✓false ✓false ✓false ✓false ✓

demo-eq-abs-01

Given
\(x \in \mathbb{R},\quad x < 0\)
Claim
\(\displaystyle \left|x\right| = -x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-abs-01 (category radicals)
  (var x real)
  (assume (negative x))
  (ask (= (abs x) (- x)))
  (expect true))

demo-eq-abs-02

Given
\(x \in \mathbb{R},\quad x < 0\)
Claim
\(\displaystyle \left|x\right| \neq x\)
Expected
false unequal at every admissible point (e.g. at \(x = -1\))

the two sides differ at every admissible point

witness (false): \(x = -1\)

(case demo-eq-abs-02 (category radicals)
  (var x real)
  (assume (negative x))
  (ask (= (abs x) x))
  (expect false)
  (witness false (x -1)))

demo-eq-sqrt-01

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \sqrt{x^{2}} = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-sqrt-01 (category radicals)
  (var x real)
  (assume (positive x))
  (ask (= (sqrt (pow x 2)) x))
  (expect true))

demo-eq-sqrt-02

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sqrt{x^{2}} = \left|x\right|\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-sqrt-02 (category radicals)
  (var x real)
  (ask (= (sqrt (pow x 2)) (abs x)))
  (expect true))

demo-eq-sqrt-03

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sqrt{x^{2}} \overset{?}{=} x\)
Expected
contingent true at \(x = 1\); false at \(x = -1\)

equal at some admissible points, different at others

witness (true): \(x = 1\)

witness (false): \(x = -1\)

Without a sign assumption sqrt(x^2) = x holds only for x >= 0.

(case demo-eq-sqrt-03 (category radicals)
  (note "Without a sign assumption sqrt(x^2) = x holds only for x >= 0.")
  (var x real)
  (ask (= (sqrt (pow x 2)) x))
  (expect contingent)
  (witness true (x 1))
  (witness false (x -1)))

demo-eq-sqrt-04

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \sqrt{x^{2}} + 1 \neq x\)
Expected
false unequal at every admissible point (e.g. at \(x = 1\))

the two sides differ at every admissible point

witness (false): \(x = 1\)

sqrt(x^2) = x for x > 0, so the difference is the constant 1.

(case demo-eq-sqrt-04 (category radicals)
  (note "sqrt(x^2) = x for x > 0, so the difference is the constant 1.")
  (var x real)
  (assume (positive x))
  (ask (= (+ (sqrt (pow x 2)) 1) x))
  (expect false)
  (witness false (x 1)))

Case set d7af4def9aaa

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-eq-abs-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-abs-02 falsefalse ✓false ✓no verdictno verdictno verdictno verdictno verdictno verdict
demo-eq-sqrt-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-sqrt-02 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
demo-eq-sqrt-03 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
demo-eq-sqrt-04 falsefalse ✓no verdictfalse ✓false ✓false ✓false ✓false ✓false ✓

demo-eq-abs-01

Given
\(x \in \mathbb{R},\quad x < 0\)
Claim
\(\displaystyle \left|x\right| = -x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-abs-01 (category radicals)
  (var x real)
  (assume (negative x))
  (ask (= (abs x) (- x)))
  (expect true))

demo-eq-abs-02

Given
\(x \in \mathbb{R},\quad x < 0\)
Claim
\(\displaystyle \left|x\right| \neq x\)
Expected
false unequal at every admissible point (e.g. at \(x = -1\))

the two sides differ at every admissible point

witness (false): \(x = -1\)

(case demo-eq-abs-02 (category radicals)
  (var x real)
  (assume (negative x))
  (ask (= (abs x) x))
  (expect false)
  (witness false (x -1)))

demo-eq-sqrt-01

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \sqrt{x^{2}} = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-sqrt-01 (category radicals)
  (var x real)
  (assume (positive x))
  (ask (= (sqrt (pow x 2)) x))
  (expect true))

demo-eq-sqrt-02

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sqrt{x^{2}} = \left|x\right|\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-eq-sqrt-02 (category radicals)
  (var x real)
  (ask (= (sqrt (pow x 2)) (abs x)))
  (expect true))

demo-eq-sqrt-03

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sqrt{x^{2}} \overset{?}{=} x\)
Expected
contingent true at \(x = 1\); false at \(x = -1\)

equal at some admissible points, different at others

witness (true): \(x = 1\)

witness (false): \(x = -1\)

Without a sign assumption sqrt(x^2) = x holds only for x >= 0.

(case demo-eq-sqrt-03 (category radicals)
  (note "Without a sign assumption sqrt(x^2) = x holds only for x >= 0.")
  (var x real)
  (ask (= (sqrt (pow x 2)) x))
  (expect contingent)
  (witness true (x 1))
  (witness false (x -1)))

demo-eq-sqrt-04

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \sqrt{x^{2}} + 1 \neq x\)
Expected
false unequal at every admissible point (e.g. at \(x = 1\))

the two sides differ at every admissible point

witness (false): \(x = 1\)

sqrt(x^2) = x for x > 0, so the difference is the constant 1.

(case demo-eq-sqrt-04 (category radicals)
  (note "sqrt(x^2) = x for x > 0, so the difference is the constant 1.")
  (var x real)
  (assume (positive x))
  (ask (= (+ (sqrt (pow x 2)) 1) x))
  (expect false)
  (witness false (x 1)))