primes
Case set df65d778fc5c
demo-prime-01
Given
\(p \in \mathbb{Z},\quad p \text{ prime},\quad p > 2\)
Claim
\(\displaystyle \left(-1\right)^{p} = -1\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-prime-01 (category primes) (var p integer) (assume (prime p)) (assume (> p 2)) (ask (= (pow -1 p) -1)) (expect true))
demo-prime-02
Given
\(p \in \mathbb{Z},\quad p \text{ prime}\)
Claim
\(\displaystyle \left(-1\right)^{p} \overset{?}{=} -1\)
Expected
contingent true at \(p = 3\); false at \(p = 2\)
equal at some admissible points, different at others
witness (true): \(p = 3\)
witness (false): \(p = 2\)
2 is the only even prime, so the equation is neither always true nor always false.
(case demo-prime-02 (category primes) (note "2 is the only even prime, so the equation is neither always true nor always false.") (var p integer) (assume (prime p)) (ask (= (pow -1 p) -1)) (expect contingent) (witness true (p 3)) (witness false (p 2)))
Case set 03f5149718d0
demo-prime-01
Given
\(p \in \mathbb{Z},\quad p \text{ prime},\quad p > 2\)
Claim
\(\displaystyle \left(-1\right)^{p} = -1\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-prime-01 (category primes) (var p integer) (assume (prime p)) (assume (> p 2)) (ask (= (pow -1 p) -1)) (expect true))
demo-prime-02
Given
\(p \in \mathbb{Z},\quad p \text{ prime}\)
Claim
\(\displaystyle \left(-1\right)^{p} \overset{?}{=} -1\)
Expected
contingent true at \(p = 3\); false at \(p = 2\)
equal at some admissible points, different at others
witness (true): \(p = 3\)
witness (false): \(p = 2\)
2 is the only even prime, so the equation is neither always true nor always false.
(case demo-prime-02 (category primes) (note "2 is the only even prime, so the equation is neither always true nor always false.") (var p integer) (assume (prime p)) (ask (= (pow -1 p) -1)) (expect contingent) (witness true (p 3)) (witness false (p 2)))
Case set d7af4def9aaa
demo-prime-01
Given
\(p \in \mathbb{Z},\quad p \text{ prime},\quad p > 2\)
Claim
\(\displaystyle \left(-1\right)^{p} = -1\)
Expected
true equal at every admissible point
the two sides are equal at every admissible point
(case demo-prime-01 (category primes) (var p integer) (assume (prime p)) (assume (> p 2)) (ask (= (pow -1 p) -1)) (expect true))
demo-prime-02
Given
\(p \in \mathbb{Z},\quad p \text{ prime}\)
Claim
\(\displaystyle \left(-1\right)^{p} \overset{?}{=} -1\)
Expected
contingent true at \(p = 3\); false at \(p = 2\)
equal at some admissible points, different at others
witness (true): \(p = 3\)
witness (false): \(p = 2\)
2 is the only even prime, so the equation is neither always true nor always false.