The side conditions are understandable, but vague, and likely rule out efficient algorithms.
Perhaps this inefficient algorithm, demonstrated on your example, can be usefully encoded in Agda.

I only operate by scanning through the two input lists and the partially built output list.

as = (2 2 0 1 0) = (a0 a1 a2 a3 a4 a5)

bs = (3 3 0 0 0) = (b0 b1 b2 b3 b4 b5)

cs = (4 1 1 1 0) = (c0 c1 c2 c3 c4 c5) is the compition of "as" followed by "bs"

These permutations act on some input XS = (X0 X1 X2 X3 X4)

I note the mapping of XS after "as" and "cs" below, but this extra output is not actually needed.

**Goal: X0 will go to the first 0 in cs, find which element of cs has the first 0.**

Look for the first 0 in as, find where this goes via bs.

It is at a2.

"Scan bs for j" procedure:

So scan bs from left ot right, with parameter j starting at 2. Values greater than j
are ignored, values less than j decrement j. Value equal to j is the correct postion in cs to put
the leading 0.

Ignore b0=3, ignore b1=3, b2=0 shifts j=2-1=1, b3=0 shifts j=1-1=0, b4=0=j, so the first 0 is at c4.

This b4 implies c4, so c4 is has the first 0 in cs.

c4=0, cs = ( ? ? ? ? 0 )/( ? ? ? ? X0 ), as / ( ? ? X0 ? ? )

**Goal: Where does the X1 go?**

It will become either the first 1 before c4 or the first 0 after c4.

It comes from either the first 1 before a2, or the first 0 after a2.

Scanning as finds the first 0 after a2 at "a4".

Scanning bs as before with j=4 (from the 4 in a4):

b0=3 j=4-1=3, b1=j=3,

The b1 implies goal is c1, which will be the first 1 before c4.

c1=1, cs = ( ? 1 ? ? 0 )/( ? X1 ? ? X0 ), as / ( ? ? X0 ? X1 )

**Goal: Where does X2 go?**

It will be the first 2 before c1, the first 1 after c1 and before c4, or the first 0 after c4.

It comes from the first 2 before a2, the first 1 before 1 or the first 0 after a4.

Scanning as finds the first 2 before a2 at a0=2.

Scanning bs as before with j=0 (from the 0 in a0):

Ignore b0=3, Ignore b1=3, b2=j=0.

This b2 implies goal is c2, which will be the first 1 after c1 and before c4.

c2=1, cs = (? 1 1 ? 0 )/( ? X1 X2 ? X0), as / ( X2 ? X0 ? X1 )

**Goal: Where does X3 go?**

It will be the first 3 before c1, first 2 between c1 and c2, first 1 between c2 and c4, first 0 after c4.

It comes from first 3 before a0, first 2 between a0 and a2, first 1 between a2 and a4, first 0 after a4.

Scanning as finds the first between a0 and a2 at "a1".

Scanning bs as before with j=1 (from the 1 in a1):

Ignore b0=3, Ignore b1=3, b2=0 shifts j=1-1=0, b3=j=0.

This b3 implies goal is c3 which will be the first 1 between c2 and c4.

c3=1, cs = (? 1 1 1 0)/(? X1 X2 X3 X0), as / ( X2 X3 X0 ? X1 )

**Goal: Where does X4 go?**

It will be the first 4 before c1, first 3 between c1 & c2, first 2 between c2 and c3, first 3 between c3 and c4, first 0 after c4.

It will come from the first 4 before a0, first 3 between a0 & a1, first 2 between a1 and a2, first 1 between a2 and a4, first 0 after a4.

Scanning as finds the first 1 between a2 and a4 at "a3".

Scanning bs as before with j=3 (from the 3 in a3):

b0=j=3.

This b0 implies goal is c0 which will be the first 4 before c1.

c0=4, cs = (4 1 1 1 0)/(X4 X1 X2 X3 X0), as / ( X2 X3 X0 X4 X1 )

Done.