title: Generate Newton fractals

text:
# Question
Title: Generate Newton fractals
You all know the Newton method to approximate the roots of a function, don't you? My goal in this task is to introduce you into an interesting aspect of this algorithm.

Newton's algorithm converges only for certain, but most of all complex input values. If you picture the convergence of the method for all input values over the complex plane, you usually get a beautiful fractal like this:

*Image from Wikimedia commons*

## Specifications

The goal of this task is, to generate such fractals. This means, that you get a polynomial as the input and have to print out the corresponding fractal as an image in a format of your choice as the output.

### Input

The input is a whitespace-separated list of complex numbers. They are written down in the style `<Real part><iImaginary part>`, like this number: `5.32i3.05`. You may assume, that the input number has no more than 4 decimal places and is smaller than 1000. The first of them must not be zero. For example, this could be an input to your program:

```
1 -2i7.5 23.0004i-3.8 i12 0 5.1233i0.1
```

The numbers are interpreted as the coefficients of a polynomial, beginning with the highest power. Throughout the rest of this specification, the input polynomial is called **P**. The above input is equal to this polynomial:

```
f(x) = x<sup>5</sup> + (-2 + 7.5*i*)x<sup>4</sup> + (23.0004 - 3.8*i*)x<sup>3</sup> + 12*i*x<sup>2</sup> + 5.1233 + 0.1*i*
```

The input may come to you either from stdin, from an argument passed to the program or from a prompt displayed to your program. You may assume, that the input does not contain any leading or trailing whitespace characters.

### Rendering

You have to render the fractal in the following way:

* Choose as many colors as roots of **P** plus an extra color for divergence
* For each number in the visible plane, determine whether the method converges and if yes to which root. Color the point according to the result.
* Do not print rulers or other fancy things
* Print a black point at the points, that are the polynomials roots for orientation. You may print up to four pixels around each root.
* Find a way to choose the visible plane in a way, that all roots are distinguishable and spread widely across it, if possible. Although a perfect placement of the output frame is not required, I reserve the right to refuse to accept an answer that chooses the frame in an unacceptable way, eg. always at the same coordinates, all roots are in one point, etc.
* The output image should have a size of 1024\*1024 pixels.
* Rendering time is 10 minutes maximum
* Using single precision floating-point values is enough

### Output

The output should be a raster graphics image in a file format of your choice, readable by standard software for a brand X operating system. If you want to use a rare format, consider adding a link to a website where one can download a viewer for it.

Output the file to stdout. If your language does not support putting something to stdout or if you find this option less convenient, find another way. In any way, it must be possible to save the generated image.

### Restrictions

* No image processing libraries
* No fractal generating libraries
* The shortest code wins

### Extensions

If you like this task, you could try to color the points according to the speed of convergence or some other criteria. I'd like to see some interesting results.

# Answer
## Python, 827 777 chars

```
import re,random
N=1024
M=N*N
R=range
P=map(lambda x:eval(re.sub('i','+',x)+'j'if 'i'in x else x),raw_input().split())[::-1]
Q=[i*P[i]for i in R(len(P))][1:]
E=lambda p,x:sum(x**k*p[k]for k in R(len(p)))
def Z(x):
 for j in R(99):
  f=E(P,x);g=E(Q,x)
  if abs(f)<1e-9:return x,1
  if abs(x)>1e5or g==0:break
  x-=f/g
 return x,0
T=[]
a=9e9
b=-a
for i in R(999):
 x,f=Z((random.randrange(-9999,9999)+1j*random.randrange(-9999,9999))/99)
 if f:a=min(a,x.real,x.imag);b=max(b,x.real,x.imag);T+=[x]
s=b-a
a,b=a-s/2,b+s/2
s=b-a
C=[[255]*3]*M
H=lambda x,k:int(x.real*k)+87*int(x.imag*k)&255
for i in R(M):
 x,f=Z(a+i%N*s/N+(a+i/N*s/N)*1j)
 if f:C[i]=H(x,99),H(x,57),H(x,76)
for r in T:C[N*int(N*(r.imag-a)/s)+int(N*(r.real-a)/s)]=0,0,0
print'P3',N,N,255
for c in C:print'%d %d %d'%c

```

Finds display bounds (and roots) by finding convergence points for a bunch of random samples. It then draws the graph by computing the convergence points for each starting point and using a hash function to get randomish colors for each convergence point. Look very closely and you can see the roots marked.

Here's the result for the example polynomial.
> 14 votes

# Answer
## Java, 1093 1058 1099 1077 chars

```
public class F{double r,i,a,b;F(double R,double I){r=R;i=I;}F a(F c){return
new F(r+c.r,i+c.i);}F m(F c){return new F(r*c.r-i*c.i,r*c.i+i*c.r);}F
r(){a=r*r+i*i;return new F(-r/a,i/a);}double l(F c){a=r-c.r;b=i-c.i;return
Math.sqrt(a*a+b*b);}public static void main(String[]a){int
n=a.length,i=0,j,x,K=1024,r[]=new int[n];String o="P3\n"+K+" "+K+"\n255 ",s[];F z=new
F(0,0),P[]=new F[n],R[]=new F[n],c,d,e,p,q;for(;i<n;)P[i]=new
F((s=a[i++].split("i"))[0].isEmpty()?0:Float.parseFloat(s[0]),s.length==1?0:Float.parseFloat(s[1]));double
B=Math.pow(P[n-1].m(P[0].r()).l(z)/2,1./n),b,S;for(i=1;i<n;){b=Math.pow(P[i].m(P[i-1].r()).l(z),1./i++);B=b>B?b:B;}S=6*B/K;for(x=0;x<K*K;){e=d=c=new
F(x%K*S-3*B,x++/K*S-3*B);for(j=51;j-->1;){p=P[0];q=p.m(new
F(n-1,0));for(i=1;i<n;){if(i<n-1)q=q.m(c).a(P[i].m(new
F(n-1-i,0)));p=p.m(c).a(P[i++]);}c=c.a(d=q.r().m(p));if(d.l(z)<S/2)break;}i=j>0?0:n;for(;i<n;i++){if(R[i]==null)R[i]=c;if(R[i].l(c)<S)break;}i=java.awt.Color.HSBtoRGB(i*1f/n,j<1||e.l(c)<S&&r[i]++<1?0:1,j*.02f);for(j=0;j++<3;){o+=(i&255)+" ";i>>=8;}System.out.println(o);o="";}}}

```

Input is command-line arguments - e.g. run `java F 1 0 0 -1`. Output is to stdout in PPM format (ASCII pixmap).

The scale is chosen using the Fujiwara bound on the absolute value of the complex roots of a polynomial; I then multiply that bound by 1.5. I do adjust brightness by convergence rate, so the roots will be in the brightest patches. Therefore it's logical to use white rather than black to mark the approximate locations of the roots (which is costing me 41 chars for something which can't even be done "correctly". If I label all points which converge to within 0.5 pixels of themselves then some roots come out unlabelled; if I label all points which converge to within 0.6 pixels of themselves then some roots come out labelled over more than one pixel; so for each root I label the first point encountered to converge to within 1 pixel of itself).

Image for the example polynomial (converted to png with the GIMP):
> 14 votes

# Answer
# Python, 339 char/bytes

```
import numpy as n;import matplotlib.pyplot as p;from colorsys import hls_to_rgb as h
a,d=1,2001j;x,y=n.ogrid[-a:a:d,-a:a:d];z=x+1j*y
for i in range(3): z-=(z**3-1)/3/z**2
z[n.isnan(z)]=0
z=n.array(n.vectorize(h)((n.angle(z)+n.pi)/3/n.pi,1.-1/(1.+n.abs(z)**.1),.8)).swapaxes(0,2)
p.figure();p.imshow(z,interpolation='nearest');p.axis('off')

```

### The plot below is for Newton Fractal of z^3 - 1 function.

Edit: Thanks to @Khuldraeseth na'Barya now the code is even shorter. Removed the irrelevant code and image.
> 4 votes

---
Tags: code-golf, graphical-output, fractal, complex-numbers
---


# Question
Title: Duplicate the KOOS Jr. Scoring interval algorithm
Inspired from a real problem; we were looking at this table and said "Hey, now that's a good codegolf problem."

The KOOS Jr. scores converts from a raw number to a percentile score given this table:

```
Raw summed score  Interval score
(0-28)            (0 to 100 scale)
 0                100.000
 1                 91.975
 2                 84.600
 3                 79.914
 4                 76.332
 5                 73.342
 6                 70.704
 7                 68.284
 8                 65.994
 9                 63.776
10                 61.583
11                 59.381
12                 57.140
13                 54.840
14                 52.465
15                 50.012
16                 47.487
17                 44.905
18                 42.281
19                 39.625
20                 36.931
21                 34.174
22                 31.307
23                 28.251
24                 24.875
25                 20.941
26                 15.939
27                  8.291
28                  0.000

```

Provide a program, function, expression, or source file generator\* that given the input raw number returns the interval score number. You may accept your input as a string or number and may produce your output as a string or number. Trailing zeros after the decimal point may be included or omitted. You may not however use scaled integers: 1 must really return 91.975 not 91975.

\*source file generator must output a valid source file for some language you specify; just outputting the table is not allowed.

# Answer
> 3 votes
# 05AB1E, 59 bytes

```
•G‚Œιã¶&‡Vc–QΩ`ååI~(Ìö{3.ùSÿ{Ćι¯TærÆcï`₃āÀ}ªHÕ¶η•4ô.¥R3°/Iè

```

Try it online!

**Explanation**

`•G‚Œιã¶&‡Vc–QΩ`ååI~(Ìö{3.ùSÿ{Ćι¯TærÆcï`₃āÀ}ªHÕ¶η•` is a compressed version of the input constructed by:

* multiplying each element in the input by 1000
* reversing the resulting list
* calculating deltas
* joining to a single base-10 number
* compressing to base-255

The rest of the code is then:

```
4ô          # split in pieces of 4
  .¥        # undelta
    R       # reverse
     3°/    # divide each by 1000
        Iè  # index into list with input

```

# Answer
> 1 votes
# Python 2, ~~166~~ ~~160~~ 139 bytes

```
lambda n:sum(int('6533222222211111111111222356EWU1LC74210ZYWTRQPOPRV1BRMO6BGYASWNLUSWQ55ZW96XMM8A2I6VX'[i::28],36)for i in range(28-n))/1e3

```

Try it online!

Edit: golf 6 bytes from glaring redundancy of `2`'s...; also saved 21 bytes by switch to base 36 (thanks ovs!) and using `1e3` instead of `1000.`

The string is an encoded list of the 28 4-digit deltas.

# Answer
> 1 votes
# PHP, 152 bytes

```
<?=intval(substr("255s1yyv1ta01pnu1mwc1kla1ik01gos1ex61d7k1bin19th183816bc14hd12l810n30ynd0wmh0ukp0shv0qda0o5n0lsr0j6z0g5p0car06eb0",$argn*4,4),36)/1e3;

```

Try it online!

# Answer
> 1 votes
## Python 3, 133 bytes

```
lambda k:sum(int('5ukygji75mxo64d3f5vstve68rdiq42l8nof8cs35qyb5bdtzihbhk086m8nel1nx3kqxvn',36)//8292**i%8292for i in range(28-k))/1e3

```

It uses packed differences, and sums them. To pack efficiently, rather than using binary, it's packed in a number that's effectively base 8292, and that number is embedded in the code as a base 36 literal.

# Answer
> 1 votes
# Stax, 59 bytes

```
â¬∟╧↓┘╟╤éJ{súÇaz░«╝╬°╢=♦Γ┘=▐▬[è2Ü←`‼frl¢£≤kpOy‼5¶^≡%#ßî↕V0Å

```

Run and debug it

# Answer
> 0 votes
# Mathematica, 196 bytes

```
(100-Accumulate[{0}~Join~IntegerDigits@9753332322223223323323344578])[[#+1]].{0,975,6,914,332,342,704,284,994,776,583,381,14,84,465,"012",487,905,281,625,931,174,307,251,875,941,939,291,0}[[#+1]]&

```

# Answer
> 0 votes
# Python 3, ~~147~~ 146 bytes

*-1 byte thanks to @JörgHülsermann*

```
lambda k:sum((int('9CU7OK2L6V5W6E8QYM3YL0TRGZIJ6Y14N43TRVCAXF6C58HP69ZC4536JNILBUC45C5S8G4DIT0J',36)&2**(14*-~i)-1)>>i*14for i in range(28-k))/1e3

```

Try it online!

---
Tags: code-golf, kolmogorov-complexity
---


title: Integers in Base Pi

text:
# Question
Title: Integers in Base Pi
### Background:

Pi (`π`) is a transcendental number, and therefore it has a non-terminating decimal representation. Similar, the representation doesn't terminate if written in any other integer base. But what if we wrote it in base `π`?

Digits in decimal represent powers of 10, so:

```
π = 3.14… = (3 * 10^0) + (1 * 10^-1) + (4 * 10^-2) + …

```

So in base `π`, the digits would represent powers of `π`:

```
π = 10 = (1 * π^1) + (0 * π^0)

```

In this new base, integers now have non-terminating representations. So 10 in decimal now becomes the following:

```
10 => 100.01022… = (1 * π^2) + (0 * π^1) + (0 * π^0) + (0 * π^-1) + (1 * π^-2) + …

```

Note that in base `π` the digits used are 0,1,2,3 because these are the digits less than `π`.

### Challenge:

Given a non-negative integer `x`, either:

1. Output (without halting) its representation in base `π`. If the number has a finite representation (0, 1, 2, 3), then the program may halt instead of printing infinite zeros.
2. Take an arbitrarily large integer `n`, and output the first `n` digits of `x` in base `π`.

### Rules:

* Since a number has multiple possible representations, **you must output the one that appears the largest** (normalized). Just as `1.0 = 0.9999…` in decimal, this problem exists in this base, too. In base `π`, one is still `1.0`, but could also be written as `0.3011…`, for example. Similarly, ten is `100.01022…`, but could also be written as `30.121…` or `23.202…`.
* This is code-golf, so fewest bytes wins. Program or function.
* No built-ins (I'm looking at *you*, Mathematica)

### Results:

```
0       = 0
1       = 1
2       = 2
3       = 3
4       = 10.220122021121110301000010110010010230011111021101…
5       = 11.220122021121110301000010110010010230011111021101…
6       = 12.220122021121110301000010110010010230011111021101…
7       = 20.202112002100000030020121222100030110023011000212…
8       = 21.202112002100000030020121222100030110023011000212…
9       = 22.202112002100000030020121222100030110023011000212…
10      = 100.01022122221121122001111210201201022120211001112…
42      = 1101.0102020121020101001210220211111200202102010100…
1337    = 1102021.0222210102022212121030030010230102200221212…
9999    = 100120030.02001010222211020202010210021200221221010…

```

First 10,000 digits of ten in base Pi

### Verification:

You can verify any output you want using the Mathematica code here. The first parameter is `x`, the third is `n`. If it times out, pick a small `n` and run it. Then click "Open in Code" to open a new Mathematica worksheet with the program. There's no time limit there.

Convert the resulting output to a number here.

**Related:**

# Answer
> 1 votes
# Julia 0.6, 81 bytes

```
f(x,i=log(π,x)÷1)=(y=big(π)^i;d::Int=x÷y;print(i==0?"$d.":"$d");f(x-d*y,i-1))

```

Prints out digits (and the . which cost me 14 bytes) until it Stack overflows at about 22k digits on TIO. If I'm allowed to pass the input as a `BigFloat` I can cut 5 bytes. Makes use of the built in arbitrary precision constant `π`. But its a bit cooler than that, its actually an adaptive precision constant, `π*1.0` is a 64 bit floating point number, `π*big(1.0)` (aka multiplied by an higher precision number) gives `π` at whatever your precision is set to.

Try it online!

# Answer
> 3 votes
# Python 3, ~~471~~ ~~317~~ 310 bytes

7 bytes thanks to caird coinheringaahing.

Surely there are golfs that I missed. Feel free to point them out in the comments.

```
def h(Q):
	a=0;C=b=4;c=d=s=1;P=o=3
	while P^C:
		a,b,c,d,s,o,P,A,B=b,s*a+o*b,d,s*c+o*d,s+o,o+2,C,0,1
		for I in Q:B*=c;A=A*a+I*B
		C=A>0
	return P
def f(n,p):
	Q=[-n];R=""
	while h([1]+Q)<1:Q=[0]+Q
	Q+=[0]*p
	for I in range(len(Q)):
		i=3;Q[I]+=3
		while h(Q):Q[I]-=1;i-=1
		R+=str(i)
	return R[:-p]+"."+R[-p:]

```

Try it online!

### Ungolfed version:

```
def poly_eval_pi_pos(poly,a=0,b=4,c=1,d=1,o=3,s=1,prev=9,curr=6):
	while prev != curr:
		a,b,c,d,s,o=b,s*a+o*b,d,s*c+o*d,s+o,o+2
		prev = curr
		res_n, res_d = 0,1
		for I in poly:
			res_d *= c
			res_n = res_n*a + I * res_d
		curr = res_n > 0
	return prev
def to_base_pi(n,precision):
	poly = [-n]
	res = ""
	while not poly_eval_pi_pos([1]+poly):
		poly = [0]+poly
	poly += [0]*precision
	for index in range(len(poly)):
		i = 3
		poly[index] += 3
		while poly_eval_pi_pos(poly):
			poly[index] -= 1
			i -= 1
		res += str(i)
	return res[:-precision]+"."+res[-precision:]

```

Try it online!

# Answer
> 3 votes
# Ruby `-rbigdecimal/math`, ~~111~~ ~~103~~ 97 bytes

```
->x,n{q=BigMath::PI n;r=q**m=Math.log(x,q).to_i;n.times{$><<"#{?.if-2==m-=1}%i"%d=x/r;x%=r;r/=q}}

```

Try it online!

Takes input number as `x` and desired precision as `n`. Outputs by printing. Makes use of the built-in BigDecimal library for arbitrary pecision PI value.

# Answer
> 1 votes
# Python 3 \+ sympy, 144 bytes

```
from sympy import*
def f(n,p):
	R="";O=n and int(log(n,pi));r=pi**O
	for _ in range(O+p):R+=str(int(n/r));n%=r;r/=pi
	return R[:O+1]+"."+R[O+1:]

```

Try it online!

Quite slow, actually.

---
Tags: code-golf, base-conversion, pi
---


title: Predecessor-completed Ascii Cubes

text:
# Question
Title: Predecessor-completed Ascii Cubes
The first *Predecessor-completed Ascii Cube (PAC 1)* is a simple cube with side length 1 and looks like this:

```
 /////\
/////  \
\\\\\  /
 \\\\\/

```

The *PAC 2* is a geometric shape such that combining it with its predecessor (the *PAC 1*) completes a side length 2 cube:

```
      front                back
   /////////\           /////////\
  /////////  \         /////////  \
 /////\\\\\   \       /////////    \
/////  \\\\\   \     /////////      \
\\\\\  /////   /     \\\\\\\\\      /
 \\\\\/////   /       \\\\\\\\\    /
  \\\\\\\\\  /         \\\\\\\\\  /
   \\\\\\\\\/           \\\\\\\\\/

```

Because the *back*-view is kind of boring, we are only interested in the *front*-view.

The same goes for the *PAC 3*: With some visual thinking the *PAC 2* can be turned around and plugged into the *PAC 3* to form a solid side length 3 cube:

```
     /////////////\
    /////////////  \
   /////\\\\\\\\\   \
  /////  \\\\\\\\\   \
 /////   /////\\\\\   \
/////   /////  \\\\\   \
\\\\\   \\\\\  /////   /
 \\\\\   \\\\\/////   /
  \\\\\  /////////   /
   \\\\\/////////   /
    \\\\\\\\\\\\\  /
     \\\\\\\\\\\\\/

```

And so on with *PAC 4*:

```
       /////////////////\
      /////////////////  \
     /////\\\\\\\\\\\\\   \
    /////  \\\\\\\\\\\\\   \
   /////   /////////\\\\\   \
  /////   /////////  \\\\\   \
 /////   /////\\\\\   \\\\\   \
/////   /////  \\\\\   \\\\\   \
\\\\\   \\\\\  /////   /////   /
 \\\\\   \\\\\/////   /////   /
  \\\\\   \\\\\\\\\  /////   /
   \\\\\   \\\\\\\\\/////   /
    \\\\\  /////////////   /
     \\\\\/////////////   /
      \\\\\\\\\\\\\\\\\  /
       \\\\\\\\\\\\\\\\\/

```

### Task:

Write a full program or function which takes a positive integer n as input and returns or prints the corresponding front-view of *PAC n* exactly as shown above. Additional trailing white space is acceptable.

This is , so try to use as few bytes as possible in the language of your choice.

# Answer
> 11 votes
## JavaScript (ES6), 229 bytes

```
f=
(n,l=n*4+1,r=1,i=n*2,g=a=>` / \\ /
`.replace(/./g,c=>c.repeat(a.pop())))=>n?g([r,,l,--i])+g([r,2,l,--i])+f(n-1,l-1?1:r-4,r-1?1:l-4).replace(/(\S).*(.)/g,r-1?`$1   $&$2$2$2$2`:`$1$1$1$1$&   $2`)+g([r,2,l,,,i])+g([r,,l,,,i+1]):``
```

```
<input type=number min=0 oninput=o.textContent=f(+this.value)><pre id=o>
```

# Answer
> 4 votes
## Batch, ~~559~~ ~~432~~ 400 bytes

```
@echo off
set m=
for /l %%i in (1,1,%1)do call set m=  %%m%%
call:c "%m:~2%" %m: =//%/\
exit/b
:c
setlocal
set m=%~1%2%~3
echo  %m%
echo %m:/\=/  \%
set s=%~1
if "%s:~,1%"=="/" goto g
set t=%2
set t=%t:~3,-3%
if %t:~,1%==/ (call:c "%s:~2%////" /\%t:/=\% "   \%~3")else call:c "%s:~2%/   " %t:\=/%/\ "\\\\%~3"
:g
set m=%m:/=-%
set m=%m:\=/%
set m=%m:-=\%
echo %m:\/=\  /%
echo  %m%

```

Explanation: The bottom half of the cube is drawn by reflecting the top half. The halves are further split into ~~seven~~ ~~six~~ three ~~strips~~ parts, as per this diagram showing the top half:

```
1       12/////////////////\233
1      12/////////////////  \233
1     ////12/\\\\\\\\\\\\\23   \3
1    ////12/  \\\\\\\\\\\\\23   \3
1   /////   12/////////\23\\\\   \3
1  /////   12/////////  \23\\\\   \3
1 /////   ////12/\\\\\23   \\\\\   \3
1/////   ////12/  \\\\\23   \\\\\   \3

```
1. The indentation (which decreases every row) and the left triangle, which increases every other row
2. The middle shrinking zigzag triangle, with the small triangle on alternate sides every other row
3. The right triangle, which increases in sync with the left

Edit: Saved over 20% by improving the code that reflected the top to the bottom half. Saved almost 10% by merging the left two and middle three strips.

# Answer
> 4 votes
# Canvas, 36 bytes

```
；Ｘø；｛１ｘ／╋
ø╶｛«５⁸２²４×⁸²«１╋²«＼＋；↔５３╋｝═

```

Try it here!

# Answer
> 4 votes
# SOGL V0.12, 32 bytes

```
ø.∫4*I└*2∙f«5└*∙+¼F«╝┼;↔±53╬5}╬±

```

Try it here!

Simple explanation:
1. iterate for each of 1..x
2. make a  shape with the width of `i*4+1` and height = `(0-indexed)i // 2`
3. pad it so it looks like
4. append a "\\" shape to that horizontally
5. insert the previous step inside that reversed 6. after everything, mirror vertically

full program:

```
ø                                 push an empty string - starting stage
 .∫                          }    iterate over 1..input
   4*                               multiply the 1-indexed counter by 4
     I                              and add 1
      └*                            repeat "/" that many times
        2∙                          and repeat vertically twice. Top 2 lines are done
          f«                        push the 0-indexed counter floor divided by 2
            5└*                     push "/" repeated 5 times
               ∙                    and repeat that vertically by the result of the "f«"
                +                   add vertically, creating a "⌐" shape
                 ¼                  prepend each next line with one less space than the above
                  F«                push 1-indexed counter floor divided by 2
                    ╝               create a "\" diagonal that long
                     ┼              and append it horizontally. Shell is done of this hexagon
                      ;↔±           get the previous item on the stack and reverse it horizontally
                         53╬5       and at [5;3] insert the previous result in this
                              ╬±  once everything's done, mirror vertically to finish the hexagon

```

# Answer
> 2 votes
# Python 2, ~~254~~ ~~234~~ ~~226~~ ~~203~~ ~~201~~ 199 bytes

Finally sub 200!

```
P=[];n=0
M=lambda r:(u''+r).translate({47:92,92:47})
exec r"n+=1;q='/'*4;P=[q*n+'/\\',q*n+'/  \\']+[q+'%s   \\'%M(r[::-1])for r in P];"*input()
print'\n'.join(l.center(8*n)for l in(P+map(M,P[::-1])))

```

**Tricks:**

This function is used to swap all `\` with `/` and vice versa
A bit long in Python2 - works only with unicode
Check out this for how it works

```
M=lambda r:(u''+r).translate({47:92,92:47})

```

---

Generates new top two rows for each iteration
For now I can't find compact way to receive this lines from previous iteration

```
P=[q*n+'/\\',q*n+'/  \\']

```

---

Reverse all rows of previous iteration and swap slashes

```
[q+'%s   \\'%M(r[::-1])for r in P]

```

---

Copy top half, reversed by rows, swap slashes

```
P+map(M,P[::-1])

```

---

Neat method for center padding strings

```
l.center(8*n)

```

Try it online!

# Answer
> 2 votes
# Haskell, ~~232~~ ~~227~~ ~~224~~ ~~187~~ ~~183~~ ~~180~~ 175 bytes

```
m '/'='\\'
m '\\'='/'
m c=c
r=reverse
k=map
n?s=('/'<$[1..4*n])++s
f 0=[]
f n=n?"/\\":n?"/  \\":[1?k m(r s)++"   \\"|s<-f$n-1]
s="":k(' ':)s
((++).r<*>k(k m)).zipWith(++)s.r.f

```

The anonymous function in the last line takes an integer argument and yields the lines to be printed for a cube of that size.

The idea is to use recursion to draw larger cubes from smaller ones. Lets look at the upper half of a cube of size 1. Then we get the upper half of a cube of size 2 by mirroring the former half and add a fixed pattern of slashes and spaces around it:

```
                                         /////////\
                                        /////////  \
     /////\    ==>    /\\\\\    ==>    ////**/\\\\\**   \
    /////  \         /  \\\\\         ////**/  \\\\\**   \

```

So the algorithm to draw a cube of size *n* is

1. Get the lines for the upper cube half of size *n-1*.
2. Mirror each line (by flipping `/`s and `\`s), and pad `////` and  `\` around.
3. Prepend two lines with the pattern `////`<sup>*n*</sup> plus `/\` and `/ \`.
4. Mirror the resulting lines to get the full cube.
5. Pad lines with appropriate number of spaces.

# Answer
> 2 votes
# Ruby,  ~~174 167 169~~  167 bytes

```
->n{a=(1..m=n*4).map{' '*m}
(-n..0).map{|i|(-2*i).times{|k|a[y=k+2*j=n+i][m+~k+i*2,2+k*2-s=4*i]=?/*(1-~j%2*s)+'  '*k+?\\*(1-j%2*s)
a[~y]=a[y].tr('/\\','\\\\/')}}
a*$/}

```

Try it online!

creates an array of `n*4` strings filled with spaces, then overwrites it with successively smaller cubes.

**Commented code**

```
->n{a=(1..m=n*4).map{' '*m}                 #make an array of n*4 strings of n*4 spaces (up to centreline of final output)
  (-n..0).map{|i|                           #iterate through cube sizes from n down to 0 (i is negative -n to 0)
    (-2*i).times{|k|                        #iterate through the number of lines in the top half of the cube
      a[y=k+2*j=n+i][m+~k+i*2,2+k*2-s=4*i]= #overwrite the correct part of the correct line
      ?/*(1-~j%2*s)+'  '*k+?\\*(1-j%2*s)    #with the correct string of the form "/spaces\" with an additional -4*i symbols on one side
      a[~y]=a[y].tr('/\\','\\\\/')          #copy the current line from top half into bottom half, subsituting / for \ and vice versa
    }
  }
a*$/}                                       #return the elements of the array a, concatenated with newlines $/

```

# Answer
> 2 votes
# Stax, 36 bytes

```
äª.$u>↓Z╙╝B↨EXª¡╜?Xáhç∙╩p/♂ù⌠r↨c⌐f/*

```

Run and debug it

This approach builds up the top half of the output iteratively. It executes the main block the specified number of times. In that block, each row is mirrored and has a prefix and suffix added. The top two new rows are added separately. When all the rows are built, they're centered, and then the bottom is mirrored vertically.

Here's the program unpacked, ungolfed, and commented.

```
{               begin block to repeat
  iHYH^H'\*     make a string of '\' characters and set the Y register
                  pseudo-code: push(((y = (i * 2)) * 2 + 1) * 2 * '\')
                  given the 0-based iteration index `i`, let y = 2 * i
                  and push a string consisting of (i*8 + 2) backslashes
  2M            split the string into to equal size (i*4 + 1) substrings
  ~+            push array to input stack and concatenate
                  on the first iteration, this is a no-op
                  subsequently, it prepends the array to the result so far
  {             begin a block to use for mapping
    4'\*+       append 4 backslashes to this element
    :R          "brace-wise" reverse
                  this reverses the string AND the slashes in it
    |YH3+92&    write 92 to index (++y * 2 + 3) in the array
                  this puts the trailing backslash at the correct position
                  this will be an out of bounds index, so the string will grow
                  92 is the character code for backslash
  m             execute map using block
}*              repeat block specified number of times
|C              vertically center all rows
{               begin block for output mapping
  Q             output this line without popping
  :Rr           "brace-wise" reverse, and then actually reverse
                  net effect is to swap forward and backward slashes
m               execute map using block
rm              reverse array, and output all rows

```

Run this one

# Answer
> 1 votes
# Haskell, 193 bytes

Longer than the winner, but the approach may be interesting -- uses even `cos` and `pi` :)

Code:

```
i s e f|max e f>s=""|max e f<s=" "|e==s="\\"|1<2="/"
w n y x=head$do{d<-[1..n];o<-[-2*d..2*d];z<-[(cos(pi*(n-d)))*o+x];i(2*d)(abs$z-y)(abs$z+y-1)}++" "
n!h=h<$>[1-2*n..2*n]
f n=((2*n)!)<$>n!w n

```

Run it like this:

```
mapM_ putStrLn (f 4)

```

This program basically 'draws' many diamonds like this one:

```
------------------------
------------------------
-----------/\-----------
----------/  \----------
---------/    \---------
--------/      \--------
--------\      /--------
---------\    /---------
----------\  /----------
-----------\/-----------
------------------------
------------------------

```

Function `i s e f` 'draws' one diamond of size `s`, where `e, f` are `(abs$z-y)(abs$z+y-1)`.

Function `w` moves the diamonds drawn by `i` to correct places. `head` used in its definition is responsible for looking at the topmost layer only.

Try it here

# Answer
> 1 votes
# Charcoal, 42 bytes

```
ＦＮ«↗×⊗⊕ι/↓↘Ｇ↖²→⊕×⁴⊕ι↘²\Ｇ←⁴↘⊕⊗ι→⁴\Ｍ⁴→‖Ｔ»‖Ｍ↓

```

Try it online! Link is to verbose version of code. Explanation:

```
ＦＮ«

```

Draw the cubes from the smallest to the largest. (Drawing from the largest to the smallest meant that I ended up with a mirror image for odd numbers which cost too many bytes to fix.)

```
↗×⊗⊕ι/

```

Print a line of `/`s. (This will become the `\`s on the right, but the drawing is done mirrored because it's golfier to mirror at the end of the loop.)

```
↓↘Ｇ↖²→⊕×⁴⊕ι↘²\

```

Print the top two rows of `\`s. (Drawing all the `\`s in one polygon meant that the cursor ended up in an awkward position which cost too many bytes to fix.)

```
Ｇ←⁴↘⊕⊗ι→⁴\

```

Print the left four rows of `\`s. (The fifth row comes from the previous cube.)

```
Ｍ⁴→

```

Move to the start of the next cube.

```
‖Ｔ»

```

Reflect horizontally ready for the next cube.

```
‖Ｍ↓

```

Mirror everything vertically to complete the cube.

---
Tags: code-golf, ascii-art
---


title: (-a) × (-a) = a × a

text:
# Question
Title: (-a) × (-a) = a × a
We all know that \\$(-a) \times (-a) = a \times a\\$ (hopefully), but can you prove it?

Your task is to prove this fact using the ring axioms. What are the ring axioms? The ring axioms are a list of rules that two binary operations on a set have to follow. The two operation are addition, \\$+\\$, and multiplication, \\$\times\\$. For this challenge here are the ring axioms where \\$+\\$ and \\$\times\\$ are closed binary operations on some set \\$S\\$, \\$-\\$ is a closed unary operation on \\$S\\$, and \\$a\\$, \\$b\\$, \\$c\\$ are members of \\$S\\$:

1. \\$a + (b + c) = (a + b) + c\\$
2. \\$a + 0 = a\\$
3. \\$a + (-a) = 0\\$
4. \\$a + b = b + a\\$*
5. \\$a \times (b \times c) = (a \times b) \times c\\$
6. \\$a \times 1 = a\\$
7. \\$1 × a = a\\$
8. \\$a \times (b + c) = (a \times b) + (a × c)\\$
9. \\$(b + c) \times a = (b \times a) + (c \times a)\\$

Your proof should be a string of equalities each being the application of one axiom.

You may apply the axioms to either the entire expression or to some sub-expression. For example if we have \\$(a + c) + (b + c)\\$ we can apply Axiom 4 to just the \\$(b + c)\\$ term, the \\$(a + c)\\$ term or the entire expression as a whole. The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to \\$((a \times c) + b) + ((-a) + 1)\\$ to get \\$((-a) + 1) + ((a \times c) + b)\\$. In each step of the proof you can only apply *one* axiom to *one* expression. All axioms are bidirectional, meaning substitution can go in either direction. Things like the following are not allowed

```
(a + b) + (c + d) = (a + (b + c)) + d Ax. 1

```

This should be done in two steps:

```
(a + b) + (c + d) = ((a + b) + c) + d Ax. 1
                  = (a + (b + c)) + d Ax. 1

```

Facts you might normally take for granted but are not listed on the axioms list *cannot be assumed*, for example \\$(-a) = (-1) \times a\\$ is true but requires multiple steps to preform.

User Anthony has kindly provided a online proof validator that can be used as a replacement for TIO.

## Example proof

Here is an example proof that \\$-(-a) = a\\$ with the axioms used labeled on the right of each step.

```
 -(-a) = (-(-a)) + 0          Ax. 2
       = 0 + (-(-a))          Ax. 4
       = (a + (-a)) + (-(-a)) Ax. 3
       = a + ((-a) + (-(-a))) Ax. 1
       = a + 0                Ax. 3
       = a                    Ax. 2

```

Try it online!

You will be tasked to prove \\$(-a) \times (-a) = a \times a\\$ using successive substitution like that shown above.

## Scoring

This is so your answers will be scored in number of steps taken to get from \\$(-a) \times (-a)\\$ to \\$a \times a\\$, with a lower score being better.

### Lemmas

Some answers have chosen to use Lemmas in their proofs, so I will describe how that should be scored to avoid any confusion. For the uninitiated, lemmas are proofs of facts that you use later in the proof. In real mathematics they can be helpful in organizing your thoughts or conveying information clearly to the reader. In this challenge using lemmas should not have an direct effect on your score. (Although proof organization may make it easier or harder to golf)

If you choose to use lemmas it will cost as many steps as it took to prove that lemma in the first place each time you use it. For example the here is the score breakdown of a proof using lemmas.

```
Lemma:
a × 0 = 0

Proof (7 steps):
a × 0 = (a × 0) + 0                        Ax. 2 (1)
      = (a × 0) + ((a × b) + (-(a × b)))   Ax. 3 (1)
      = ((a × 0) + (a × b)) + (-(a × b))   Ax. 1 (1)
      = (a × (0 + b)) + (-(a × b))         Ax. 8 (1)
      = (a × (b + 0)) + (-(a × b))         Ax. 4 (1)
      = (a × b) + (-(a × b))               Ax. 2 (1)
      = 0                                  Ax. 3 (1)

Theorem:
(a × 0) + (b × 0) = 0

Proof (15 steps):
(a × 0) + (b × 0) = 0 + (b × 0)  Lemma (7)
                  = (b × 0) + 0  Ax. 4 (1)
                  = b × 0        Ax. 2 (1)
                  = 0            Lemma (7)

```

---

\*: It has been pointed out that this axiom is not strictly necessary to prove this property, however you are still allowed to use it.

†: Since \\$1\\$ does not appear in the desired equality any proof that uses these axioms is not minimal. That is these axioms cannot help with proving the desired fact. They have been included just for the sake of completeness.

# Answer
## 18 Steps

```
(-a)*(-a) = ((-a)*(-a))+0                                             Axiom 2
          = ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))        Axiom 3
          = (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a))))        Axiom 4
          = ((a*a)+((a*(-a))+((-a)*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = ((a*a)+((a+(-a))*(-a)))+(-((a*a)+(a*(-a))))               Axiom 9
          = ((a*a)+(0*(-a)))+(-((a*a)+(a*(-a))))                      Axiom 3
          = ((a*(a+0))+(0*(-a)))+(-((a*a)+(a*(-a))))                  Axiom 2
          = ((a*(a+(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))           Axiom 3
          = (((a*a)+(a*(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))       Axiom 8
          = ((a*a)+((a*(a+(-a)))+(0*(-a))))+(-((a*a)+(a*(-a))))       Axiom 1
          = (a*a)+(((a*(a+(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))       Axiom 1
          = (a*a)+((((a*a)+(a*(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))   Axiom 8
          = (a*a)+(((a*a)+((a*(-a))+(0*(-a))))+(-((a*a)+(a*(-a)))))   Axiom 1
          = (a*a)+(((a*a)+((a+0)*(-a)))+(-((a*a)+(a*(-a)))))          Axiom 9
          = (a*a)+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))              Axiom 2
          = (a*a)+0                                                   Axiom 3
          = a*a                                                       Axiom 2

```

I wrote a program to check my solution. So if you find an error in this, then my program is wrong too.
> 58 votes

# Answer
## 18 steps

Different from the already posted 18-step solution.

```
a*a = a*a + 0                                                 A2
    = a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))        A3
    = (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))        A1
    = (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a)))          A8
    = a*(a + ((-a) + (-a))) + (-(a*(-a) + a*(-a)))            A8
    = a*((a + (-a)) + (-a)) + (-(a*(-a) + a*(-a)))            A1
    = a*(0 + (-a)) + (-(a*(-a) + a*(-a)))                     A3
    = a*((-a) + 0) + (-(a*(-a) + a*(-a)))                     A4
    = a*(-a) + (-(a*(-a) + a*(-a)))                           A2
    = (a + 0)*(-a) + (-(a*(-a) + a*(-a)))                     A2
    = (a + (a + (-a)))*(-a) + (-(a*(-a) + a*(-a)))            A3
    = ((a + a) + (-a))*(-a) + (-(a*(-a) + a*(-a)))            A1
    = ((-a) + (a + a))*(-a) + (-(a*(-a) + a*(-a)))            A4
    = ((-a)*(-a) + (a + a)*(-a)) + (-(a*(-a) + a*(-a)))       A9
    = ((-a)*(-a) + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))  A9
    = (-a)*(-a) + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))  A1
    = (-a)*(-a) + 0                                           A3
    = (-a)*(-a)                                               A2

```
> 38 votes

# Answer
# ~~29~~ 26 Steps

No lemmas!

Comment if you see anything wrong. (It's very easy to make a mistake)

```
(-a) × (-a) = ((-a) + 0) × (-a)                                                  Ax. 2
            = ((-a) + (a + (-a))) × (-a)                                         Ax. 3
            = ((a + (-a)) + (-a)) × (-a)                                         Ax. 4
            = (a + ((-a) + (-a))) × (-a)                                         Ax. 1
            = (a × (-a)) + (((-a) + (-a)) × (-a))                                Ax. 9
            = (a × ((-a) + 0)) + (((-a) + (-a)) × (-a))                          Ax. 2
            = (a × ((-a) + (a + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 3
            = (a × ((a + (-a)) + (-a))) + (((-a) + (-a)) × (-a))                 Ax. 4
            = (a × (a + ((-a) + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 1
            = ((a × a) + (a × ((-a) + (-a)))) + (((-a) + (-a)) × (-a))           Ax. 8
            = (a × a) + ((a × ((-a) + (-a))) + (((-a) + (-a)) × (-a)))           Ax. 1
            = (a × a) + (((a × (-a)) + (a × (-a))) + (((-a) + (-a)) × (-a)))     Ax. 8
            = (a × a) + (((a + a) × (-a)) + (((-a) + (-a)) × (-a)))              Ax. 9
            = (a × a) + (((a + a) + ((-a) + (-a))) × (-a))                       Ax. 9
            = (a × a) + ((((a + a) + (-a)) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + (a + (-a))) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + 0) + (-a)) × (-a))                                Ax. 3
            = (a × a) + ((a + (-a)) × (-a))                                      Ax. 2
            = (a × a) + (0 × (-a))                                               Ax. 3
            = (a × a) + ((0 × (-a)) + 0)                                         Ax. 2
            = (a × a) + ((0 × (-a)) + ((0 × (-a)) + (-(0 × (-a)))))              Ax. 3
            = (a × a) + (((0 × (-a)) + (0 × (-a))) + (-(0 × (-a))))              Ax. 1
            = (a × a) + (((0 + 0) × (-a)) + (-(0 × (-a))))                       Ax. 9
            = (a × a) + ((0 × (-a)) + (-(0 × (-a))))                             Ax. 2
            = (a × a) + 0                                                        Ax. 3
            = (a × a)                                                            Ax. 2

```

Credit goes to Maltysen for **0 × (-a) = 0**
> 29 votes

# Answer
# 18 steps

Not the first 18-step proof, but it’s simpler than the others.

```
(-a)*(-a)
= (-a)*(-a) + 0                             [Axiom 2]
= (-a)*(-a) + ((-a)*a + -((-a)*a))          [Axiom 3]
= ((-a)*(-a) + (-a)*a) + -((-a)*a)          [Axiom 1]
= ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a)    [Axiom 2]
= ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a)  [Axiom 9]
= (((-a)*(-a) + (-a)*a) + 0*a) + -((-a)*a)  [Axiom 1]
= ((-a)*((-a) + a) + 0*a) + -((-a)*a)       [Axiom 8]
= ((-a)*(a + (-a)) + 0*a) + -((-a)*a)       [Axiom 4]
= ((-a)*0 + 0*a) + -((-a)*a)                [Axiom 3]
= (0*a + (-a)*0) + -((-a)*a)                [Axiom 4]
= ((a + (-a))*a + (-a)*0) + -((-a)*a)       [Axiom 3]
= ((a*a + (-a)*a) + (-a)*0) + -((-a)*a)     [Axiom 9]
= (a*a + ((-a)*a + (-a)*0)) + -((-a)*a)     [Axiom 1]
= (a*a + (-a)*(a + 0)) + -((-a)*a)          [Axiom 8]
= (a*a + (-a)*a) + -((-a)*a)                [Axiom 2]
= a*a + ((-a)*a + -((-a)*a))                [Axiom 1]
= a*a + 0                                   [Axiom 3]
= a*a                                       [Axiom 2]

```

Validate
> 22 votes

# Answer
# 23 steps

```
(-a) * (-a) = ((-a) * (-a)) + 0                                 ✔ axiom 2
            = ((-a) * (-a)) + (((-a) * a) + -((-a) * a))        ✔ axiom 3
            = (((-a) * (-a)) + (-a) * a) + -((-a) * a)          ✔ axiom 1
            = (-a) * (-a + a) + -((-a) * a)                     ✔ axiom 8
            = (-a) * (a + (-a)) + -((-a) * a)                   ✔ axiom 4
            = ((-a) * 0) + -((-a) * a)                          ✔ axiom 3
            = (((-a) * 0) + 0) + -((-a) * a)                    ✔ axiom 2
            = ((-a) * 0 + ((-a)*0 + -((-a)*0))) + -((-a) * a)   ✔ axiom 3
            = (((-a) * 0 + (-a)*0) + -((-a)*0)) + -((-a) * a)   ✔ axiom 1
            = ((-a) * (0 + 0) + -((-a)*0)) + -((-a) * a)        ✔ axiom 8
            = ((-a) * 0 + -((-a)*0)) + -((-a) * a)              ✔ axiom 2
            = 0 + -((-a) * a)                                   ✔ axiom 3
            = (0* a) + -(0*a) + -((-a) * a)                     ✔ axiom 3
            = ((0+0)* a) + -(0*a) + -((-a) * a)                 ✔ axiom 2
            = ((0 * a ) + (0*a) + -(0*a)) + -((-a) * a)         ✔ axiom 9
            = ((0 * a ) + ((0*a) + -(0*a))) + -((-a) * a)       ✔ axiom 1
            = ((0 * a ) + 0) + -((-a) * a)                      ✔ axiom 3
            = (0 * a ) + -((-a) * a)                            ✔ axiom 2
            = ((a + -a) * a ) + -((-a) * a)                     ✔ axiom 3
            = ((a * a) + (-a) * a) + -((-a) * a)                ✔ axiom 9
            = (a * a) + (((-a) * a) + -((-a) * a))              ✔ axiom 1
            = (a * a) + 0                                       ✔ axiom 3
            = a * a                                             ✔ axiom 2

```

Try it online!

Yes you read that right, I've written a proof-checker for this puzzle (naturally there's a possibility that the checker itself is wrong)
> 15 votes

# Answer
```
A2: (-a) x (-a) = ((-a) + 0) x (-a)
A3:             = ((-a) + (a + (-a))) x (-a)
A9:             = ((-a) x (-a)) + ((a + (-a)) x (-a))
A4:             = ((-a) x (-a)) + (((-a) + a) x (-a))
A9:             = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a))
A2:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + 0))
A3:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + (a x (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x a) + (a x (-a))))
A4:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x (-a)) + (a x a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + ((a x ((-a) + (-a))) + (a x a))
A1:             = (((-a) x ((-a) + (-a))) + (a x ((-a) + (-a)))) + (a x a)
A9:             = (((-a) + a) x ((-a) + (-a))) + (a x a)
A4:             = ((a + (-a)) x ((-a) + (-a))) + (a x a)
Lemma:          = (0 x ((-a) + (-a))) + (a x a)
A3:             = 0 + (a x a)
A4:             = (a x a) + 0
A2:             = (a x a)

Lemma: 0 = 0 x a

A3: 0 = (0 x a) + (-(0 x a))
A2:   = ((0 + 0) x a) + (-(0 x a))
A9:   = ((0 x a) + (0 x a)) + (-(0 x a))
A1:   = (0 x a) + ((0 x a) + (-(0 x a)))
A3:   = (0 x a) + 0
A2:   = (0 x a)

```

**~~27~~ 26 steps** Thank you Funky Computer Man for noticing a duplicate line.
> 9 votes

# Answer
# 304 steps

Community wiki because this proof is generated by Mathematica's FindEquationalProof function.

The proof is rather long. Mathematica doesn't know how to golf it.

This is the Mathematica code that generates the proof (requires Mathematica 11.3), where `p`, `t`, `n` means `+`, `×`, `-` respectively:

```
ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
   ForAll[a, p[a, 0] == a],
   ForAll[a, p[a, n[a]] == 0],
   ForAll[{a, b}, p[a, b] == p[b, a]],
   ForAll[{a, b, c}, t[a, t[b, c]] == t[t[a, b], c]],
   ForAll[a, t[a, 1] == a], ForAll[a, t[1, a] == a],
   ForAll[{a, b, c}, t[a, p[b, c]] == p[t[a, b], t[a, c]]],
   ForAll[{a, b, c}, t[p[b, c], a] == p[t[b, a], t[c, a]]]};

proof = FindEquationalProof[t[n[a], n[a]] == t[a, a], ringAxioms];

proof["ProofNotebook"]

```

It is not easy to count the steps directly, so I calculate it by the number of paths from the axioms to the conclusion in the "proof graph".

```
graph = proof["ProofGraph"];
score = Sum[
  Length[FindPath[graph, axiom, "Conclusion 1", Infinity,
    All]], {axiom,
   Select[VertexList[graph], StringMatchQ["Axiom " ~~ __]]}]

```

Try it online!

This is the proof generated by the code:

```
Axiom 1

We are given that:

x1==p[x1, 0]

Axiom 2

We are given that:

x1==t[x1, 1]

Axiom 3

We are given that:

x1==t[1, x1]

Axiom 4

We are given that:

p[x1, x2]==p[x2, x1]

Axiom 5

We are given that:

p[x1, p[x2, x3]]==p[p[x1, x2], x3]

Axiom 6

We are given that:

p[x1, n[x1]]==0

Axiom 7

We are given that:

p[t[x1, x2], t[x3, x2]]==t[p[x1, x3], x2]

Axiom 8

We are given that:

p[t[x1, x2], t[x1, x3]]==t[x1, p[x2, x3]]

Axiom 9

We are given that:

t[x1, t[x2, x3]]==t[t[x1, x2], x3]

Hypothesis 1

We would like to show that:

t[n[a], n[a]]==t[a, a]

Critical Pair Lemma 1

The following expressions are equivalent:

p[0, x1]==x1

Proof

Note that the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Axiom 4 and Axiom 1 respectively.

Critical Pair Lemma 2

The following expressions are equivalent:

p[x1, p[n[x1], x2]]==p[0, x2]

Proof

Note that the input for the rule:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Axiom 5 and Axiom 6 respectively.

Critical Pair Lemma 3

The following expressions are equivalent:

t[p[1, x1], x2]==p[x2, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x3_, x2_]]->t[p[x1, x3], x2]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[1, x1_]->x1

where these rules follow from Axiom 7 and Axiom 3 respectively.

Critical Pair Lemma 4

The following expressions are equivalent:

t[x1, p[1, x2]]==p[x1, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x1_, x3_]]->t[x1, p[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 1]->x1

where these rules follow from Axiom 8 and Axiom 2 respectively.

Critical Pair Lemma 5

The following expressions are equivalent:

t[p[1, x1], 0]==t[x1, 0]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

p[x1_, t[x2_, x1_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 6

The following expressions are equivalent:

t[0, 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Critical Pair Lemma 5 and Axiom 1 respectively.

Substitution Lemma 1

It can be shown that:

t[0, 0]==0

Proof

We start by taking Critical Pair Lemma 6, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 7

The following expressions are equivalent:

t[x1, 0]==t[p[x1, 1], 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 5 and Axiom 4 respectively.

Critical Pair Lemma 8

The following expressions are equivalent:

t[0, p[1, x1]]==t[0, x1]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

p[x1_, t[x1_, x2_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 9

The following expressions are equivalent:

t[p[x1, 1], p[1, 0]]==p[p[x1, 1], t[x1, 0]]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[p[x1_, 1], 0]->t[x1, 0]

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 7 respectively.

Substitution Lemma 2

It can be shown that:

t[p[x1, 1], 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Critical Pair Lemma 9, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 3

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Substitution Lemma 2, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Substitution Lemma 4

It can be shown that:

p[x1, 1]==p[x1, p[1, t[x1, 0]]]

Proof

We start by taking Substitution Lemma 3, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Critical Pair Lemma 10

The following expressions are equivalent:

t[0, x1]==t[0, p[x1, 1]]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 8 and Axiom 4 respectively.

Critical Pair Lemma 11

The following expressions are equivalent:

t[p[1, 0], p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

t[x2_, x1_]

which can be unified with the input for the rule:

t[0, p[x1_, 1]]->t[0, x1]

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 10 respectively.

Substitution Lemma 5

It can be shown that:

t[1, p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Critical Pair Lemma 11, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 6

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Substitution Lemma 5, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Substitution Lemma 7

It can be shown that:

p[x1, 1]==p[x1, p[1, t[0, x1]]]

Proof

We start by taking Substitution Lemma 6, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Substitution Lemma 8

It can be shown that:

p[x1, p[n[x1], x2]]==x2

Proof

We start by taking Critical Pair Lemma 2, and apply the substitution:

p[0, x1_]->x1

which follows from Critical Pair Lemma 1.

Critical Pair Lemma 12

The following expressions are equivalent:

n[n[x1]]==p[x1, 0]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

p[n[x1_], x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Substitution Lemma 8 and Axiom 6 respectively.

Substitution Lemma 9

It can be shown that:

n[n[x1]]==x1

Proof

We start by taking Critical Pair Lemma 12, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 13

The following expressions are equivalent:

x1==p[n[x2], p[x2, x1]]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

n[x1_]

which can be unified with the input for the rule:

n[n[x1_]]->x1

where these rules follow from Substitution Lemma 8 and Substitution Lemma 9 respectively.

Critical Pair Lemma 14

The following expressions are equivalent:

t[x1, x2]==p[n[x2], t[p[1, x1], x2]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 3 respectively.

Critical Pair Lemma 15

The following expressions are equivalent:

t[x1, x2]==p[n[x1], t[x1, p[1, x2]]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 4 respectively.

Critical Pair Lemma 16

The following expressions are equivalent:

p[1, t[x1, 0]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[x1_, 0]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 4 respectively.

Substitution Lemma 10

It can be shown that:

p[1, t[x1, 0]]==1

Proof

We start by taking Critical Pair Lemma 16, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 17

The following expressions are equivalent:

t[t[x1, 0], 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[x1_, 0]]->1

where these rules follow from Critical Pair Lemma 5 and Substitution Lemma 10 respectively.

Substitution Lemma 11

It can be shown that:

t[x1, t[0, 0]]==t[1, 0]

Proof

We start by taking Critical Pair Lemma 17, and apply the substitution:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

which follows from Axiom 9.

Substitution Lemma 12

It can be shown that:

t[x1, 0]==t[1, 0]

Proof

We start by taking Substitution Lemma 11, and apply the substitution:

t[0, 0]->0

which follows from Substitution Lemma 1.

Substitution Lemma 13

It can be shown that:

t[x1, 0]==0

Proof

We start by taking Substitution Lemma 12, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 18

The following expressions are equivalent:

t[x1, t[0, x2]]==t[0, x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 0]->0

where these rules follow from Axiom 9 and Substitution Lemma 13 respectively.

Critical Pair Lemma 19

The following expressions are equivalent:

p[1, t[0, x1]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[0, x1_]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 7 respectively.

Substitution Lemma 14

It can be shown that:

p[1, t[0, x1]]==1

Proof

We start by taking Critical Pair Lemma 19, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 20

The following expressions are equivalent:

t[0, t[0, x1]]==t[0, 1]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[0, x1_]]->1

where these rules follow from Critical Pair Lemma 8 and Substitution Lemma 14 respectively.

Substitution Lemma 15

It can be shown that:

t[0, x1]==t[0, 1]

Proof

We start by taking Critical Pair Lemma 20, and apply the substitution:

t[x1_, t[0, x2_]]->t[0, x2]

which follows from Critical Pair Lemma 18.

Substitution Lemma 16

It can be shown that:

t[0, x1]==0

Proof

We start by taking Substitution Lemma 15, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Critical Pair Lemma 21

The following expressions are equivalent:

t[n[1], x1]==p[n[x1], t[0, x1]]

Proof

Note that the input for the rule:

p[n[x1_], t[p[1, x2_], x1_]]->t[x2, x1]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 14 and Axiom 6 respectively.

Substitution Lemma 17

It can be shown that:

t[n[1], x1]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 21, and apply the substitution:

t[0, x1_]->0

which follows from Substitution Lemma 16.

Substitution Lemma 18

It can be shown that:

t[n[1], x1]==n[x1]

Proof

We start by taking Substitution Lemma 17, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 22

The following expressions are equivalent:

t[n[1], t[x1, x2]]==t[n[x1], x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[n[1], x1_]->n[x1]

where these rules follow from Axiom 9 and Substitution Lemma 18 respectively.

Substitution Lemma 19

It can be shown that:

n[t[x1, x2]]==t[n[x1], x2]

Proof

We start by taking Critical Pair Lemma 22, and apply the substitution:

t[n[1], x1_]->n[x1]

which follows from Substitution Lemma 18.

Critical Pair Lemma 23

The following expressions are equivalent:

t[x1, n[1]]==p[n[x1], t[x1, 0]]

Proof

Note that the input for the rule:

p[n[x1_], t[x1_, p[1, x2_]]]->t[x1, x2]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 15 and Axiom 6 respectively.

Substitution Lemma 20

It can be shown that:

t[x1, n[1]]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 23, and apply the substitution:

t[x1_, 0]->0

which follows from Substitution Lemma 13.

Substitution Lemma 21

It can be shown that:

t[x1, n[1]]==n[x1]

Proof

We start by taking Substitution Lemma 20, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 24

The following expressions are equivalent:

n[t[x1, x2]]==t[x1, t[x2, n[1]]]

Proof

Note that the input for the rule:

t[x1_, n[1]]->n[x1]

contains a subpattern of the form:

t[x1_, n[1]]

which can be unified with the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

where these rules follow from Substitution Lemma 21 and Axiom 9 respectively.

Substitution Lemma 22

It can be shown that:

t[n[x1], x2]==t[x1, t[x2, n[1]]]

Proof

We start by taking Critical Pair Lemma 24, and apply the substitution:

n[t[x1_, x2_]]->t[n[x1], x2]

which follows from Substitution Lemma 19.

Substitution Lemma 23

It can be shown that:

t[n[x1], x2]==t[x1, n[x2]]

Proof

We start by taking Substitution Lemma 22, and apply the substitution:

t[x1_, n[1]]->n[x1]

which follows from Substitution Lemma 21.

Substitution Lemma 24

It can be shown that:

t[a, n[n[a]]]==t[a, a]

Proof

We start by taking Hypothesis 1, and apply the substitution:

t[n[x1_], x2_]->t[x1, n[x2]]

which follows from Substitution Lemma 23.

Conclusion 1

We obtain the conclusion:

True

Proof

Take Substitution Lemma 24, and apply the substitution:

n[n[x1_]]->x1

which follows from Substitution Lemma 9.

```
> 9 votes

# Answer
# 6 + 7 + 7 + 6 + 3 = 29 steps

I really hope I didn't screw anything up, leave a comment if you think I did.

```
Lemma 1. a*0=0 (6 steps)

0 = a*0 + -(a*0)  axiom 3
= a*(0+0) + -(a*0) axiom 2
= (a*0 + a*0) + -(a*0) axiom 8
= a*0 + (a*0 + -(a*0)) axiom 1
= a*0 + 0 axiom 3
= a*0 axiom 2

Lemma 2. a*(-b) = -(a*b) (7 steps)

a*(-b) = a*(-b) + 0 axiom 2
= a*(-b) + (a*b + -(a*b)) axiom 3
= (a*(-b) + a*b) + -(a*b) axiom 1
= a*(-b+b) + -(a*b) axiom 8
= a*0 + -(a*b) axiom 3
= 0 + -(a*b) lemma 1
= -(a*b) axiom 2

Lemma 3. (-a)*b = -(a*b) (7 steps)
    same as above

Lemma 4. -(-(a)) = a (6 steps)

 -(-a) = (-(-a)) + 0    axiom 2
 = 0 + (-(-a))          axiom 4
 = (a + (-a)) + (-(-a)) axiom 3
 = a + ((-a) + (-(-a))) axiom 1
 = a + 0                axiom 3
 = a                    axiom 2

Theorem. -a*-a=0 (3 steps)

-a*-a = -(a*(-a)) lemma 3
= -(-(a*a)) lemma 2
= a*a lemma 4

Q.E.D.

```
> 8 votes

# Answer
## ~~22~~ 23 Steps

New answer, as my previous was flawed. Let me add some general comments first:

* The problem does not allow to add terms on both sides of an equation; rather, we can only modify an initial string.
* Multiplication is not assumed to be commutative.
* We are given a unit **1**, but it plays no role whatsoever in the puzzle because it is involved exclusively in the rules that define it.

Now for the proof (notice I define **n = (-a)** to simplify reading):

```
(-a)×(-a) :=
n×n =
n×n + 0 =                                [Ax. 2]
n×n + [n×a + -(n×a)] =                   [Ax. 3]
[n×n + n×a] + -(n×a) =                   [Ax. 1]
[n×(n+a)] + -(n×a) =                     [Ax. 8]
[n×(n+a) + 0] + -(n×a) =                 [Ax. 2]
[n×(n+a) + (n×a + -(n×a))] + -(n×a) =    [Ax. 3]
[(n×(n+a) + n×a) + -(n×a)] + -(n×a) =    [Ax. 1]
[n×((n+a) + a) + -(n×a)] + -(n×a) =      [Ax. 8]
[n×((a+n) + a) + -(n×a)] + -(n×a) =      [Ax. 4]
[n×(0 + a) + -(n×a)] + -(n×a) =          [Ax. 3]
[n×(a + 0) + -(n×a)] + -(n×a) =          [Ax. 4]
[n×a + -(n×a)] + -(n×a) =                [Ax. 2]
[(n+0)×a + -(n×a)] + -(n×a) =            [Ax. 2]
[(0+n)×a + -(n×a)] + -(n×a) =            [Ax. 4]
[((a+n)+n)×a + -(n×a)] + -(n×a) =        [Ax. 3]
[((a+n)×a+n×a) + -(n×a)] + -(n×a) =      [Ax. 9]
[(a+n)×a+(n×a + -(n×a))] + -(n×a) =      [Ax. 1]
[(a+n)×a + 0] + -(n×a) =                 [Ax. 3]
[(a+n)×a] + -(n×a) =                     [Ax. 2]
[a×a+n×a] + -(n×a) =                     [Ax. 9]
a×a+[n×a + -(n×a)] =                     [Ax. 1]
a×a+0 =                                  [Ax. 3]
a×a                                      [Ax. 2]

```
> 7 votes

# Answer
# 34 steps

```
Lemma 1: 0=0*a (8 steps)
    0
A3: a*0 + -(a*0)
A4: -(a*0) + a*0
A2: -(a*0) + a*(0+0)
A8: -(a*0) + (a*0 + a*0)
A1: (-(a*0) + a*0) + a*0
A3: 0 + a*0
A4: a*0 + 0
A2: a*0

Theorem: -a*-a = a*a (49 steps)

    -a * -a
A2: (-a+0) * -a
A2: (-a+0) * (-a+0)
A3: (-a+(a+-a)) * (-a+0)
A3: (-a+(a+-a)) * (-a+(a+-a))
A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a))
A8: -a*(-a+(a+-a)) + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+0)      + a*(-a+(a+-a))
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*(a+-a)
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*-a          + a*-a + a*a + a*-a
A8: -a*-a          + (-a+a)*-a             + a*a + a*-a
A3: -a*-a          + 0*-a                  + a*a + a*-a
L1: -a*-a          + 0                     + a*a + a*-a
A2: -a*-a                                  + a*a + a*-a
A4: a*a + -a*-a + a*-a
A8: a*a + (-a+a)*-a
A3: a*a + 0*-a
L1: a*a + 0
A2: a*a

```
> 5 votes

# Answer
# 25 steps

Note: based on the question, I'm assuming that the rules of logic (including equality) are implied and do not count towards the total step count. That is, things like "if x=y, then y=x" and "if ((P AND Q) AND R) then (P AND (Q AND R))" can be used implicitly.

**Lemma Z** *\[6 steps\]*: `0*a = 0`:

```
0 = (0*a) + (-(0*a))       | Ax. 3
  = ((0+0)*a) + (-(0*a))   | Ax. 2
  = (0*a + 0*a) + (-(0*a)) | Ax. 9
  = 0*a + (0*a + (-(0*a))) | Ax. 1
  = 0*a + (0)              | Ax. 3
  = 0*a                    | Ax. 2

```

**Lemma M** *\[12 steps\]*: `(-a)*b = -(a*b)`

```
(-a)*b = (-a)*b + 0                | Ax. 2
       = (-a)*b + (a*b + (-(a*b))) | Ax. 3
       = ((-a)*b + a*b) + (-(a*b)) | Ax. 5
       = ((-a)+a)*b + (-(a*b))     | Ax. 9
       = 0*b + (-(a*b))            | Ax. 3
       = 0 + (-(a*b))              | Lem. Z [6]
       = -(a*b)                    | Ax. 2

```

**Theorem** *\[25 steps\]*: `(-a)*(-a) = a*a`

```
(-a)*(-a) = (-a)*(-a) + 0                | Ax. 2
          = 0 + (-a)*(-a)                | Ax. 4
          = (a*a + (-(a*a))) + (-a)*(-a) | Ax. 3
          = a*a + ((-(a*a)) + (-a)*(-a)) | Ax. 1
          = a*a + ((-a)*a + (-a)*(-a))   | Lem. M [12]
          = a*a + ((-a)*(a + (-a)))      | Ax. 8
          = a*a + ((-a)*0)               | Ax. 3
          = a*a + 0                      | Lem. Z [6]
          = a*a                          | Ax. 2

```

I feel like there's room for improvement here; for example, I use the commutative property of addition, though it feels like that should be unnecessary, since `(-a)*(-a) = a*a` is true in algebraic structures where addition is non-commutative. On the other hand, in those structures, the additive identity is commutative, and that's all I needed for the proof. I dunno. More generally, the proof's structure seems rather directionless; I just sort of threw stuff at the problem until it worked, so I bet there's some optimization to be done.

This was fun--thanks for the interesting and creative question OP! I haven't seen challenges like these before; hopefully becomes a thing!
> 5 votes

---
Tags: math, atomic-code-golf, abstract-algebra, proof-golf
---


title: Zero-sum counting

text:
# Question
Title: Zero-sum counting
Write a program or function that given *n ≥ 1* returns the number of solutions to ±1 ± 2 ± 3 ± ... ± n = 0.

For n = 6 there are no solutions, so the answer is 0. For n = 4 there are two solutions, so the answer is 2 (the two solutions are 1 - 2 - 3 + 4 = -1 + 2 + 3 - 4 = 0).

This is OEIS sequence A063865. Some example input/outpus are:

```
n       a(n)
1       0
2       0
3       2
4       2
5       0
6       0
7       8
8       14
9       0
10      0
11      70
12      124
13      0
14      0
15      722
16      1314

```

---

Shortest code in bytes wins.

# Answer
# JavaScript (ES6), 35 bytes

*Saved 1 byte thanks to @tsh*

```
f=(n,s)=>n--?f(n,n-~s)+f(n,n+~s):!s

```

Try it online!
> 10 votes

# Answer
# Wolfram Language (Mathematica), 33 bytes

```
Count[{1,-1}~Tuples~#.Range@#,0]&

```

Counts the `n`-tuples of 1 and -1 whose dot product with `Range[n]` is 0.

Try it online!
> 9 votes

# Answer
# Haskell, 42 bytes

```
f n=sum[1|0<-sum<$>mapM(\x->[x,-x])[1..n]]

```

Try it online!

This is ~~2~~ 1 byte shorter than any recursive function that I could write.
> 9 votes

# Answer
# 05AB1E, 10 bytes

```
X®‚sã€ƶO_O

```

Try it online!

**Explanation**

```
X®‚          # push [1,-1]
   sã        # cartesian product with input
     €ƶ      # multiply each element in each list with its 1-based index
       O     # sum each list
        _    # logical negation of each sum
         O   # sum

```
> 6 votes

# Answer
# C (gcc), ~~45~~ ~~62~~ ~~52~~ 50 bytes

```
f(n,r){n=n?f(n-1,r+n)+f(n-1,r-n):!r;}F(n){f(n,0);}

```

Port of Kevin Cruijssen's Java 8 answer.

Try it online here.

Note that due to the improvements suggested in the comments, the code produces undefined behaviour to the point of not working when compiled with clang.

Thanks to etene for golfing 3 bytes. Thanks to Kevin Cruijssen for golfing 10 more bytes. Thanks to Christoph for golfing another 2 bytes.

Ungolfed version:

```
f(n, r) { // recursive function - return type and parameter type are omitted, they default to int
    n = // instead of returning, we set n - dirty trick
        n ? // if n is not 0, recurse
        f(n-1,r+n) // +n
       +f(n-1,r-n) // -n
        !r; // else if r != 0 return 0 else return 1
}
F(n) { // function to start the recursion; again implicitly int(int)
    n = f(n, 0); // call the recursive function; this time we simply don't return
}

```
> 5 votes

# Answer
# 05AB1E, ~~9~~ 8 bytes

Thanks to **Emigna** for saving a byte!

### Code:

```
LæO·sLO¢

```

Uses the **05AB1E** encoding. Try it online!

### Explanation

```
L           # Create the list [1, 2, .., input]
 æ          # Compute the powerset of this list
  O         # Sum each list
   ·        # Double each element
    sLO     # Compute the sum of [1, 2, .., input]
       ¢    # Count the number of occurrences

```
> 5 votes

# Answer
# MATL, ~~14~~ 13 bytes

```
[la]Z^G:!Y*~s

```

*Thanks to @Giuseppe for saving 1 byte!*

Try it online! Or verify all test cases.

### Explanation

Consider `n = 3` as an example. Stack is shown upside down, that is, newest appears below.

```
[la]   % Push array [1 -1]
       % STACK: [1 -1]
Z^     % Cartesian power with inplicit input n
       % STACK: [ 1  1  1
                  1  1 -1
                  1 -1  1
                  1 -1 -1
                 -1  1  1
                 -1  1 -1
                 -1 -1  1
                 -1 -1 -1]
G:     % Push n, range: gives [1 2 ... n]
       % STACK: [ 1  1  1
                  1  1 -1
                  1 -1  1
                  1 -1 -1
                 -1  1  1
                 -1  1 -1
                 -1 -1  1
                 -1 -1 -1],
                 [1  2  3]
!      % Transpose
       % STACK: [ 1  1  1
                  1  1 -1
                  1 -1  1
                  1 -1 -1
                 -1  1  1
                 -1  1 -1
                 -1 -1  1
                 -1 -1 -1],
                 [1
                  2
                  3]
Y*     % Matrix multiplication
       % STACK: [6
                 0
                 2
                -4
                 4
                -2
                 0
                -6]
~      % Logical negation
       % STACK: [0
                 1
                 0
                 0
                 0
                 0
                 1
                 0]
s      % Sum of vector. Implicit display
       % STACK: 2

```
> 4 votes

# Answer
# Jelly, 8 bytes

```
ŒPS€ċÆṁ$

```

Try it online!

### How it works

```
ŒPS€ċÆṁ$  Main link. Argument: n

ŒP        Take the powerset of [1, ..., n].
  S€      Take the sum of each subset.
       $  Combine the two links to the left into a monadic chain.
     Æṁ       Compute the median of the sums, i.e, (1 + ... + n)/2.
    ċ         Count the occurrences of the median.

```
> 4 votes

# Answer
# APL (Dyalog), ~~31~~ 22 bytes

*9 bytes saved thanks to @H.PWiz*

```
1⊥0=⊂∘⍳+.×¨∘,3-2×∘⍳⍴∘2

```

Try it online!
> 3 votes

# Answer
# Java 8, ~~72~~ ~~71~~ 70 bytes

```
n->f(0,n)int f(int r,int n){return n>0?f(r+n,--n)+f(r+~n,n):r==0?1:0;}

```

Port of *@Arnauld*'s JavaScript (ES6) answer.
-2 bytes thanks to *@OlivierGrégoire*.

Try it online.

**Explanation:**

```
n->                 // Method with integer parameter and integer return-type
  f(0,n)            //  Call the recursive method with 0 and this parameter

int f(int r,int n){ // Recursive method with integer as both two parameters and return-type
  return n>0?       //  If `n` is not 0 yet:
    f(r+n,--n)      //   Recursive call with `r+n` (and `n` lowered by 1 first with `--n`)
    +f(r+~n,n)      //   + Recursive call with `r-n` (and `n` also lowered by 1)
   :r==0?           //  Else-if `r` is 0
     1              //   Return 1
    :               //  Else:
     0;}            //   Return 0

```
> 3 votes

# Answer
# Python 2, 74 bytes

```
def f(n):l=k=1;exec"l+=l<<n*k;k+=1;"*n;return(l>>n*n*-~n/4)%2**n*(~-n%4>1)

```

More of a fun submission, direct generating function computation.
> 3 votes

# Answer
# Octave (with Communications Package), 39 bytes

```
@(n)sum((2*de2bi(0:2^n-1)-1)*(1:n)'==0)

```

Try it online!

### Explanation:

Take a range **0 ... n^2-1** and convert it to binary. This gives a matrix with all combinations of **0** and **1**. Multiply by **2** and subtract **1** to get a matrix with all combinations of **-1** and **+1**.

Take the dot-product with a range **1 ... n** to get all combinations of **±1 ± 2 ... ±n**. Count how many are zero.

Basically the same thing, same byte count:

```
@(n)nnz(~((2*de2bi(0:2^n-1)-1)*(1:n)'))

```
> 3 votes

# Answer
# Haskell, 55 bytes

A straightforward approach of computing all those sums and checking how many are zero.

```
f 0=[0]
f n=[(n+),(n-)]>>=(<$>f(n-1))
g x=sum[1|0<-f x]

```

Try it online!

EDIT: @H.PWiz has a shorter and way more elegant solution using `mapM`!
> 3 votes

# Answer
# Python 2 and 3, 50 bytes

Recursive approach like most of the answers:

```
f=lambda n,r=0:f(n-1,r+n)+f(n-1,r-n)if n else r==0

```

Try it online

The double recursive call takes too much bytes... There's probably a way to simplify it.
> 3 votes

# Answer
# Bash \+ GNU utilities, 63 bytes

Bash can probably do better than this with recursive functions, but I can't resist this sort of `eval`/escape/expansion monstrosity:

```
p=eval\ printf\ %s
$p\\\\n \$[$($p \\\{+,-}{1..$1})]|grep -c ^0

```

Try it online!

---

Update: I don't think bash can do better with recursive functions. This is the best I could do for a score of 90. `eval` hell it is then.
> 3 votes

# Answer
# Brachylog, 12 bytes

```
⟦₁{{ṅ|}ᵐ+0}ᶜ

```

Try it online!

### Explanation

```
⟦₁               The range [1, …, Input]
  {       }ᶜ     Count the number of times the following predicate succeeds on that range:
   {  }ᵐ           Map for each element of the range:
    ṅ                Negate
     |               Or do nothing
        +0         The sum of the elements after the map is 0

```
> 3 votes

# Answer
# Octave, 42 bytes

```
@(n)sum((dec2bin(0:2^n-1)*2-97)*(1:n)'==0)

```

Try it online!
> 2 votes

# Answer
# , 32 bytes

```
1#.0=1#.1+i.*"1[:<:@+:@#:[:i.2^]

```

Try it online!

There is certainly much room for golfing. Exlpanation will follow.
> 2 votes

# Answer
# Haskell, 41 bytes

```
(%0)
n%k|n<1=0^k^2|m<-n-1=m%(k+n)+m%(k-n)

```

Try it online!
> 2 votes

# Answer
# Jelly, 10 bytes

```
RżN$ŒpS€ċ0

```

Try it online!
> 1 votes

# Answer
# Perl 5, `-p` 35 bytes

```
#!/usr/bin/perl -p
$_=grep!eval,glob join"{+,-}",0..$_

```

Try it online!
> 1 votes

# Answer
# Pari/GP, 30 bytes

```
n->Pol(prod(i=1,n,x^i+x^-i))%x

```

Try it online!
> 1 votes

# Answer
# Stax, 9 bytes

```
è%é┐╬@₧╠¬

```

Run and debug it

~~One of the shortest answers so far~~  defeated by Jelly.

I feel that checking explicitly which signs sum to zero is not very golfy, so instead I take the powerset and check how many sets in the powerset have the sum of half the nth triangular number. This method is, not surprisingly, of the same time complexity as checking which signs sum to zero.

ASCII equivalent:

```
RS{|+Hmx|+#

```
> 1 votes

# Answer
# Prolog (SWI), 99 bytes

```
p(0,0,1).
p(0,_,0).
p(X,Y,Z):-A is X-1,B is Y+X,p(A,B,C),D is Y-X,p(A,D,E),Z is C+E.
X*Y:-p(X,0,Y).

```

Try it online!
> 1 votes

# Answer
# Pyth, ~~14~~ 13 bytes

```
lf!s.nT*F_BRS

```

Try it here

### Explanation

```
lf!s.nT*F_BRS
            SQ  Take the list [1, ..., <implicit input>].
         _BR    Get the pairs [[1, -1], [2, -2], ...].
       *F       Take the Cartesian product.
 f!s.nT         Find the ones where the flattened sum is 0.
l               Take the length.

```
> 1 votes

# Answer
# CJam, 25 bytes

```
ri,:)_Wf*:a.+:m*:e_1fb0e=

```

Try it online!

This is a fairly direct translation of @emigna's 05AB1E solution. It's certainly golfable.
> 1 votes

# Answer
# Pyth, 10 bytes

```
/mysdySQsS

```

Try it online. Alternatively, verify all test cases at once.

Explaination:

```
/mysdySQsS    Implicit: Q=input()
      SQ      Generate range [1...Q]
     y        Generate powerset of above
 m            Map d in the above over...
  ysd         ... double the sum of d
        sS    Sum of range [1...Q] (final Q is implicit)
/             Count the matches (implicit output)

```
> 0 votes

# Answer
# , 28 bytes

```
(*>:){1j3#1+//.@(*/)/@,.=@i.

```

Uses the other definition from OEIS where `a(n) = coefficient of x^(n(n+1)/4) in Product_{k=1..n} (1+x^k) if n = 0 or 3 mod 4 else a(n) = 0`.

Try it online!

## Explanation

```
(*>:){1j3#1+//.@(*/)/@,.=@i.  Input: n
                          i.  Range [0, n)
                        =     Self-Classify. Forms an identity matrix of order n
          1           ,.      Stitch. Prepend 1 to each row
                    /         Reduce using
                                Convolution
                 */               Product table
           +//.                   Sum along anti-diagonals
      1j3#                    Copy each once, padding with 3 zeroes after
     {                        Index at n*(n+1)
  >:                            Increment n
 *                              Times n

```
> 0 votes

# Answer
# Husk, 9 bytes

```
#½Σḣ¹mΣṖḣ

```

Try it online!

### Explanation

```
#½Σḣ¹mΣṖḣ  Implicit input
        ḣ  [1..input]
       Ṗ   Powerset
     mΣ    Sum each list
#          Count occurrence of
   ḣ¹        [1..input]
 ½Σ          Half of sum

```
> 0 votes

# Answer
# Gol\>\<\>, 26 bytes

```
:IFPlMF2K+}:@-}||0lMF$z+|h

```

Try it online! or Run test cases from 1 to 16!

### How it works

```
:IFPlMF2K+}:@-}||0lMF$z+|h

Main outer loop
:IFPlMF ...... ||
:        Duplicate top; effectively generate two explicit zeroes
         Top is the loop counter `i`;
         the rest is the generated 2**i sums
 I       Take input as number
  F ........... |  Pop n and loop n times
   P     i++
    lM   Push stack length - 1, which is 2**(i-1)
      F ...... |   Loop 2**(i-1) times

Main inner loop: generate +i and -i from 2**(i-1) previous sums
2K+}:@-}
          Stack: [... x i]
2K        [... x i x i]    Copy top two
  +}      [x+i ... x i]    Add top two and move to the bottom
    :@    [x+i ... i i x]  Duplicate top and rotate top 3
      -}  [i-x x+i ... i]  Subtract and move to the bottom

Counting zeroes
0lMF$z+|h
0lM        Push zero (zero count) and 2**n (loop count)
   F...|   Loop 2**n times
    $z+    Swap top two; Take logical not; add to the count
        h  Print top as number and halt

```
> 0 votes

---
Tags: code-golf, math, arithmetic
---


title: Interval Notations

text:
# Question
Title: Interval Notations
## Challenge:

## Input:

Two integer parameters `a` and `b` (where `a<b` and the difference is at least 2)

## Output:

Output or return this text, where `a` and `b` are filled in:

```
(a,b) = ]a,b[ = {a<x<b}   = {a<x&&x<b}   = a+1..b-1
[a,b) = [a,b[ = {a<=x<b}  = {a<=x&&x<b}  = a..b-1
(a,b] = ]a,b] = {a<x<=b}  = {a<x&&x<=b}  = a+1..b
[a,b] = [a,b] = {a<=x<=b} = {a<=x&&x<=b} = a..b

```

## Challenge rules:

* I/O is flexible. Can be printed to STDOUT, returned as a string/character-array, etc. Can be inputted as two integers, decimals, strings (not sure why since you need to calculate the `a+1` and `b-1`, but be my guest..), etc.
* Any amount of leading and/or trailing new-lines are allowed, and any amount of trailing and/or leading spaces for each line is allowed.
* The spaces at the equal signs (including those to align them in the same column) are mandatory, spaces between the other characters are not allowed.
* `a+1` and `b-1` are replaced with the correct values after these calculations.
* You are not allowed to use  instead of `<=`.
* You are not allowed to use `&` instead of `&&`.
* You are allowed to output the numbers with `.0` (as long as it's consistent, and not more than one decimal zero).
* You can assume `a` is at least 2 lower than `b` (in order for `(a,b)` to be correct).
* The lines should be output in the order shown.

## Example:

Input: `a=-5, b=10`
Output:

```
(-5,10) = ]-5,10[ = {-5<x<10}   = {-5<x&&x<10}   = -4..9
[-5,10) = [-5,10[ = {-5<=x<10}  = {-5<=x&&x<10}  = -5..9
(-5,10] = ]-5,10] = {-5<x<=10}  = {-5<x&&x<=10}  = -4..10
[-5,10] = [-5,10] = {-5<=x<=10} = {-5<=x&&x<=10} = -5..10

```

## General rules:

* This is , so shortest answer in bytes wins.
Don't let code-golf languages discourage you from posting answers with non-codegolfing languages. Try to come up with an as short as possible answer for 'any' programming language.
* Standard rules apply for your answer, so you are allowed to use STDIN/STDOUT, functions/method with the proper parameters and return-type, full programs. Your call.
* Default Loopholes are forbidden.
* If possible, please add a link with a test for your code.
* Also, please add an explanation if necessary.

*PS: For those who had seen this challenge in the Sandbox when it was still a challenge with `a` and `b` hard-coded, I've changed it to an input challenge to prevent boring hard-coded and encoded answers like we usually see with KC challenges.*

# Answer
> 2 votes
# Stax, 74 bytes

```
ÉyU≤₧pΔz▀σ┬`♪•a≤☻Σ╕←k►¬╗Ö)ßâL╫§▐ƒ┼°╚íS3:Y¶7]7♂e╖à╙ô≥;M0h8♦Oún┼ë`←B╠╫║┌♂α▲╚

```

Run and debug it

This uses stax's string templates heavily. Unpacked, ungolfed, and commented, it looks like this.

```
Y                   save second input in Y register (first is already in X)
.)].([|*            cross product of ")]" and "(["; this produces [")(", ")[", "](", "]["]
{                   begin block to map over interval delimiters
  E"`x,`y"a++       push delimiters separately, then wrap them around the inputs    e.g. "(-5,10)"
  c"(])["|t         copy last value, then replace parentheses with braces           e.g. "]-5,10["
  ih'=              push half the iteration index and "="                           e.g. 0 "="
  |;'=              push iteration parity (alternating 0 and 1) and "="             e.g. 0 "=" 0 "="
  "{`x<`*x<`*`y}"   multiply each equal sign by its occurrence, and template        e.g. "{-5<x<10}"
  c'x.x&:mR         copy last value, then replace "x" with "x&&x"                   e.g. "{-5<x&&x<10}"
  yvih xi|e         calculate final bounds offsets                                  e.g. -5 1 10 -1
  "`+..`+"          add inputs to offsets, and embed in template                    e.g. "-4..9"
  5l                combine last 5 values into array
m                   map [")(", ")[", "](", "]["] using block
:<                  left-align grid colums to add extra spaces
m" = "*             for each row, join with " = " and output

```

Run this one

# Answer
> 10 votes
# JavaScript (ES6), ~~184~~ ~~182~~ ~~181~~ 180 bytes

Takes input in currying syntax `(a)(b)`. Returns an array of 4 strings.

```
a=>b=>[1,2,3,4].map(k=>'31,23 = 31,23 = {10x72}4{10x&&x72}45..6'.replace(/\d/g,(n,i)=>[(+n?k<3:k&1)?'<':'<=',a,b,'][)([[]('[(i*17^k*718)%9],'   = '.slice(k/2),a+k%2,b-(k<3)][n%7]))

```

Try it online!

### How?

For each row **k** with **1 ≤ k ≤ 4**, we start with the following template:

```
"31,23 = 31,23 = {10x72}4{10x&&x72}45..6"

```

and replace each decimal digit **n** at position **i** according to the following table:

```
  n  | Replaced with           | Code
-----+-------------------------+------------------------------------------
 0,7 | comparison operator     | (+n ? k < 3 : k & 1) ? '<' : '<='
  1  | a                       | a
  2  | b                       | b
  3  | interval bound          | '][)([[]('[(i * 17 ^ k * 718) % 9]
  4  | a substring of '   = '  | '   = '.slice(k / 2)
  5  | either 'a' or 'a + 1'   | a + k % 2
  6  | either 'b' or 'b - 1'   | b - (k < 3)

```

# Answer
> 4 votes
# Python 2, ~~225~~ ~~203~~ 195 bytes

```
a,b=input()
for d in 0,1:
 for m in 0,1:k=`a`+','+`b`;o='{'+`a`+'<'+m*'=';c='x<'+d*'='+`b`+'}'+'  '[m+d:];print' = '.join(['(['[m]+k+')]'[d],']['[m]+k+'[]'[d],o+c,o+'x&&'+c,`a+1-m`+'..'+`b-1+d`])

```

Try it online!

# Answer
> 4 votes
# m4, 194

Seems like a job for a macro processor. Not sure if m4 meets our standards for a programming language. It does have looping ability and arithmetic eval, so I assume its close to the mark.

```
define(l,`$1a,b$2 = $3a,b$4 = {a<$5x<$6b} $8= {a<$5x&&x<$6b} $8= $7')dnl
l(`(',`)',],[,,,incr(a)..decr(b),`  ')
l([,`)',[,[,=,,a..decr(b),` ')
l(`(',],],],,=,incr(a)..b,` ')
l([,],[,],=,=,a..b,)

```

This is my first non-trivial look at m4, so I suspect there are more golfing opportunities I've missed.

Inputs are passed using `-D` macro definitions at the command line. Not sure if anything needs to be added to the score for these, as as far as I can tell this is the only way to meaningfully pass parameters:

```
$ m4 -Da=-5 -Db=10 intnot.m4
(-5,10) = ]-5,10[ = {-5<x<10}   = {-5<x&&x<10}   = -4..9
[-5,10) = [-5,10[ = {-5<=x<10}  = {-5<=x&&x<10}  = -5..9
(-5,10] = ]-5,10] = {-5<x<=10}  = {-5<x&&x<=10}  = -4..10
[-5,10] = [-5,10] = {-5<=x<=10} = {-5<=x&&x<=10} = -5..10 $

```

Try it online.

---

Thanks @Dennis for adding m4 to TIO so quickly!

# Answer
> 3 votes
# Python 2, 187 bytes

```
t=a,b=input()
for j in 1,0:
 for i in 1,0:print"%%s%d,%d%%s = "%t*2%('[('[i],'])'[j],'[]'[i],']['[j])+"{%d<%sx%%s<%s%d}%s = "%(a,'='[i:],'='[j:],b,' '*(i+j))*2%('','&&x')+`a+i`+'..'+`b-j`

```

Try it online!

# Answer
> 3 votes
## Perl 5, 181 bytes

I thought this would have worked out a lot shorter...

```
$_="sd,ds = sd,ds = {dsxsd}s= {dsx&&xsd}s= d..d
"x4;s!s!("()][<<   [)[[<=<  (]]]<<=  [][]<=<= "=~s/[<= ]+/$&$&/gr=~/ +|<=|./g)[$-++]!ge;s/d/$F[$x%2]+{8,1,9,-1,19,-1,28,1}->{$x++}/ge

```

Try it online!

### Explanation

Originally this was using a `printf` format string, but just having `s` and `d` was shorter when combined with `s///`.

First the format string is built into `$_` and quadruplicated, then all `s`s are replaced with the corresponding bracket, `<`, `<=` or spaces, depending on the replacement index. I hoped to save some more bytes with the duplication of the last 5 chars of each block, but this only ended up saving 2 bytes. The resultant string is split up into elements of spaces, `<=` or single characters.

Finally all `d`s are replaced with the desired number which is adjusted based on the index of the current replacement via a hash key.

# Answer
> 3 votes
# JavaScript, ~~190~~ 189 bytes

```
x=>y=>`(0)7]0[7{1<x<2}  7{1<52}  73..4
[0)7[0[7{18x<26{185261..4
(0]7]0]7{1<x826{1<5=263..2
[0]7[0]7{18x82}7{185=2}71..2`.replace(/\d/g,d=>[[x,y],x,y,x+1,y-1,`x&&x<`,`}  = `,` = `,`<=`][d])

```

Try it online

# Answer
> 3 votes
# Java (JDK 10), 251 bytes

```
a->b->("(a,b)q]a,b[q{a<x<b}  q{a<x&&x<b}  q"+-~a+".."+~-b+"\n[a,b)q[a,b[q{a<=x<b} q{a<=x&&x<b} qa.."+~-b+"\n(a,b]q]a,b]q{a<x<=b} q{a<x&&x<=b} q"+-~a+"..b\n[a,b]q[a,b]q{a<=x<=b}q{a<=x&&x<=b}qa..b").replace("a",a+"").replace("b",b+"").replace("q"," = ")

```

Try it online!

## Credits

# Answer
> 2 votes
# Python 2, ~~277~~ ~~199~~ ~~193~~ 189 bytes

```
a,b=input()
for i in 4,3,2,1:x,y=i%2,i>2;e='=';p=`a`+','+`b`;print'(['[x]+p+'])'[y],e,']['[x]+p+']['[y],e,2*('{%d<%s<%s%d} %s= '%(a,e*x+'%sx',e[y:],b,i/2*' '))%('','x&&')+`a+1-x`+'..'+`b-y`

```

Try it online!

# Answer
> 1 votes
# Excel, 399 bytes

```
="("&A1&","&B1&") = ]"&A1&","&B1&"[ = {"&A1&"<x<"&B1&"}   = {"&A1&"<x&&x<"&B1&"}   = "&A1+1&".."&B1-1&"
 ["&A1&","&B1&") = ["&A1&","&B1&"[ = {"&A1&"<=x<"&B1&"}  = {"&A1&"<=x&&x<"&B1&"}  = "&A1&".."&B1-1&"
 ("&A1&","&B1&"] = ]"&A1&","&B1&"] = {"&A1&"<x<="&B1&"}  = {"&A1&"<x&&x<="&B1&"}  = "&A1+1&".."&B1&"
 ["&A1&","&B1&"] = ["&A1&","&B1&"] = {"&A1&"<=x<="&B1&"} = {"&A1&"<=x&&x<="&B1&"} = "&A1&".."&B1

```

Nothing particularly interesting here.

# Answer
> 1 votes
# Javascript, ~~273~~ ~~258~~ 232 bytes

Thanks Kevin Cruijssen for saving me 15 bytes !

```
e=>f=>'(j)h]j[h{a<x<b}  h{a<x&&x<b}  hc..d\n[j)h[j[h{a<=x<b} h{a<=x&&x<b} ha..d\n(j]h]j]h{a<x<=b} h{a<x&&x<=b} hc..b\n[j]h[j]h{a<=x<=b}h{a<=x&&x<=b}ha..b'.replace(/a|b|c|d|h|j/g,m=>{return{a:e,b:f,c:e+1,d:f-1,h:" = ",j:e+","+f}[m]})

```

Try it online

Thanks for TFeld for giving me that idea, saving around 60 bytes from my original answer.

**Ungolfed :**

```
e => f => '(j)h]j[h{a<x<b}  h{a<x&&x<b}  hc..d'
 + '\n[j)h[j[h{a<=x<b} h{a<=x&&x<b} ha..d'
 + '\n(j]h]j]h{a<x<=b} h{a<x&&x<=b} hc..b'
 + '\n[j]h[j]h{a<=x<=b}h{a<=x&&x<=b}ha..b'
.replace(/a|b|c|d|h|j/g, m=>{
        return {a:e,b:f,c:e+1,d:f-1,h:" = ",j:e+","+f}[m]
    }
)

```

---

# Javascript (original answer), 340 bytes

```
(a,b)=>alert(`(${a},${b}) = ]${a},${b}[ = {${a}<x<${b}}   = {${a}<x&&x<${b}}   = ${a+1}..${b-1}\n[${a},${b}) = [${a},${b}[ = {${a}<=x<${b}}  = {${a}<=x&&x<${b}}  = ${a}..${b-1}\n(${a},${b}] = ]${a},${b}] = {${a}<x<=${b}}  = {${a}<x&&x<=${b}}  = ${a+1}..${b}\n[${a},${b}] = [${a},${b}] = {${a}<=x<=${b}} = {${a}<=x&&x<=${b}} = ${a}..${b}\n`)

```

# Answer
> 1 votes
# C (gcc), 224 237 bytes

```
f(a,b,c,m,n,o){for(c=0;++c<5;printf("%c%d,%d%c = %c%d,%d%c = {%d<%sx<%s%d}%*s= {%d<%sx&&x<%s%d}%*s= %d..%d\n","[("[m],a,b,"])"[n],"[]"[m],a,b,"]["[n],a,"="+m,"="+n,b,o,"",a,"="+m,"="+n,b,o,"",a+m,b-n)){m=c%2;n=c<3;o=3-c/2;}}

```

Try it online!

Moving the "\<\[=\]" into the format string allowed me to remove the array altogether. Also, moving `printf()` into the `for` loop saved a semicolon.

**Original answer**

```
f(a,b,c,m,n,o){char*e[]={"<=","<"};for(c=0;++c<5;){m=c%2;n=c<3;o=3-c/2;printf("%c%d,%d%c = %c%d,%d%c = {%d%sx%s%d}%*s= {%d%sx&&x%s%d}%*s= %d..%d\n","[("[m],a,b,"])"[n],"[]"[m],a,b,"]["[n],a,e[m],e[n],b,o,"",a,e[m],e[n],b,o,"",a+m,b-n);}}

```

Try it online!

There's nothing particularly noteworthy here: I used the usual tricks for shaving the size of the function (hoisting `int` autos into the function header, using K&R style, indexing into string constants.) Storing the {"\<=","\<"} into an array proved more size-efficient than inserting a format specifier for this challenge as it was used more than once.

# Answer
> 1 votes
# Retina, 216 bytes

```
.+
$&()][<<  ¶$&[)[[<=< ¶$&(]]]<<= ¶$&[][]<=<=
((.*),(.*))(.)(.)(.)(.)(<=?)(<=?)( *)
$4$1$5 = $6$1$7 = {$2$8x$9$3}$10 = {$2$8x&&x$9$3}$10 = $2_$8..$3_$9
_<=

\d+_
$&*___
T`<`_` _+<|\.-_+<
___<
_
__<
-1
_(_*)
$.1
-0
0

```

Try it online! Explanation:

```
.+
$&()][<<  ¶$&[)[[<=< ¶$&(]]]<<= ¶$&[][]<=<=
((.*),(.*))(.)(.)(.)(.)(<=?)(<=?)( *)
$4$1$5 = $6$1$7 = {$2$8x$9$3}$10 = {$2$8x&&x$9$3}$10 = $2_$8..$3_$9

```

Build up the main bulk of the result.

```
_<=

```

If the variable is involved in a loose inequality, then the value is inclusive, so we can delete the placeholder.

```
\d+_
$&*___

```

Convert the value to unary and add 2.

```
T`<`_` _+<|\.-_+<

```

Remove the placeholder for a strict lower inequality or a negative strict upper inequality. It's still had 2 added, but 1 will be subtracted later, giving the desired result.

```
___<
_

```

Subtract 2 from the other non-zero strict inequalities, restoring the original value, from which 1 will be subtracted later.

```
__<
-1

```

Change a strict upper inequality of `0` to `-1`.

```
_(_*)
$.1

```

Subtract 1 from the remaining strict inequalities and convert to decimal.

```
-0
0

```

Fix up another edge case.

# Answer
> 1 votes
# Python 3, 180 bytes:

```
lambda a,b:[eval('f"'+"{%r[j]}{a},{b}{%r[i]} = "*2%('([',')]','][','[]')+"{{{a}<{'='[:j]}x%s<{'='[:i]}{b}}}{'  '[i+j:]} = "*2%('','&&x')+'{a+j}..{b-i}"')for i in(1,0)for j in(1,0)]

```

## explanation

Basically builds an f-string that is evaluated in a list comprehension. Old-style `%` string interpolation is used to delay evaluating the expressions until the f-string is evaluated.

```
lambda a,b:[
    eval(
      'f"' +                                                            # f-string prefix
      "{%r[j]}{a},{b}{%r[i]} = "*2%('([',')]','][','[]') +              # first two terms
      "{{{a}<{'='[:j]}x%s<{'='[:i]}{b}}}{'  '[i+j:]} = "*2%('','&&x') + # second two terms
      '{a+j}..{b-i}"'                                                   # last term
      )
    for i in(1,0)for j in(1,0)
    ]

```

The first part of the string, 'f"', will become the prefix for the f-string.

The second part of the string builds the format string for the first two interval expressions. `%r` is used to save from needing to put quotes in the format, i.e., `"{%r[j]}"` is the same as `"{'%s'[j]}"`. When the f-string is evaluated, the correct bracket is selected.

The third part of the string builds the next two interval expressions.

The last part formats the "a..b" part of the f-string.

The assembled f-string looks like: `f"{'(['[j]}{a},{b}{')]'[i]} = .... = {a+j}..{b-i}"`

When the f-string is evaluated, all the expressions in braces `{}` are are replaced by their value. So, `{a}` gets replaced by the value of `a`, and `{'(['[j]}` gets replaced by `(` if j is 0 or `[` if j is 1.

# Answer
> 1 votes
# SOGL V0.12, 110 bytes

```
<ŗŗ}”⁴
"{ŗ<ŗx³
W}↔b ,e++Κ+²
4∫2\f»¹Aa{Ƨ[(²a{Ƨ[]²ba{ =*}eο+++:³⁴;³&&x⁴a_beh+H⁶;!+ƨ.+Κο++++}⁰№Iā;0E{┼ē4=‽"δY↑æ‘┼

```

Try it Here!

# Answer
> 0 votes
# Python 3, 248 bytes

```
def f(a,b):
 l=[['(',')','[','<',1],['[',']',']','<=',0]]
 r=[0,1]
 for i in r:
  for j in r:
   print(('%s%d,%d%s='*2+'{%d%sx%s%d}={%d%sx&&x%s%d}=%d..%d')%((l[j][0],a,b,l[i][1],l[1-j][2],a,b,l[i][2])+(a,l[j][3],l[i][3],b)*2+(a+l[j][4],b-l[i][4])))

```

Try it online!

---
Tags: code-golf, string, number, integer
---