1. Propagation Rules

x >= max{ 0, min(D, y), -max(D,y) }
x <= max{ max(D, y), -min(D, y) } 
y >= -max(D, x) 
y <=  max(D, x) 

2. Consistency

f1: Y <= 5
f2: Z <= 5
f3: Z != 1
f4: X = Y * Z
f5: Y >= Z + 1
f6: X != 9

*: domain changed

(1)
all domain propagators are idempotent

		Q		|	f	|			D(X)			|			D(Y)			|			D(Z)			|		new
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
f1,f2,f3,f4,f5,f6		f1				[0..10]						[0..5]*						[0..10]					{f4,f5}
f2,f3,f4,f5,f6			f2				[0..10]						[0..5]						[0..5]*					{f3,f4,f5}
f3,f4,f5,f6			f3				[0..10]						[0..5]						[0, 2..5]*					{f2,f4,f5}
f4,f5,f6,f2			f4				[0, 2..6, 8..10]*				[0..5]						[0, 2..5]					{f6}
f5,f6,f2				f5				[0, 2..6, 8..10]				[1..5]*						[0, 2..4]*					{f1,f2,f3,f4}
f6,f2,f1,f3,f4			f6				[0, 2..6, 8, 10]*				[1..5]						[0, 2..4]					{f4}
f2,f1,f3,f4			f2				[0, 2..6, 8, 10]				[1..5]						[0, 2..4]					{}
f1,f3,f4				f1				[0, 2..6, 8, 10]				[1..5]						[0, 2..4]					{}
f3,f4					f3				[0, 2..6, 8, 10]				[1..5]						[0, 2..4]					{}
f4					f4				[0, 2..4, 6, 8, 10]*				[1..5]						[0, 2..4]					{f6}
f6					f6				[0, 2..4, 6, 8, 10]				[1..5]						[0, 2..4]					{}

(2)

		Q		|	f	|			D(X)			|			D(Y)			|			D(Z)			|		new
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
f1,f2,f3,f4,f5,f6		f1				[0..10]						[0..5]*						[0..10]					{f4,f5}
f2,f3,f4,f5,f6			f2				[0..10]						[0..5]						[0..5]*					{f3,f4,f5}
f3,f4,f5,f6			f3				[0..10]						[0..5]						[0..5]					{}
f4,f5,f6				f4				[0..10]						[0..5]						[0..5]					{}
f5,f6					f5				[0..10]						[1..5]*						[0..4]*					{f1,f2,f3,f4}
f6,f1,f2,f3,f4			f6				[0..10]						[1..5]						[0..4]					{}
f1,f2,f3,f4			f1				[0..10]						[1..5]						[0..4]					{}
f2,f3,f4				f2				[0..10]						[1..5]						[0..4]					{}
f3,f4					f3				[0..10]						[1..5]						[0..4]					{}
f4					f4				[0..10]						[1..5]						[0..4]					{}


3. Idempotence

No, it's not. For example, when D: D(A) = [3..17],  D(B) = [3..3],  D(C) = [1..6], 
after one run of the propagator, 
      A >= 3
      A <= 18
      B >= 3/6
      B <= 17
      C >= 3
      C <= 17/3
D becomes D': D'(A) = [3..17], D'(B) = [3..3], D'(C) = [1..5]; 
after another run of the propagator, 
      A >= 3
      A <= 15
      B >= 3/5
      B <= 17
      C >= 3
      C <= 17/3
D' becomes D'': D"(A) = [3..15], D''(B) = [3..3], D''(C) = [1..5] where D' != D'', so it is not idempotent.

4. Reification

x <= y /\ x <= z /\ (x = y \/ x = z)       <=>       x<=y, x<=z, b1 <=> x=y, b2 <=> x=z, (b1 \/ b2) 
(y <= z /\  x= y) \/ (y  >  z /\ x = z)     <=>       b3 <=> y<=z, b4 <=> x=y, b5 <=> y>z, b6 <=> x=z, b7 <=> (b3 /\ b4), b8 <=> (b5 /\ b6), (b7 \/ b8)

The first one is stronger.
You can show an example where the first one propagates but the second one doesnt, like
	D(x) = [0..10], D(y) = [0..3], D{z] = [0..5]
But then again
	D[x] = [0..10], D(y) = [1..2], D(z) = [3..5]  
will immediately set b3 = true and b5 = false in the second decomposition, 
this sets which sets b8 = false setting b7 true setting b4 true
	D[x] = [1..2]
Does the first propagate as much? Yes
x <= y makes
	D[x] = [0..2]
This makes b2 false, making b1 true which gives
        D[x] = [1..2]	

5. Alldifferent

(a) D(x) = {1}, D(y) = {3, 4, 5}, D(z) = {3, 4, 5}, D(t) = {3, 4, 5, 6, 7}, D(u) = {3, 5}, D(v) = {2}
(b) D(x) = {1}, D(y) = {3, 4, 5}, D(z) = {3, 4, 5}, D(t) = {6, 7}, D(u) = {3, 5}, D(v) = {2}


6. Cumulative

After initial bounds:
D(s1) = [0..10], D(s2) = [0..7], D(s3) = [0..6], D(s4) = [0..9], D(s5) = [0..8]

After propagation of the precedence constraints:
D(s1) = [0..5], D(s2) = [2..7], D(s3) = [0..3], D(s4) = [6..9], D(s5) = [0..8]

Compulsory part of s3 is [3..6)  (that is it starts at 3 and ends at 6)
Note that this means it is not guaranteed to use resources at time 6.

After propagation of cumulative to shift s1 backwards
D(s1) = [0..1]

s1 now has a compulsory part [1..2)

This causes 
D(s3) = [2..3]

propagation of precedence causes
D(s4) = [8..9]

Compulsory part of s3 extends to [3..8)
Compusory part of s4 becomes [9..12)

The compulsory part of s4 creates propagations
D(s2) = [2..4]
D(s5) = [0..5]

This creates compulsory part for s4 [4..7)

This moves s5 to 0 
D(s5) = {0}
and creates compulsory part for s5 [0..4)

This fixes s2 to 4
D(s4) = {4} 
and creates compulsory part for s2 [4..9)

This fixes s4 to 9
D(s4) = 9
and creates compulsory part for s5 [9..12)

There are three possible solutions
	s1 = 0, s3 = 2
	s1 = 0, s3 = 3
	s1 = 1, s3 = 3