diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 80d92135a35da3f0c37c1f06e123bd4bcb0c3f25..27b84364df8b482c82b5496a360894b5f3c60728 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -8,37 +8,50 @@ open CoAlgMisc
 
 let mkRule_MultiModalK sort bs sl =
   assert (List.length sl = 1);
-  let dep f bsl =
-    assert (List.length bsl = 1);
-    let bs1 = List.hd bsl in
+  let dep f bsl =                 (* dependencies for formula f *)
+    assert (List.length bsl = 1); (* -+                 *)
+    let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
     let res = bsetMake () in
     bsetAdd res f;
-    let (role : int) = lfGetDest3 sort f in
+    let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
     let filterFkt f1 =
       if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
         && bsetMem bs1 (lfGetDest1 sort f1)
-      then bsetAdd res f1
+      then
+        (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
+        bsetAdd res f1
       else ()
     in
     bsetIter filterFkt bs;
     res
   in
   let getRules f acc =
-    if lfGetType sort f = ExF then
+    if lfGetType sort f = ExF then (* f = ∃R.C *)
       let bs1 = bsetMake () in
-      bsetAdd bs1 (lfGetDest1 sort f);
-      let (role : int) = lfGetDest3 sort f in
+      bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C }          *)
+      let (role : int) = lfGetDest3 sort f in (* role := R *)
       let filterFkt f1 =
         if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
+          (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
           bsetAdd bs1 (lfGetDest1 sort f1)
         else ()
       in
-      bsetIter filterFkt bs;
-      let s1 = List.hd sl in
+      bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
+      let s1 = List.hd sl in (* [s1] := sl *)
       let rle = (dep f, [(s1, bs1)]) in
       rle::acc
     else acc
   in
+  (* effectively:
+        mkRule_MultiModalK sort bs [s1]
+            = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
+                                     | ∀R.D ∈ bs, D ∈ bs1
+                                     }
+                , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
+                )
+              | "∃R.C" ∈ bs
+              }
+  *)
   let rules = bsetFold getRules bs [] in
   let res = ref (Some rules) in
   fun () ->
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index 6eb456acae122955c7dd73ef9ca6b394bbc56965..8b5e3015008c54c31c30892e78cffb343a551c25 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -77,10 +77,10 @@ type formulaType =
   | OrF
   | AtF
   | NomF
-  | ExF
-  | AxF
-  | ChcF
-  | FusF
+  | ExF  (* Existential / diamond *)
+  | AxF  (* Universal / box *)
+  | ChcF (* Choice *)
+  | FusF (* Fusion *)
 
 type localFormula = int
 type bset = S.bitset