Added notes.

src/NOTES.txt

@@ -0,0 +1,34 @@
+Interm constraints
+------------------
+
+- Broadly cf. Berezin; I've already proven somewhere a similar procedure
+  terminates, as it is similar to set inclusion constraints.
+- On unif of st with non-basic variable bt, add constraint
+  (st,bt) to constraint list. Interpretation: st is always a non-tuple,
+  because we don't seek variable goals, and so we have that
+    st in unpair(bt)
+- Constraints must remain 'solvable'. Once bt becomes a non-tuple, we
+  can unify. If bt becomes a tuple, we can split the constraint into
+  two.
+- Problem: constraints destroy simple relations between realizable and
+  traces, etc. Trace generation becomes more difficult, and maybe the
+  whole 'classes' concept becomes a bit more vague, as the only clear
+  way out is to 
+- When testing for occurrence of say, terms in out(e) or in(e), we can
+  take the constaints into account. That way we can ensure that the
+  pattern is realizable in the end, if the constraints are met.
+
+Channels
+--------
+
+- Define specific channel types; go in after (a,b,[ChType,] message)
+- Auth channels: incoming recv on auth channel must come from
+  non-intruder and must match identically. Note: first-binding may be
+  violated by this; and hence 'first occurrence on this type of channel'
+  seems a better constraint.
+- Conf channels: outgoing send on conf channel may not be bound to
+  incoming node of intruder, but also taking care of avoiding tupling.
+  Hence, send(x,y) may not connect to recv(x), because that would imply
+  the intruder did the projection. These side cases need thorough
+  investigation and sane definitions in the semantics.
+