Index: /trunk/Library/Generator22D.fss
===================================================================
--- /trunk/Library/Generator22D.fss (revision 3917)
+++ /trunk/Library/Generator22D.fss (revision 3919)
@@ -68,4 +68,22 @@
         rowsImpl[\ E \](g).generate[\ R \](r, body)
   end
+
+theorems[\R, L1, L2\]() =
+<|[\((ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->Boolean, (ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->R)\]
+(fn (r, q, f) => conditionAbiding[\ R, L1, L2 \](r, q, f), fn (r, q, f) => efficientImplAbiding[\ R, L1, L2 \](r, q, f))
+|>
+  
+  (*--- conditions ---*)
+  conditionAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) : Boolean = abiding(q, r)
+
+  (*--- implementation using the abide-tree reduction  *)
+  efficientImplAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) = do
+
+    (* println("Abide!") *)
+
+    (* we assume that two operators have the same lifting, i.e., L1 = L2 *)
+    r.unlift(GeneratorATWrapper(seed()).generateAT[\L1\](q, r, fn a => r.lift(f(a))))
+  end
+
 end
 
@@ -93,4 +111,22 @@
         colsImpl[\ E \](g).generate[\ R \](r, body)
   end
+
+theorems[\R, L1, L2\]() =
+<|[\((ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->Boolean, (ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->R)\]
+(fn (r, q, f) => conditionAbiding[\ R, L1, L2 \](r, q, f), fn (r, q, f) => efficientImplAbiding[\ R, L1, L2 \](r, q, f))
+|>
+  
+  (*--- conditions ---*)
+  conditionAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) : Boolean = abiding(q, r)
+
+  (*--- implementation using the abide-tree reduction  *)
+  efficientImplAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) = do
+
+    (* println("Abide!") *)
+
+    (* we assume that two operators have the same lifting, i.e., L1 = L2 *)
+    r.unlift(GeneratorATWrapper(seed()).generateAT[\L1\](r, q, fn a => r.lift(f(a))))
+  end
+
 end
 
@@ -330,5 +366,14 @@
 ) : SomeMSS2DTuple[\T\] = MSS2DTuple[\T, s0, s1\](b, n, s, e, w, ne, nw, se, nw, c, r)
 
-object MSS2DReductionAbove[\T\](op, ot) extends { AssociativeReduction[\SomeMSS2DTuple[\T\]\] }
+(* annotation for operators with the `abide' property*)
+trait AbideWith[\T\] end
+
+abiding[\R, Q\]( r : R, q : Q ) = 
+typecase(r, q) of
+  (R, AbideWith[\R\]) => true
+  else => false
+end
+
+object MSS2DReductionAbove[\T\](op, ot) extends { AssociativeReduction[\SomeMSS2DTuple[\T\]\], AbideWith[\MSS2DReductionBeside[\T\]\] }
   getter asString(): String = "MSS2DReductionAbove"
   simpleJoin(x: SomeMSS2DTuple[\T\], y: SomeMSS2DTuple[\T\]): SomeMSS2DTuple[\T\] = 
@@ -357,5 +402,5 @@
 end
 
-object MSS2DReductionBeside[\T\](op, ot) extends { AssociativeReduction[\SomeMSS2DTuple[\T\]\] }
+object MSS2DReductionBeside[\T\](op, ot) extends { AssociativeReduction[\SomeMSS2DTuple[\T\]\], AbideWith[\MSS2DReductionAbove[\T\]\] }
     getter asString(): String = "MSS2DReductionBeside"
     simpleJoin(x: SomeMSS2DTuple[\T\], y: SomeMSS2DTuple[\T\]): SomeMSS2DTuple[\T\] = 
Index: /trunk/Library/Generator22D.fsi
===================================================================
--- /trunk/Library/Generator22D.fsi (revision 3917)
+++ /trunk/Library/Generator22D.fsi (revision 3919)
@@ -79,3 +79,19 @@
 rects[\ E, nat b0, nat s0, nat b1, nat s1 \](g : Array2[\E, b0, s0, b1, s1\]) : Rects[\E, b0, s0, b1, s1\]
 
+trait AbideWith[\T\] end
+
+trait SomeMSS2DTuple[\T\] end
+
+mssBody[\T\](v:T) : SomeMSS2DTuple[\T\] 
+
+object MSS2DReductionAbove[\T\](op, ot) extends { AssociativeReduction[\SomeMSS2DTuple[\T\]\], AbideWith[\MSS2DReductionBeside[\T\]\] }
+  getter asString(): String
+  simpleJoin(x: SomeMSS2DTuple[\T\], y: SomeMSS2DTuple[\T\]): SomeMSS2DTuple[\T\]
 end
+
+object MSS2DReductionBeside[\T\](op, ot) extends { AssociativeReduction[\SomeMSS2DTuple[\T\]\], AbideWith[\MSS2DReductionAbove[\T\]\] }
+    getter asString(): String 
+    simpleJoin(x: SomeMSS2DTuple[\T\], y: SomeMSS2DTuple[\T\]): SomeMSS2DTuple[\T\] 
+end
+
+end