Proof step e-706a96c1242f8bb9
definition_equality → concludes about shift_x_plus_one of Triangle read by rows: T(n,k) is the number of binary words of length n having degree of asymmetry equal to k (n >= 0; 0 <= k <= n/2). JSON
Theorem
Ore-algebra identity of two definitions polytool ?
Operation
All-n equality of two definitions
{
"operation": "definition_equality"
}
Premises
None: this step is a direct theorem check.
Claims
Verification and certificate
- polytool: replayed (the certificate replayed when the step was written)
- Lean: not attempted
- certificate:
definition_equality, SHA-25600fe99fd95d38dfca83405203eb80715042ac3738bbef305426d30e50b944d36, 26,520 bytes (4,564 compressed); download JSON