First commit

Signed-off-by: Mattias Andrée <maandree@kth.se>

1 files changed, 4213 insertions, 0 deletions

diff --git a/libnormalform.h b/libnormalform.h
new file mode 100644
index 0000000..ed3b256
--- /dev/null
+++ b/libnormalform.h
@@ -0,0 +1,4213 @@
+/* See LICENSE file for copyright and license details. */
+#ifndef LIBNORMALFORM_H
+#define LIBNORMALFORM_H
+
+#include <stdarg.h>
+#include <stddef.h>
+#include <stdint.h>
+
+
+#if defined(__GNUC__)
+# pragma GCC diagnostic push
+# pragma GCC diagnostic ignored "-Winline"
+#endif
+
+
+/* For internal use { */
+
+#if defined(__GNUC__)
+# define LIBNORMALFORM_USE_RESULT__ __attribute__((__warn_unused_result__))
+# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR)))
+# define LIBNORMALFORM_USE_FREE__ __attribute__((__malloc__))
+# define LIBNORMALFORM_NONNULL_INPUT__ __attribute__((__nonnull__))
+# define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX) __attribute__((__nonnull__(INDEX)))
+# if defined(LIBNORMALFORM_ALLOW_BAD_WARNINGS)
+#  define LIBNORMALFORM_NULL_LAST__ __attribute__((__sentinel__))
+# else
+#  define LIBNORMALFORM_NULL_LAST__
+# endif
+/*
+ * Unfortunately __attribute__((__sentinel__)) requires (in contrary to the
+ * documentation) the `NULL` to be inside `...`, and not at the argument before
+ * the `...`, so a "-Wformat=" warning will be generated if and empty list is
+ * used when constructing a sentence. Therefore, by default this attribute is
+ * not used, as the user may have configured the compiler to fail if the warning
+ * is generated.
+ */
+#else
+# define LIBNORMALFORM_USE_RESULT__
+# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR)
+# define LIBNORMALFORM_USE_FREE__
+# define LIBNORMALFORM_NONNULL_INPUT__
+# define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX)
+# define LIBNORMALFORM_NULL_LAST__
+#endif
+
+
+#define LIBNORMALFORM_CHECKED__(CONNECTIVE)\
+	size_t i__ = 0;\
+	while (xs[i__])\
+		i__ += 1;\
+	if (i__ < n) {\
+		while (n--)\
+			libnormalform_free(xs[n]);\
+		return NULL;\
+	}\
+	return libnormalform_##CONNECTIVE(xs);
+
+#define LIBNORMALFORM_VALIST__(CONNECTIVE)\
+	size_t n__ = 0, i__ = 0;\
+	va_list args2__;\
+	va_copy(args2__, args);\
+	if (a) {\
+		do {\
+			n__ += 1;\
+		} while (va_arg(args2__, LIBNORMALFORM_SENTENCE *));\
+	}\
+	va_end(args2__);\
+	{\
+		LIBNORMALFORM_SENTENCE *xs[n__ + 1U];\
+		if (n__) {\
+			xs[i__++] = a;\
+			while (--n__)\
+				xs[i__++] = va_arg(args, LIBNORMALFORM_SENTENCE *);\
+		}\
+		xs[i__] = NULL;\
+		return libnormalform_##CONNECTIVE(xs);\
+	}
+
+#define LIBNORMALFORM_ELLIPSIS__(CONNECTIVE)\
+	LIBNORMALFORM_SENTENCE *ret__;\
+	va_list args__;\
+	va_start(args__, a);\
+	ret__ = libnormalform_v##CONNECTIVE(a, args__);\
+	va_end(args__);\
+	return ret__;
+
+#define LIBNORMALFORM_VALIST_CHECKED__(CONNECTIVE)\
+	size_t n__ = 0, i__ = 0;\
+	va_list args2__;\
+	va_copy(args2__, args);\
+	if (a) {\
+		do {\
+			n__ += 1;\
+		} while (va_arg(args2__, LIBNORMALFORM_SENTENCE *));\
+	}\
+	va_end(args2__);\
+	if (n__ < n) {\
+		if (n) {\
+			libnormalform_free(a);\
+			while (--n)\
+				libnormalform_free(va_arg(args2__, LIBNORMALFORM_SENTENCE *));\
+		}\
+		return NULL;\
+	}\
+	{\
+		LIBNORMALFORM_SENTENCE *xs__[n__ + 1U];\
+		if (n__) {\
+			xs__[i__++] = a;\
+			while (--n__)\
+				xs__[i__++] = va_arg(args, LIBNORMALFORM_SENTENCE *);\
+		}\
+		xs__[i__] = NULL;\
+		return libnormalform_##CONNECTIVE(xs__);\
+	}
+
+#define LIBNORMALFORM_ELLIPSIS_CHECKED__(CONNECTIVE)\
+	LIBNORMALFORM_SENTENCE *ret__;\
+	va_list args__;\
+	va_start(args__, a);\
+	ret__ = libnormalform_v##CONNECTIVE##_checked(n, a, args__);\
+	va_end(args__);\
+	return ret__;
+
+#define LIBNORMALFORM_TWO__(CONNECTIVE)\
+	LIBNORMALFORM_SENTENCE *xs__[3] = {l, r, NULL};\
+	if (!l || !r) {\
+		libnormalform_free(l);\
+		libnormalform_free(r);\
+		return NULL;\
+	}\
+	return libnormalform_##CONNECTIVE(xs__);
+
+#define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
+	(libnormalform_##CONNECTIVE##_checked(\
+		sizeof((LIBNORMALFORM_SENTENCE *[]){__VA_OPT__(__VA_ARGS__,) NULL}) / sizeof(LIBNORMALFORM_SENTENCE *) - 1U,\
+		(LIBNORMALFORM_SENTENCE *[]){__VA_OPT__(__VA_ARGS__,) NULL}))
+
+/* } */
+
+
+struct libnormalform_term;
+
+
+
+
+
+#define LIBNORMALFORM_AVOID_FOR_ALL                 (UINT64_C(1) <<  0) /**< Prefer ¬∃x.¬φ over ∀x.φ */
+#define LIBNORMALFORM_AVOID_NEGATED_FOR_ALL         (UINT64_C(1) <<  1) /**< Prefer  ∃x.¬φ over ¬∀x.φ */
+#define LIBNORMALFORM_AVOID_FOR_ANY                 (UINT64_C(1) <<  2) /**< Prefer ¬∀x.¬φ over ∃x.φ */
+#define LIBNORMALFORM_AVOID_NEGATED_FOR_ANY         (UINT64_C(1) <<  3) /**< Prefer  ∀x.¬φ over ¬∃x.φ */
+#define LIBNORMALFORM_RELAX_FOR_ONE                 (UINT64_C(1) <<  4) /**< Relax any positive ∃!x.φ into ∃x.φ */
+#define LIBNORMALFORM_REDUCE_XOR                    (UINT64_C(1) <<  5) /**< Rewrite XOR to negation normal form */
+#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL         (UINT64_C(1) <<  6) /**< Express   φ(x)∀x:θ(x)   on the form  ∀x.(θ(x) → φ(x)) */
+#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL (UINT64_C(1) <<  7) /**< Express ¬(φ(x)∀x:θ(x))  on the form ¬∀x.(θ(x) → φ(x)) */
+#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY         (UINT64_C(1) <<  8) /**< Express   φ(x)∃x:θ(x)   on the form  ∃x.(θ(x) ∧ φ(x)) */
+#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY (UINT64_C(1) <<  9) /**< Express ¬(φ(x)∃x:θ(x))  on the form ¬∃x.(θ(x) ∧ φ(x)) */
+#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE         (UINT64_C(1) << 10) /**< Express   φ(x)∃!x:θ(x)  on the form  ∃!x.(θ(x) ∧ φ(x)) */
+#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE (UINT64_C(1) << 11) /**< Express ¬(φ(x)∃!x:θ(x)) on the form ¬∃!x.(θ(x) ∧ φ(x)) */
+#define LIBNORMALFORM_ELIMINATE_FOR_ALL             (UINT64_C(1) << 12) /**< Relax any non-translatable  ∀x.φ to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL     (UINT64_C(1) << 13) /**< Relax any non-translatable ¬∀x.φ to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_FOR_ANY             (UINT64_C(1) << 14) /**< Relax any non-translatable  ∃x.φ to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY     (UINT64_C(1) << 15) /**< Relax any non-translatable ¬∃x.φ to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_FOR_ONE             (UINT64_C(1) << 16) /**< Relax any non-translatable ∃!x.φ to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE     (UINT64_C(1) << 17) /**< Relax any ¬∃!x.φ to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_VARIABLE            (UINT64_C(1) << 18) /**< Relax any positive variable literal to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE    (UINT64_C(1) << 19) /**< Relax any negative variable literal to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_FUNCTION            (UINT64_C(1) << 20) /**< Relax any positive function literal to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION    (UINT64_C(1) << 21) /**< Relax any negative function literal to ⊤ */
+#define LIBNORMALFORM_ELIMINATE_XOR                 (UINT64_C(1) << 22) /**< Relax any non-reduce XOR to ⊤ */
+#define LIBNORMALFORM_ALL_EXPRESS_FLAGS__          ((UINT64_C(1) << 23) - 1U) /* For internal use */
+
+
+/**
+ * Opaque data type use to express and sentences
+ *
+ * This object incluses caches and preallocated memory
+ * makes object unsafe to be used from two different
+ * threads at the same time
+ *
+ * @seealso  libnormalform_clone
+ */
+typedef struct libnormalform_sentence LIBNORMALFORM_SENTENCE;
+
+
+/**
+ * Specification for how application provided strings
+ * shall be interpreted
+ */
+struct libnormalform_representation_spec {
+	/**
+	 * Application-specific data that will be passed into
+	 * `.get_variable`, `.get_function`, `.get_map`, and
+	 * `.get_transformer` (making it reenterant so it can be
+	 * called by multiple threads, or to configure the function)
+	 * 
+	 * May be `NULL`
+	 */
+	void *user_data;
+
+	/**
+	 * Deserialise a variable from a unterminated string
+	 * 
+	 * The function shall be able to return the reference
+	 * to any `struct libnormalform_variable` given its
+	 * `.identifier` sans NUL-termination
+	 * 
+	 * The function shall be pure in the sence that if
+	 * it is called twice (or more) with the identifer
+	 * at the beginning of `s` it shall return the same
+	 * pointer, not two different copies (`user_data` be
+	 * use used to store the variables if they are
+	 * constructed dynamically)
+	 * 
+	 * May be `NULL`
+	 * 
+	 * @param   s           The string beginning with the variable's
+	 *                      identifier
+	 * @param   end_out     Output parameter for the position in
+	 *                      `s` after the last byte in the identifer
+	 * @param   user_data   `.user_data`
+	 * @return              A pointer to the referenced variable, `NULL`
+	 *                      on failure (`errno` may be set)
+	 * 
+	 * It is recommended that, on failure, `errno` is set
+	 * according to the below specification, however it is
+	 * up to the application to choose what to do with `errno`
+	 * 
+	 * @throws  EINVAL  `s` in not formatted to represent a valid variable
+	 * @throws  ENOENT  `s` does not represent any known variable
+	 */
+	struct libnormalform_variable *(*get_variable)(char *s, char **end_out, void *user_data);
+
+	/**
+	 * Same as `.get_variable` except that it returns
+	 * reference to a function (`struct libnormalform_function *`)
+	 */
+	struct libnormalform_function *(*get_function)(char *s, char **end_out, void *user_data);
+
+	/**
+	 * Same as `.get_variable` except that it returns
+	 * reference to a domain (`struct libnormalform_map *`)
+	 */
+	struct libnormalform_map *(*get_map)(char *s, char **end_out, void *user_data);
+
+	/**
+	 * Same as `.get_transformer` except that it returns
+	 * reference to a function (`struct libnormalform_transformer *`)
+	 */
+	struct libnormalform_transformer *(*get_transformer)(char *s, char **end_out, void *user_data);
+};
+
+
+/**
+ * Type if a `struct libnormalform_term`, used to
+ * determine which member of `.term` to use and
+ * whether it is negated
+ */
+enum libnormalform_term_type {
+	LIBNORMALFORM_CONJUNCTION,            /**< AND clause; empty clause is used for contradiction */
+	LIBNORMALFORM_DISJUNCTION,            /**< OR  clause; empty clause is used for tautology */
+	LIBNORMALFORM_EXCLUSIVE_DISJUNCTION,  /**< XOR clause; never used for empty clauses */
+	LIBNORMALFORM_TRANSFORMATION,         /**< Transformater function with input **/
+	LIBNORMALFORM_VARIABLE,               /**< Positive variable literal **/
+	LIBNORMALFORM_NEGATED_VARIABLE,       /**< Negative variable literal **/
+	LIBNORMALFORM_FUNCTION,               /**< Positive boolean function literal **/
+	LIBNORMALFORM_NEGATED_FUNCTION,       /**< Negative boolean function literal **/
+	LIBNORMALFORM_FOR_ALL,                /**<  ∀x∈D.(P(x) → Q(x)) expression */
+	LIBNORMALFORM_NEGATED_FOR_ALL,        /**< ¬∀x∈D.(P(x) → Q(x)) expression */
+	LIBNORMALFORM_FOR_ANY,                /**<  ∃x∈D.(P(x) ∧ Q(x)) expression */
+	LIBNORMALFORM_NEGATED_FOR_ANY,        /**< ¬∃x∈D.(P(x) ∧ Q(x)) expression */
+	LIBNORMALFORM_FOR_ONE,                /**<  ∃!x∈D.(P(x) ∧ Q(x)) expression */
+	LIBNORMALFORM_NEGATED_FOR_ONE         /**< ¬∃!x∈D.(P(x) ∧ Q(x)) expression */
+};
+
+
+/**
+ * Value of an atomic sentence
+ */
+enum libnormalform_value {
+	LIBNORMALFORM_FALSE = 0,  /**< Variable has the value False */
+	LIBNORMALFORM_TRUE = 1    /**< Variable has the value True */
+};
+
+
+/**
+ * Built in transformer functions
+ */
+enum libnormalform_builtin_transformer {
+	LIBNORMALFORM_NOT_BUILT_IN = 0,  /**< Application provided transformer */
+	LIBNORMALFORM_DOMAIN_VIEW,   /**< Selects the `.key` from a `struct libnormalform_mapping *` */
+	LIBNORMALFORM_IMAGE_VIEW     /**< Selects the `.value` from a `struct libnormalform_mapping *` */
+};
+
+
+/**
+ * Relationship (dependency) between the value of two sentences
+ */
+enum libnormalform_sentences_relationship {
+	/**
+	 * Left-hand implies right-hand (⊨ P → Q)
+	 * 
+	 * Example:
+	 * -  P = ⋀{a, b}, Q = ⋀{a}
+	 * 
+	 * Truthtable:
+	 *    P: 001
+	 *    Q: 011
+	 *    ∧: 001
+	 *    ∨: 011
+	 *    ⊕: 010
+	 *    →: 111
+	 *    ←: 101
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q = P
+	 * -  P ∨ Q = Q
+	 * -  P ⊕ Q = ¬P ∧ Q
+	 * -  P → Q = ⊤
+	 * -  P ← Q cannot be simplified
+	 */
+	LIBNORMALFORM_MATERIAL_IMPLICATION = -1,
+
+	/**
+	 * The terms are identical (⊨ P ↔ Q)
+	 * 
+	 * Example:
+	 * -  P = ⋀{a, b}, Q = ⋀{a, b}
+	 * 
+	 * Truthtable:
+	 *    P: 01
+	 *    Q: 01
+	 *    ∧: 01
+	 *    ∨: 01
+	 *    ⊕: 00
+	 *    →: 11
+	 *    ←: 11
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q = P = Q
+	 * -  P ∨ Q = P = Q
+	 * -  P ⊕ Q = ⊥
+	 * -  P → Q = ⊤
+	 * -  P ← Q = ⊤
+	 */
+	LIBNORMALFORM_IDENTICAL,
+
+	/**
+	 * Right-hand implies left-hand (⊨ P ← Q)
+	 * 
+	 * Example:
+	 * -  P = ⋀{a}, Q = ⋀{a, b}
+	 * 
+	 * Truthtable:
+	 *    P: 011
+	 *    Q: 001
+	 *    ∧: 001
+	 *    ∨: 011
+	 *    ⊕: 010
+	 *    →: 101
+	 *    ←: 111
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q = Q
+	 * -  P ∨ Q = P
+	 * -  P ⊕ Q = P ∧ ¬Q
+	 * -  P → Q cannot be simplified
+	 * -  P ← Q = ⊤
+	 */
+	LIBNORMALFORM_CONVERSE_IMPLICATION,
+
+	/**
+	 * The terms are the inverse of each other (⊨ P ↮ Q)
+	 * 
+	 * Example:
+	 * -  P = a, Q = ¬a
+	 * 
+	 * Truthtable:
+	 *    P: 01
+	 *    Q: 10
+	 *    ∧: 00
+	 *    ∨: 11
+	 *    ⊕: 11
+	 *    →: 10
+	 *    ←: 01
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q = ⊥
+	 * -  P ∨ Q = ⊤
+	 * -  P ⊕ Q = ⊤
+	 * -  P → Q = Q
+	 * -  P ← Q = P
+	 */
+	LIBNORMALFORM_MUTUALLY_INVERSE,
+
+	/**
+	 * Both terms cannot be satisfied at the same time,
+	 * but are not each other's inverse (⊨ P ⊼ Q)
+	 * 
+	 * Example:
+	 * -  P = ⋀{a, b}, Q = ⋀{¬b}
+	 * 
+	 * Truthtable:
+	 *    P: 001
+	 *    Q: 010
+	 *    ∧: 000
+	 *    ∨: 011
+	 *    ⊕: 011
+	 *    →: 110
+	 *    ←: 101
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q = ⊥
+	 * -  P ∨ Q cannot be simplified
+	 * -  P ⊕ Q = P ∨ Q
+	 * -  P → Q = ¬P
+	 * -  P ← Q = ¬Q
+	 */
+	LIBNORMALFORM_MUTUALLY_EXCLUSIVE,
+
+	/**
+	 * The terms cannot be unsatisfied at the same time,
+	 * but they are not identical (⊨ P ∨ Q)
+	 * 
+	 * Example:
+	 * -  P = ⋁{a, b}, Q = ⋁{¬b}
+	 * 
+	 * Truthtable:
+	 *    P: 011
+	 *    Q: 101
+	 *    ∧: 001
+	 *    ∨: 111
+	 *    ⊕: 110
+	 *    →: 101
+	 *    ←: 011
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q cannot be simplified
+	 * -  P ∨ Q = ⊤
+	 * -  P ⊕ Q = ¬P ∨ ¬Q
+	 * -  P → Q = Q
+	 * -  P ← Q = P
+	 */
+	LIBNORMALFORM_JOINTLY_UNDENIABLE,
+
+	/**
+	 * The terms are unrelated to each other
+	 * 
+	 * Example:
+	 * -  P = a, Q = b
+	 * 
+	 * Truthtable:
+	 *    P: 0011
+	 *    Q: 0101
+	 *    ∧: 0001
+	 *    ∨: 0111
+	 *    ⊕: 0110
+	 *    →: 1101
+	 *    ←: 1011
+	 * 
+	 * Consequence:
+	 * -  P ∧ Q cannot be simplified
+	 * -  P ∨ Q cannot be simplified
+	 * -  P ⊕ Q cannot be simplified
+	 * -  P → Q cannot be simplified
+	 * -  P ← Q cannot be simplified
+	 */
+	LIBNORMALFORM_MUTUALLY_INDEPENDENT
+};
+
+
+
+/**
+ * Relationship (commonality) between the value of two domains
+ *
+ * (The documentation uses the term "set", however,
+ * properly they are bags (multisets), however this
+ * is only important for uniqueness qualification;
+ * for the mathematics, you can thing about it as
+ * sets)
+ */
+enum libnormalform_domain_relationship {
+	/**
+	 * The left-hand set is a superset of the right-hand set (A ⊇ B)
+	 * 
+	 * Example:
+	 * -  A = {a, b}, B = {a}
+	 * 
+	 * Euler diagram:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A────────────────┐      │
+	 *    │  │╱╱╱╱╱╱╱┌─B──────┐╱│      │
+	 *    │  │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│      │
+	 *    │  │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│      │
+	 *    │  │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│      │
+	 *    │  │╱╱╱╱╱╱╱└────────┘╱│      │
+	 *    │  │╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱│      │
+	 *    │  └──────────────────┘      │
+	 *    └────────────────────────────┘
+	 * 
+	 * Venn diagram of possibly non-empty intersections:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A─────────────┐         │
+	 *    │  │███████████████│         │
+	 *    │  │██████┌────────┼──────┐  │
+	 *    │  │██████│████████│      │  │
+	 *    │  │██████│████████│      │  │
+	 *    │  └──────┼────────┘      │  │
+	 *    │         │               │  │
+	 *    │         └─────────────B─┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Consequence:
+	 * -  A ∩ B = B
+	 * -  A ∪ B = A
+	 * -  A ∆ B = A ∖ B
+	 * -  ⋀A ⊨ ⋀B
+	 * -  ⋁B ⊨ ⋁A
+	 * -  ⋀A ∧ ⋀B = ⋀A
+	 * -  ⋀A ∨ ⋀B = ⋀B
+	 * -  ⋀A ⊕ ⋀B = ¬⋀A ∧ ⋀B
+         * -  ⋀A → ⋀B = ⊤
+	 * -  ⋀A ← ⋀B cannot be simplified
+	 * -  ⋁A ∧ ⋁B = ⋁B
+	 * -  ⋁A ∨ ⋁B = ⋁A
+	 * -  ⋁A ⊕ ⋁B = ⋁A ∧ ¬⋁B
+         * -  ⋁A → ⋁B cannot be simplified
+	 * -  ⋁A ← ⋁B = ⊤
+	 */
+	LIBNORMALFORM_SUPERSET_OF = -1,
+
+	/**
+	 * The two terms are identical (A = B)
+	 * 
+	 * Example:
+	 * -  A = {a, b}, B = {a, b}
+	 * 
+	 * Euler diagram:
+	 *    ┌────────────────────────────┐
+	 *    │    ┌─A,B──────────────┐    │
+	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
+	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
+	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
+	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
+	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
+	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
+	 *    │    └──────────────────┘    │
+	 *    └────────────────────────────┘
+	 * 
+	 * Venn diagram of possibly non-empty intersections:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A─────────────┐         │
+	 *    │  │               │         │
+	 *    │  │      ┌────────┼──────┐  │
+	 *    │  │      │████████│      │  │
+	 *    │  │      │████████│      │  │
+	 *    │  └──────┼────────┘      │  │
+	 *    │         │               │  │
+	 *    │         └─────────────B─┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Consequence:
+	 * -  A ∩ B = A = B
+	 * -  A ∪ B = A = B
+	 * -  A ∆ B = ∅
+	 * -  ⋀A = ⋀B
+	 * -  ⋁A = ⋁B
+	 * -  ⋀A ∧ ⋀B = ⋀A = ⋀B
+	 * -  ⋀A ∨ ⋀B = ⋀A = ⋀B
+	 * -  ⋀A ⊕ ⋀B = ⊥
+         * -  ⋀A → ⋀B = ⊤
+	 * -  ⋀A ← ⋀B = ⊤
+	 * -  ⋁A ∧ ⋁B = ⋁A = ⋁B
+	 * -  ⋁A ∨ ⋁B = ⋁A = ⋁B
+	 * -  ⋁A ⊕ ⋁B = ⊥
+         * -  ⋁A → ⋁B = ⊤
+	 * -  ⋁A ← ⋁B = ⊤
+	 */
+	LIBNORMALFORM_SAME_AS,
+
+	/**
+	 * The left-hand set is a subset of the right-hand set (A ⊆ B)
+	 * 
+	 * Example:
+	 * -  A = {a}, B = {a, b}
+	 * 
+	 * Euler diagram:
+	 *    ┌────────────────────────────┐
+	 *    │      ┌─B────────────────┐  │
+	 *    │      │╲┌─A──────┐╲╲╲╲╲╲╲│  │
+	 *    │      │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│  │
+	 *    │      │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│  │
+	 *    │      │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│  │
+	 *    │      │╲└────────┘╲╲╲╲╲╲╲│  │
+	 *    │      │╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲│  │
+	 *    │      └──────────────────┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Venn diagram of possibly non-empty intersections:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A─────────────┐         │
+	 *    │  │               │         │
+	 *    │  │      ┌────────┼──────┐  │
+	 *    │  │      │████████│██████│  │
+	 *    │  │      │████████│██████│  │
+	 *    │  └──────┼────────┘██████│  │
+	 *    │         │███████████████│  │
+	 *    │         └─────────────B─┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Consequence:
+	 * -  A ∩ B = A
+	 * -  A ∪ B = B
+	 * -  A ∆ B = B ∖ A
+	 * -  ⋀B ⊨ ⋀A
+	 * -  ⋁A ⊨ ⋁B
+	 * -  ⋀A ∧ ⋀B = ⋀B
+	 * -  ⋀A ∨ ⋀B = ⋀A
+	 * -  ⋀A ⊕ ⋀B = ⋀A ∧ ¬⋀B
+         * -  ⋀A → ⋀B cannot be simplified
+	 * -  ⋀A ← ⋀B = ⊤
+	 * -  ⋁A ∧ ⋁B = ⋁A
+	 * -  ⋁A ∨ ⋁B = ⋁B
+	 * -  ⋁A ⊕ ⋁B = ¬⋁A ∧ ⋁B
+         * -  ⋁A → ⋁B = ⊤
+	 * -  ⋁A ← ⋁B cannot be simplified
+	 */
+	LIBNORMALFORM_SUBSET_OF,
+
+	/**
+	 * The sets have no common elements (A ∩ B = ∅)
+	 * 
+	 * Example:
+	 * -  A = {a}, B = {b}
+	 * 
+	 * Euler diagram:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A───────┐  ┌─B───────┐  │
+	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
+	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
+	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
+	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
+	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
+	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
+	 *    │  └─────────┘  └─────────┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Venn diagram of possibly non-empty intersections:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A─────────────┐         │
+	 *    │  │███████████████│         │
+	 *    │  │██████┌────────┼──────┐  │
+	 *    │  │██████│        │██████│  │
+	 *    │  │██████│        │██████│  │
+	 *    │  └──────┼────────┘██████│  │
+	 *    │         │███████████████│  │
+	 *    │         └─────────────B─┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Consequence:
+	 * -  A ∩ B = ∅
+	 * -  A ∪ B cannot be simplified
+	 * -  A ∆ B = A ∪ B
+	 * -  ⋀A ∧ ⋀B = ⋀(A ∪ B)
+	 * -  ⋀A ∨ ⋀B cannot be simplified
+	 * -  ⋀A ⊕ ⋀B cannot be simplified
+         * -  ⋀A → ⋀B cannot be simplified
+	 * -  ⋀A ← ⋀B cannot be simplified
+	 * -  ⋁A ∧ ⋁B cannot be simplified
+	 * -  ⋁A ∨ ⋁B = ⋁(A ∪ B)
+	 * -  ⋁A ⊕ ⋁B cannot be simplified
+         * -  ⋁A → ⋁B cannot be simplified
+	 * -  ⋁A ← ⋁B cannot be simplified
+	 */
+	LIBNORMALFORM_DISJOINT_WITH,
+
+	/**
+	 * Both sets have unique elements (A ⊆ A ∪ B ⊇ B, A ∩ B ⊇ ∅)
+	 * 
+	 * Example:
+	 * -  A = {a, b}, B = {b, c}
+	 * 
+	 * Euler diagram:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A─────────────┐         │
+	 *    │  │╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱│         │
+	 *    │  │╱╱╱╱╱╱┌────────┼────B─┐  │
+	 *    │  │╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲│  │
+	 *    │  │╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲│  │
+	 *    │  └──────┼────────┘╲╲╲╲╲╲│  │
+	 *    │         │╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲│  │
+	 *    │         └───────────────┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Venn diagram of possibly non-empty intersections:
+	 *    ┌────────────────────────────┐
+	 *    │  ┌─A─────────────┐         │
+	 *    │  │███████████████│         │
+	 *    │  │██████┌────────┼──────┐  │
+	 *    │  │██████│████████│██████│  │
+	 *    │  │██████│████████│██████│  │
+	 *    │  └──────┼────────┘██████│  │
+	 *    │         │███████████████│  │
+	 *    │         └─────────────B─┘  │
+	 *    └────────────────────────────┘
+	 * 
+	 * Consequence:
+	 * -  A ∩ B cannot be simplified
+	 * -  A ∪ B cannot be simplified
+	 * -  A ∆ B cannot be simplified
+	 * -  ⋀A ∧ ⋀B = ⋀(A ∪ B)
+	 * -  ⋀A ∨ ⋀B cannot be simplified
+	 * -  ⋀A ⊕ ⋀B cannot be simplified
+         * -  ⋀A → ⋀B cannot be simplified
+	 * -  ⋀A ← ⋀B cannot be simplified
+	 * -  ⋁A ∧ ⋁B cannot be simplified
+	 * -  ⋁A ∨ ⋁B = ⋁(A ∪ B)
+	 * -  ⋁A ⊕ ⋁B cannot be simplified
+         * -  ⋁A → ⋁B cannot be simplified
+	 * -  ⋁A ← ⋁B cannot be simplified
+	 */
+	LIBNORMALFORM_CONJOINT_WITH
+};
+
+
+/**
+ * Variable that can be referenced in a sentence
+ */
+struct libnormalform_variable {
+	/**
+	 * The value of the sentence
+	 *
+	 * This need not be sent when the sentence is constructed,
+	 * but not be set before it is evaluated; it is only used
+	 * by `libnormalform_evaluate`
+	 */
+	enum libnormalform_value value;
+
+	/**
+	 * Application-specific data that the application
+	 * could use to identify the variable
+	 * 
+	 * May be `NULL`
+	 */
+	void *user_data;
+
+	/**
+	 * Identifier for variable
+	 *
+	 * This need only be set when `libnormalform_to_string`
+	 * is called. The value must be parsable by the application
+	 * without any explicit termination
+	 */
+	const char *identifier;
+
+	/**
+	 * `NULL` or copy of of the object for `libnormalform_clone`
+	 * 
+	 * This field should normally be unset, but before calling
+	 * `libnormalform_clone`, the application must set it
+	 * either to `NULL` (if the clone can use the same reference)
+	 * or to a clone of the variable.
+	 */
+	struct libnormalform_variable *copy_for_clone;
+};
+
+
+/**
+ * Boolean-codomain function that can be referenced in a sentence
+ */
+struct libnormalform_function {
+	/**
+	 * Function that is used to evaluate the trueness of something
+	 * 
+	 * @param   user_data  `.user_data`
+	 * @param   input      Input to the function, normally it will
+	 *                     be `NULL`, but it is inside the antecedent
+	 *                     for a qualifier, it will be the `.key`
+	 *                     for some `struct libnormalform_mapping`,
+	 *                     and if it is inside the predicate of a
+	 *                     qualifier, it will be the `.value`
+	 *                     for some `struct libnormalform_mapping`
+	 * @return             1 if the function is true,
+	 *                     0 if the function is false,
+	 *                     -1 on failure (the function may set `errno`)
+	 * 
+	 * For `libnormalform_exists`, `libnormalform_nexists`,
+	 * and `libnormalform_unique`, it will only be called
+	 * for the `.key` for `struct libnormalform_mapping`'s
+	 * 
+	 * For `libnormalform_universally`, `libnormalform_existentially`,
+	 * and `libnormalform_uniquely`, it will only be called
+	 * for the `.value` for `struct libnormalform_mapping`'s
+	 */
+	int (*evaluate)(void *user_data, void *input);
+
+	/**
+	 * Application-specific data that will be passed into
+	 * `.evaluate` (making it reenterant so it can be called
+	 * by multiple threads, or to configure the function)
+	 * 
+	 * May be `NULL`
+	 */
+	void *user_data;
+
+	/**
+	 * Identifier for function
+	 *
+	 * This need only be set when `libnormalform_to_string`
+	 * is called. The value must be parsable by the application
+	 * without any explicit termination
+	 */
+	const char *identifier;
+
+	/**
+	 * `NULL` or copy of of the object for `libnormalform_clone`
+	 * 
+	 * This field should normally be unset, but before calling
+	 * `libnormalform_clone`, the application must set it
+	 * either to `NULL` (if the clone can use the same reference)
+	 * or to a clone of the variable.
+	 */
+	struct libnormalform_function *copy_for_clone;
+
+	/**
+	 * See `.requires_relaxation`
+	 */
+	struct libnormalform_function *relaxation;
+
+	/**
+	 * Before calling `libnormalform_express`, `libnormalform_dnf`,
+	 * or `libnormalform_cnf` this shall be set to 0 if the function
+	 * may keep the function as is, or to a non-0 value if it shall
+	 * be replaced `.relaxation` or by TRUE if `.relaxation` is `NULL`
+	 */
+	int requires_relaxation;
+};
+
+
+/**
+ * Generic function that can be referenced in a sentence
+ * 
+ * The function must be pure and distributive over any boolean operator
+ * (it must be an endomorphism). That is, the output is always the
+ * same for the same input without any side effects, and for any sentence
+ * A * B, where * is any boolean operator and F is the function,
+ * F(A * B) = F(A) * F(B).
+ */
+struct libnormalform_transformer {
+	/**
+	 * Function that is used to transform input
+	 * 
+	 * @param   user_data  `.user_data`
+	 * @param   input      Input to the function, normally it will
+	 *                     be `NULL`, but it is inside the antecedent
+	 *                     for a qualifier, it will be the `.key`
+	 *                     for some `struct libnormalform_mapping`,
+	 *                     and if it is inside the predicate of a
+	 *                     qualifier, it will be the `.value`
+	 *                     for some `struct libnormalform_mapping`,
+	 *                     except that during the create of a
+	 *                     `struct libnormalform_term`, the library
+	 *                     may insert builtin transformers that will
+	 *                     have the `struct libnormalform_mapping *`
+	 *                     as input and will output the `.key` or
+	 *                     `.value`
+	 * @return             The transformation of `input` (not `NULL`),
+	 *                     `NULL` on failure (the function may set `errno`)
+	 * 
+	 * For `libnormalform_exists`, `libnormalform_nexists`,
+	 * and `libnormalform_unique`, it will only be called
+	 * for the `.key` for `struct libnormalform_mapping`'s
+	 * 
+	 * For `libnormalform_universally`, `libnormalform_existentially`,
+	 * and `libnormalform_uniquely`, it will only be called
+	 * for the `.value` for `struct libnormalform_mapping`'s
+	 */
+	void *(*transform)(void *user_data, void *input);
+
+	/**
+	 * The function is called when the output of `.transform`
+	 * is not longer needed by the library
+	 * 
+	 * May be `NULL`
+	 * 
+	 * This function is not called if `.transform` output `NULL`
+	 * 
+	 * @param  user_data  `.user_data`
+	 * @param  output     The pointer that was returned by `.transform`
+	 */
+	void (*deallocate)(void *user_data, void *output);
+
+	/**
+	 * Application-specific data that will be passed into
+	 * `.transform` and `.deallocate` (making them reenterant
+	 * so it can be called by multiple threads, or to
+	 * configure the function)
+	 * 
+	 * May be `NULL`
+	 */
+	void *user_data;
+
+	/**
+	 * Identifier for function
+	 *
+	 * This need only be set when `libnormalform_to_string`
+	 * is called. The value must be parsable by the application
+	 * without any explicit termination
+	 */
+	const char *identifier;
+
+	/**
+	 * `NULL` or copy of of the object for `libnormalform_clone`
+	 * 
+	 * This field should normally be unset, but before calling
+	 * `libnormalform_clone`, the application must set it
+	 * either to `NULL` (if the clone can use the same reference)
+	 * or to a clone of the variable.
+	 */
+	struct libnormalform_transformer *copy_for_clone;
+
+	/**
+	 * Before calling `libnormalform_express`, `libnormalform_dnf`,
+	 * or `libnormalform_cnf` this shall be set to 0 if the function
+	 * may keep the function, or to a non-0 value if it shall
+	 * be replaced with a tautology
+	 */
+	int requires_elimination;
+
+	/**
+	 * This field will automatically be set to `LIBNORMALFORM_NOT_BUILT_IN`
+	 * to indicated that the object originates in the application,
+	 * however a `struct libnormalform_term *` created by the library
+	 * (via `libnormalform_express`, `libnormalform_dnf`, or
+	 * `libnormalform_cnf`) can contain objects with other values in this
+	 * field, to describe what it does. In particular, depending on the
+	 * flags used when creating the `struct libnormalform_term *`,
+	 * qualification sentences may contain `LIBNORMALFORM_DOMAIN_VIEW`
+	 * and `LIBNORMALFORM_IMAGE_VIEW` and transformers.
+	 */
+	enum libnormalform_builtin_transformer builtin;
+};
+
+
+/**
+ * Key–value pair
+ */
+struct libnormalform_mapping {
+	/**
+	 * Key
+	 * 
+	 * In mapped qualifiers (`libnormalform_all`,
+	 * `libnormalform_any`, `libnormalform_one`), this
+	 * is used as the input for the antecedent
+	 * 
+	 * In unmapped qualifiers (`libnormalform_exists`,
+	 * `libnormalform_nexists`, `libnormalform_unique`),
+	 * is this used as the input for the predicate
+	 * 
+	 * In premapped qualifiers (`libnormalform_universally`,
+	 * `libnormalform_existentially`, `libnormalform_uniquely`),
+	 * is this unused
+	 * 
+	 * Unused for domain size checks (`libnormalform_empty`,
+	 * `libnormalform_nonempty`, `libnormalform_singleton`)
+	 */
+	void *key;
+
+	/**
+	 * Value
+	 * 
+	 * In mapped qualifiers (`libnormalform_all`,
+	 * `libnormalform_any`, `libnormalform_one`), this
+	 * is used as the input for the predicate
+	 * 
+	 * In unmapped qualifiers (`libnormalform_exists`,
+	 * `libnormalform_nexists`, `libnormalform_unique`),
+	 * is this unused
+	 * 
+	 * In premapped qualifiers (`libnormalform_universally`,
+	 * `libnormalform_existentially`, `libnormalform_uniquely`),
+	 * is this used as the input for the predicate
+	 * 
+	 * Unused for domain size checks (`libnormalform_empty`,
+	 * `libnormalform_nonempty`, `libnormalform_singleton`)
+	 */
+	void *value;
+};
+
+
+/**
+ * Domain of interest for qualifiers
+ */
+struct libnormalform_map {
+	/**
+	 * Associative array over values in the domain
+	 */
+	struct libnormalform_mapping *mappings;
+
+	/**
+	 * The number of elements in `.mappings`
+	 */
+	size_t nmappings;
+
+	/**
+	 * Application-specific data that the application
+	 * could use to identify the domain
+	 * 
+	 * May be `NULL`
+	 */
+	void *user_data;
+
+	/**
+	 * Identifier for domain
+	 *
+	 * This need only be set when `libnormalform_to_string`
+	 * is called. The value must be parsable by the application
+	 * without any explicit termination
+	 */
+	const char *identifier;
+
+	/**
+	 * `NULL` or copy of of the object for `libnormalform_clone`
+	 * 
+	 * This field should normally be unset, but before calling
+	 * `libnormalform_clone`, the application must set it
+	 * either to `NULL` (if the clone can use the same reference)
+	 * or to a clone of the variable.
+	 */
+	struct libnormalform_map *copy_for_clone;
+};
+
+
+struct libnormalform_atom_comparsion {
+	int version;
+	enum libnormalform_sentences_relationship relationship;
+};
+
+struct libnormalform_domain_comparsion {
+	int version;
+	enum libnormalform_domain_relationship relationship;
+};
+
+struct libnormalform_analysers { /* TODO doc */
+	void *user_data;
+	int (*compare_variable_to_variable)(void *user_data, struct libnormalform_atom_comparsion *result,
+	                                    struct libnormalform_variable *left, struct libnormalform_variable *right);
+	int (*compare_function_to_function)(void *user_data, struct libnormalform_atom_comparsion *result,
+	                                    struct libnormalform_function *left, struct libnormalform_function *right);
+	int (*compare_variable_to_function)(void *user_data, struct libnormalform_atom_comparsion *result,
+	                                    struct libnormalform_variable *left, struct libnormalform_function *right);
+	int (*compare_domains)(void *user_data, struct libnormalform_domain_comparsion *result,
+	                       struct libnormalform_map *left, struct libnormalform_map *right);
+};
+
+
+/**
+ * Qualifier
+ */
+struct libnormalform_qualification {
+	struct libnormalform_map *map;          /**< The domain of interest */
+	struct libnormalform_term *antecedent;  /**< The antecedent, `NULL` if joined with the predicate */
+	struct libnormalform_term *predicate;   /**< The predicate */
+};
+
+
+/**
+ * Clause of terms
+ */
+struct libnormalform_clause {
+	struct libnormalform_term *terms;  /**< The terms in the clause */
+	size_t nterms;                     /**< The number of terms in the clause */
+};
+
+
+/**
+ * Transformater function with input
+ */
+struct libnormalform_transformation {
+	struct libnormalform_transformer *transformer;  /**< The transformer function */
+	struct libnormalform_term *sentence;            /**< The sentence the transformation is over */
+};
+
+
+/**
+ * Application-readable sentence
+ */
+struct libnormalform_term {
+	/**
+	 * The type of the clause, qualifier, literal, or transformation
+	 */
+	enum libnormalform_term_type type;
+
+	/**
+	 * Whether the term or own of its subterms have been reduced;
+	 */
+	int reduced;
+
+	/**
+	 * The description of the sentence
+	 */
+	union {
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`
+		 */
+		struct libnormalform_clause disjunction;
+
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_CONJUNCTION`
+		 */
+		struct libnormalform_clause conjunction;
+
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION`
+		 */
+		struct libnormalform_clause exclusive_disjunction;
+
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`,
+		 * `LIBNORMALFORM_CONJUNCTION`, or
+		 * `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION`
+		 */
+		struct libnormalform_clause clause;
+
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_TRANSFORMATION`
+		 */
+		struct libnormalform_transformation transformation;
+
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_VARIABLE` or
+		 * `LIBNORMALFORM_NEGATED_VARIABLE`
+		 */
+		struct libnormalform_variable *variable;
+
+		/**
+		 * Use if `.type` is `LIBNORMALFORM_FUNCTION` or
+		 * `LIBNORMALFORM_NEGATED_FUNCTION`
+		 */
+		struct libnormalform_function *function;
+
+		/**
+		 * Use if '.type` is `LIBNORMALFORM_FOR_ALL` or
+		 * `LIBNORMALFORM_NEGATED_FOR_ALL`
+		 */
+		struct libnormalform_qualification for_all;
+
+		/**
+		 * Use if '.type` is `LIBNORMALFORM_FOR_ANY` or
+		 * `LIBNORMALFORM_NEGATED_FOR_ANY`
+		 */
+		struct libnormalform_qualification for_any;
+
+		/**
+		 * Use if '.type` is `LIBNORMALFORM_FOR_ONE` or
+		 * `LIBNORMALFORM_NEGATED_FOR_ONE`
+		 */
+		struct libnormalform_qualification for_one;
+
+		/**
+		 * Use if '.type` is `LIBNORMALFORM_FOR_ALL`,
+		 * `LIBNORMALFORM_NEGATED_FOR_ALL`, `LIBNORMALFORM_FOR_ANY`,
+		 * `LIBNORMALFORM_NEGATED_FOR_ANY`, `LIBNORMALFORM_FOR_ONT`,
+		 * or `LIBNORMALFORM_NEGATED_FOR_ONE`
+		 */
+		struct libnormalform_qualification qualification;
+	} term;
+};
+
+
+
+
+
+/**
+ * Increase the reference count of a sentence object by 1
+ * 
+ * @param   this  The sentence object
+ * @return        `this` on success, `NULL` on failure
+ * 
+ * @throws  ENOMEM  The reference count is already maximised (at SIZE_MAX)
+ * 
+ * Reasonable application can safely assume that `this` is always returned
+ * 
+ * Note, `NULL` is returned without `errno` modified if `this` is `NULL`
+ * 
+ * Be aware that this function is not thread-safe
+ * 
+ * @seealso  libnormalform_clone
+ * @seealso  libnormalform_free
+ */
+LIBNORMALFORM_SENTENCE *(libnormalform_ref)(LIBNORMALFORM_SENTENCE *this);
+
+
+/**
+ * Create a copy of a sentence object
+ * 
+ * This may be necessary as usage of sentence objects are not thread-safe,
+ * creating a copy of a sentence object will allow one thread to safely
+ * use one copy and another thread the other copy
+ * 
+ * Before calling this function, the application shall set `.copy_for_clone`
+ * in each `struct libnormalform_variable`, `struct libnormalform_function`,
+ * `struct libnormalform_map` and `struct libnormalform_transformer`, used
+ * by the sentence. `.copy_for_clone` shall either be set to `NULL` or a copy
+ * of object. If `NULL` is used, the copy of `this` will use the same
+ * instance of the object as `this`.
+ * 
+ * @param   this  The sentence object
+ * @return        A unique pointer on success or `NULL` if
+ *                `this` is `NULL`; `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create a copy of `this`
+ * 
+ * Be aware that this function is not thread-safe
+ * 
+ * @seealso  libnormalform_ref
+ * @seealso  libnormalform_free
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_clone)(LIBNORMALFORM_SENTENCE *this);
+
+
+/**
+ * When `this` is a `LIBNORMALFORM_SENTENCE *`:
+ * 
+ *     Decrease the reference count of a sentence object by 1, 
+ *     if the object reference count reaches 0, deallocate the
+ *     object.
+ * 
+ *     Because all functions that return a new sentence object
+ *     (excluding `libnormalform_clone`), adopt the ownership
+ *     of the reference to each input sentence (and may create
+ *     it's own subsentences), this function is called recursively,
+ *     and the application shall not attempt to call this function
+ *     for sentences used to create other sentences
+ * 
+ *     Be aware the this function will not deallocate any
+ *     `struct libnormalform_variable *`,
+ *     `struct libnormalform_function *`, or
+ *     `struct libnormalform_map *` used in the sentence as
+ *     these are owned any managed by the application
+ * 
+ * When `this` is a `struct libnormalform_term *`:
+ * 
+ *     Recursively deallocate `this`. This will only deallocate
+ *     `this` and subobjects with the same type
+ * 
+ *     If `.type` is invalid for `this` or any subobject, the
+ *     function's behaviour is undefined
+ * 
+ * This function is a no-operation function when `this` is `NULL`
+ * 
+ * @param   this  The object
+ * 
+ * This function's behaviour is undefined if `this` is not `NULL`
+ * but not of the one of the above listed types
+ * 
+ * Be aware that this function is not thread-safe
+ */
+void (libnormalform_free)(void *this);
+
+
+/**
+ * Evaluate a sentence to determine it's trueness
+ * 
+ * Before calling this function, the application code shall
+ * configure any `struct libnormalform_variable`,
+ * `struct libnormalform_function`, and `struct libnormalform_map`
+ * used by the sentence. For each `struct libnormalform_variable`,
+ * `.value` shall either be set to `LIBNORMALFORM_TRUE` or
+ * `LIBNORMALFORM_FALSE` to indicate the value of the atom.
+ * For each `struct libnormalform_function`, `.evaluate` shall
+ * be set to a pointer to function that evaluates the input and
+ * `.user_data` shall be set to any application data the function
+ * needs to operate; `.evaluate` shall return 1, 0, or -1 as
+ * specified for this function; and may set `errno` to indicate
+ * an error (library itself does not look at `errno`, but may
+ * be used to signal the error to the application, of course
+ * the error may also be specified to the application in an
+ * application-specific way). For each `struct libnormalform_map`,
+ * `.mappings` shall be to the associated array of values
+ * that shall be tested by the qualifier-sentence it is
+ * used by, and `.nmappings` shall be set to the number of
+ * pairs in this array.
+ * 
+ * @param   this  The sentence to evaluate
+ * @return        1 if the sentence is true,
+ *                0 if the sentence is false,
+ *                -1 on failure
+ * 
+ * Only application code may cause this function to
+ * fail, therefore no error codes are predefined for
+ * this function, instead `errno` is only set by
+ * the failing application code
+ * 
+ * Be aware that this function is not thread-safe
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this);
+
+
+
+
+
+/**
+ * Return an application readable expression of a statement in negation
+ * normal form, optionally with XOR, and reduce the statement to a
+ * statement that is at least as true (but as false as possible), and
+ * is minimised, according what the application specifies that it can
+ * work with
+ * 
+ * Before calling this function, the application shall set `.relaxation`
+ * `.requires_relaxation` in each `struct libnormalform_function` used
+ * used by the sentence. `.requires_relaxation` may be set as 0 if the
+ * function shall not be replaced (in this case `.relaxation` need not
+ * be set), but set to 1 if the function most be replaced with a more
+ * true function. In the latter case, `.relaxation` shall either be set
+ * to the new function or to `NULL`; if set to null, the function is
+ * reduced to a tautological sentence. For any `libnormalform_transformer`
+ * it must also set `.requires_elimination` to 1 if the transformation
+ * must be replaces with a tautology, and 0 otherwise.
+ * 
+ * @param   this       The sentence to describe
+ * @param   flags      The bitwise OR of any number of the following values:
+ *                     - LIBNORMALFORM_AVOID_FOR_ALL:                   Prefer ¬∃x.¬φ over ∀x.φ
+ *                     - LIBNORMALFORM_AVOID_NEGATED_FOR_ALL:           Prefer  ∃x.¬φ over ¬∀x.φ
+ *                     - LIBNORMALFORM_AVOID_FOR_ANY:                   Prefer ¬∀x.¬φ over ∃x.φ
+ *                     - LIBNORMALFORM_AVOID_NEGATED_FOR_ANY:           Prefer  ∀x.¬φ over ¬∃x.φ
+ *                     - LIBNORMALFORM_RELAX_FOR_ONE:                   Relax any positive ∃!x.φ into ∃x.φ
+ *                     - LIBNORMALFORM_REDUCE_XOR:                      Do not use XOR in the returned statement,
+ *                                                                      but transform it to negation normal form
+ *                     - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL            Express   φ(x)∀x:θ(x)   on the form  ∀x.(θ(x) → φ(x))
+ *                     - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL    Express ¬(φ(x)∀x:θ(x))  on the form ¬∀x.(θ(x) → φ(x))
+ *                     - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY            Express   φ(x)∃x:θ(x)   on the form  ∃x.(θ(x) ∧ φ(x))
+ *                     - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY    Express ¬(φ(x)∃x:θ(x))  on the form ¬∃x.(θ(x) ∧ φ(x))
+ *                     - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE            Express   φ(x)∃!x:θ(x)  on the form  ∃!x.(θ(x) ∧ φ(x))
+ *                     - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE    Express ¬(φ(x)∃!x:θ(x)) on the form ¬∃!x.(θ(x) ∧ φ(x))
+ *                     - LIBNORMALFORM_ELIMINATE_FOR_ALL                Relax any non-translatable  ∀x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL        Relax any non-translatable ¬∀x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_FOR_ANY                Relax any non-translatable  ∃x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ANY     Relax any non-translatable ¬∃x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_IN_FOR_ONE             Relax any non-translatable ∃!x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ONE     Relax any ¬∃!x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_VARIABLE               Relax any positive variable literal to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE       Relax any negative variable literal to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_FUNCTION               Relax any positive function literal to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION       Relax any negative function literal to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_XOR                    Remove all XOR's (nullified by `LIBNORMALFORM_REDUCE_XOR`)
+ * @param   analysers  Application provided functions to help reduce the statement, or `NULL`
+ * @return             The description of the sentence, `NULL` on failure;
+ *                     the returned pointer shall be deallocated with
+ *                     `libnormalform_free` when it is no longer needed
+ * 
+ * @seealso  libnormalform_dnf
+ * @seealso  libnormalform_cnf
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+struct libnormalform_term *(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO man */
+                                                   const struct libnormalform_analysers *analysers);
+
+
+/**
+ * Variant of `libnormalform_express` that always canonicalises
+ * the statement to disjunctive normal form
+ * 
+ * @param   this       The sentence to describe
+ * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR`
+ *                     is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not,
+ *                     but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless
+ *                     there is a risk that it would be too costly (EXPSPACE)
+ * @param   analysers  Application provided functions to help reduce the statement, or `NULL`
+ * @return             The description of the sentence, `NULL` on failure;
+ *                     the returned pointer shall be deallocated with
+ *                     `libnormalform_free` when it is no longer needed
+ * 
+ * @seealso  libnormalform_express
+ * @seealso  libnormalform_cnf
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+struct libnormalform_term *(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */
+                                               const struct libnormalform_analysers *analysers);
+
+
+/**
+ * Variant of `libnormalform_express` that always canonicalises
+ * the statement to conjuctive normal form
+ * 
+ * @param   this       The sentence to describe
+ * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR`
+ *                     is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not,
+ *                     but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless
+ *                     there is a risk that it would be too costly (EXPSPACE)
+ * @param   analysers  Application provided functions to help reduce the statement, or `NULL`
+ * @return             The description of the sentence, `NULL` on failure;
+ *                     the returned pointer shall be deallocated with
+ *                     `libnormalform_free` when it is no longer needed
+ * 
+ * @seealso  libnormalform_express
+ * @seealso  libnormalform_dnf
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */
+                                               const struct libnormalform_analysers *analysers);
+
+
+/**
+ * Convert a sentence object to a string that can be parsed
+ * by `libnormalform_from_string` (and is somewhat human-readable)
+ * 
+ * Before calling this function, the application shall set `.identifier`
+ * in each `struct libnormalform_variable`, `struct libnormalform_function`,
+ * `struct libnormalform_map`, and `struct libnormalform_transformer` used
+ * by the sentence to a non-`NULL`, unique string that identifies (but
+ * does not necessarily describe) the object. The application must be able
+ * to find the end of any such string without any explicit termination
+ * (e.g., eithout there being a NUL-terminator)
+ * 
+ * Note that when a sentence is created, it is optimised and
+ * reduced into fewer types of connetives (it's reducted into
+ * negation normal form, except with XOR allowed, but not
+ * necessarily to any canonical form) during construction,
+ * so this function will not necessarily reproduce the sentence
+ * as it was specified when it was constructed.
+ * 
+ * @param   this  The sentence object to serialise
+ * @return        String-representation of `this`, `NULL` failure;
+ *                the caller shall deallocate the returned pointer
+ *                with free(3) when it is no longer needed
+ *
+ * @throws  ENOMEM  Insufficient memory available to serialise `this`
+ * 
+ * @seealso  libnormalform_from_string
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_USE_FREE__ LIBNORMALFORM_NONNULL_INPUT__
+char *(libnormalform_to_string)(LIBNORMALFORM_SENTENCE *this);
+
+
+/**
+ * Convert a string, created with `libnormalform_to_string`
+ * (or is on similar form), to sentence object
+ * 
+ * The string shall be on the whitespace-insensitive form:
+ * 
+ *     constant         ::= "TRUE" | "FALSE";
+ *     connective1      ::= "NOT";
+ *     connective2      ::= "AND" | "OR" | "XOR" | "IF" | "IMPLY" |
+ *                          "NAND" | "NOR" | "XNOR" | "NIF" | "NIMPLY";
+ *     qualifier0       ::= "EMPTY" | "NONEMPTY" | "SINGLETON";
+ *     qualifier1       ::= "EXISTS" | "NEXISTS" | "UNIQUE" |
+ *                          "EXISTENTIALLY" | "UNIVERSALLY" | "UNIQUELY";
+ *     qualifier2       ::= "ALL" | "ANY" | "ONE";
+ *     unary            ::= connective1 [reference-point] "(" sentence ")";
+ *     variadic         ::= connective2 [reference-point] "(" [sentence-list] ")";
+ *     sentence-list    ::= sentence ["," sentence-list];
+ *     qualified0       ::= qualifier0 [reference-point] "(" map ")";
+ *     qualified1       ::= qualifier1 [reference-point] "(" map "," sentence ")";
+ *     qualified2       ::= qualifier2 [reference-point] "(" map "," sentence "," sentence ")";
+ *     atom             ::= atom-var | atom-fun;
+ *     atom-var         ::= "VARIABLE" [reference-point] "(" variable ")";
+ *     atom-fun         ::= "FUNCTION" [reference-point] "(" function ")";
+ *     transformation   ::= "TRANSFORMATION" [reference-point] "(" transformer "," sentence ")";
+ *     reference-point  ::= "@" decimal-number;
+ *     reference        ::= "REF(" decimal-number ")";
+ *     one-to-nine      ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9";
+ *     zero-to-nine     ::= "0" | one-to-nine;
+ *     decimal-number   ::= "0" | positive-decimal;
+ *     positive-decimal ::= one-to-nine [digits];
+ *     digits           ::= zero-to-nine [digits];
+ *     sentence         ::= constant | unary | variadic | qualified0 | qualified1 |
+ *                          qualified2 | atom | transformation | reference;
+ * 
+ * where "sentence" is the root, and where "map" is parsed by `*spec->get_map`,
+ * "variable" is parsed by `*spec->get_variable`, "function" is parsed by
+ * `*spec->get_function`, and "transformer" is parsed by `*spec->get_transformer`.
+ * References must start at 0 and increment by one, in left-to-right order,
+ * every time reference point is specified, and forward-references are not allowed
+ * (this includes reference to containing sentence (whose reference ID is lower
+ * because it is written earlier)).
+ * 
+ * @param   s        The representation of the sentence to deserialise
+ * @param   end_out  Output parameter for the end of `s`;
+ *                   if `NULL` the function will fail if `s` contains
+ *                   excess information
+ * @param   spec     Specification for how application managed objects
+ *                   are to be deserialise
+ * @return           A unique pointer, that is a deserialisation of `s`,
+ *                   or `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to deserialise `s`
+ * @throws  EINVAL  `s` was not properly formatted
+ * @throws  EINVAL  `end_out` was `NULL` and `s` containd excess information
+ * @throws  EDOM    `s` contained a empty clause for a connective
+ *                  that does not support empty clauses
+ * @throws  EDOM    `s` contained a transformation over a qualifer
+ * @throws  ENOENT  `s` contained a variable but `spec->get_variable` was `NULL`
+ * @throws  ENOENT  `s` contained a boolean function but `spec->get_function` was `NULL`
+ * @throws  ENOENT  `s` contained a domain but `spec->get_map` was `NULL`
+ * @throws  ENOENT  `s` contained a transformation but `spec->get_transformer` was `NULL`
+ * 
+ * If function in `spec` fails, this function will fail and keep `errno`
+ * as set by the function that failed
+ * 
+ * The function itself does not modify `s` and can operate on read-only
+ * memory, however an offset of the string may be passed into application
+ * code. The application is free to modify `s` if it knows the memory
+ * is indeed writable.
+ * 
+ * @seealso  libnormalform_to_string
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) LIBNORMALFORM_ONE_NONNULL_INPUT__(3)
+LIBNORMALFORM_SENTENCE *(libnormalform_from_string)(char *s, char **end_out, const struct libnormalform_representation_spec *spec);
+
+
+
+
+
+/**
+ * Create an atomic sentence whose value is externally set
+ * 
+ * @param   variable  The variable the sentence shall express
+ * @return            A sentence object referencing `variable`, `NULL` on failure
+ * @throws  ENOMEM    Insufficient memory available to create the sentence
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_variable)(struct libnormalform_variable *variable);
+
+
+/**
+ * Create an atomic sentence whose value is externally evaluated
+ * 
+ * @param   function  The function the sentence shall express
+ * @return            A sentence object referencing `function`, `NULL` on failure
+ * @throws  ENOMEM    Insufficient memory available to create the sentence
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_function)(struct libnormalform_function *function);
+
+
+/**
+ * Create an endomorphic transformation of the input for a sentence
+ *
+ * `function->builtin` will automatically be initialised to `LIBNORMALFORM_NOT_BUILT_IN`
+ * 
+ * @param   function  The transformation function
+ * @param   sentence  The sentence whose input shall be transformed
+ * @return            A sentence whose input is transformed by `function`, `NULL` on failure
+ * @throws  ENOMEM    Insufficient memory available to create the sentence
+ * @throws  EDOM      `sentence` is a qualifier
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+LIBNORMALFORM_SENTENCE *(libnormalform_transformation)(struct libnormalform_transformer *function, LIBNORMALFORM_SENTENCE *sentence);
+
+
+/**
+ * TRUE: Tautology
+ *
+ * Always true
+ *
+ * Commonly written "⊤", "1", or "T"
+ * 
+ * @return            An atomic sentence with a constant value of True, `NULL` on failure
+ * @throws  ENOMEM    Insufficient memory available to create the sentence
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_true)(void);
+
+
+/**
+ * FALSE: Contradiction
+ * 
+ * Always false
+ * 
+ * Commonly written "⊥", "1", or "F"
+ * 
+ * @return            An atomic sentence with a constant value of False, `NULL` on failure
+ * @throws  ENOMEM    Insufficient memory available to create the sentence
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_false)(void);
+
+
+/**
+ * NOT: Negation
+ *
+ * The condition must not be met:
+ * ¬0 = 1
+ * ¬1 = 0
+ *
+ * Properties:
+ * -  Involution
+ * -  Distribution over AND changes connective to OR (De Morgan's law)
+ * -  Distribution over OR changes connective to AND (De Morgan's law)
+ * 
+ * Commonly written "¬" ("¬x"), "~", or "!", or with overstroke
+ * 
+ * @param   x  The sentence that should be negated;
+ *             ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `x` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `x` to
+ * be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_not)(LIBNORMALFORM_SENTENCE *x);
+
+
+/**
+ * FOR ALL: Universal quantification (mapped)
+ * 
+ * The predicate must be met for every element that the antecedent
+ * is met for; if no element exists, or the antecedent is false for
+ * every element, the sentence is true
+ * 
+ * Properties:
+ * -  Vacuous truth
+ * -  ∀x∈D.P(x) → ⊤ = ⊤
+ * -  ∀x∈D.⊥ → Q(x) = ⊤
+ * -  ∀x∈D.⊤ → ⊥ ⊨ D = ∅
+ * -  Conjunction
+ * 
+ * Commonly written "∀" ("∀x∈d.k(x) → v(x)", "∀x∈d (k(x) → v(x))", or "v(x) ∀ x∈d : k(x)")
+ * 
+ * The antecedent is tested for every `.key` in the domain,
+ * and the predicate is tested for every associated `.value`
+ * where the antecedent is met; but the testing is cut short
+ * if the antecedent is met and not the predicate for an element
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   k  The antecedent; ownership is transfered to this function
+ * @param   v  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `k` or `v` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `k` or
+ * `v` to be `NULL`)
+ * 
+ * @seealso  libnormalform_nexists
+ * @seealso  libnormalform_universally
+ * @seealso  libnormalform_any
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+LIBNORMALFORM_SENTENCE *(libnormalform_all)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v);
+
+
+/**
+ * THERE EXISTS: Existential quantification (mapped)
+ * 
+ * The predicate must be met for at least one element that the
+ * antecedent is met for; if no element exists, or the antecedent is
+ * false for every element, the sentence is false
+ * 
+ * Properties:
+ * -  Vacuous falsity
+ * -  ∃x∈D.P(x) ∧ ⊥ = ⊥
+ * -  ∃x∈D.⊥ ∧ Q(x) = ⊥
+ * -  ∃x∈D.⊤ ∧ ⊤ ⊨ D ⊃ ∅
+ * -  Disjunction
+ * 
+ * Commonly written "∃" ("∃x∈d.k(x) ∧ v(x)", "∃x∈d (k(x) ∧ v(x))", or "v(x) ∃ x∈d : k(x)")
+ * 
+ * The antecedent is tested for every `.key` in the domain,
+ * and the predicate is tested for every associated `.value`
+ * where the antecedent is met; but the testing is cut short
+ * if both the antecedent and predicate is met for an element
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   k  The antecedent; ownership is transfered to this function
+ * @param   v  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `k` or `v` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `k` or
+ * `v` to be `NULL`)
+ * 
+ * @seealso  libnormalform_exists
+ * @seealso  libnormalform_existentially
+ * @seealso  libnormalform_one
+ * @seealso  libnormalform_all
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+LIBNORMALFORM_SENTENCE *(libnormalform_any)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v);
+
+
+/**
+ * THERE EXISTS ONE: Unique existential quantification (mapped)
+ * 
+ * The predicate must be met for exactly one element that the
+ * antecedent is met for; if no element exists, or the antecedent is
+ * false for every element, the sentence is false
+ * 
+ * Properties:
+ * -  Vacuous falsity
+ * -  ∃!x∈D.P(x) ∧ ⊥ = ⊥
+ * -  ∃!x∈D.⊥ ∧ Q(x) = ⊥
+ * -  ∃!x∈D.⊤ ∧ ⊤ ⊨ |D| = 1
+ * 
+ * Commonly written "∃!" ("∃!x∈d.k(x) ∧ v(x)", "∃!x∈d (k(x) ∧ v(x))", or "v(x) ∃! x∈d : k(x)")
+ * 
+ * The antecedent is tested for every `.key` in the domain,
+ * and the predicate is tested for every associated `.value`
+ * where the antecedent is met; but the testing is cut short
+ * if both the antecedent and predicate is met for two elements
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   k  The antecedent; ownership is transfered to this function
+ * @param   v  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `k` or `v` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `k` or
+ * `v` to be `NULL`)
+ * 
+ * @seealso  libnormalform_unique
+ * @seealso  libnormalform_uniquely
+ * @seealso  libnormalform_any
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+LIBNORMALFORM_SENTENCE *(libnormalform_one)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v);
+
+
+
+
+
+/**
+ * AND: Conjunction
+ *
+ * Also known as BUT
+ * 
+ * All conditions must be met
+ * 
+ * 0 ∧ 0 = 0
+ * 0 ∧ 1 = 0
+ * 1 ∧ 0 = 0
+ * 1 ∧ 1 = 1
+ * 
+ * Properties:
+ * -  Vacuous truth
+ * -  Identity singleton
+ * -  Commutative
+ * -  Associative
+ * -  Distributive over OR
+ * -  Distributive over XOR
+ * -  ⊤ as identity
+ * -  Dominated by ⊥
+ * -  Idempotent
+ * -  Connecting complement results in contradiction
+ * -  More lax term is absorbed (A ∧ (A ∨ B) simplifies to A)
+ * 
+ * Commonly written "∧" ("⋀" if n-ary), "&", or with juxtaposition
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective AND; this can be any number
+ *              of arguments, even none; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_AND
+ * @seealso  libnormalform_and_checked
+ * @seealso  libnormalform_andl_checked
+ * @seealso  libnormalform_vand_checked
+ * @seealso  libnormalform_andl
+ * @seealso  libnormalform_vand
+ * @seealso  libnormalform_and2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_and)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * OR: Disjunction
+ * 
+ * Also known as Inclusive disjunction
+ * 
+ * At least one condition must be met
+ * 
+ * 0 ∨ 0 = 0
+ * 0 ∨ 1 = 1
+ * 1 ∨ 0 = 1
+ * 1 ∨ 1 = 1
+ * 
+ * Properties:
+ * -  Vacuous falsity
+ * -  Identity singleton
+ * -  Commutative
+ * -  Associative
+ * -  Distributive over AND
+ * -  ⊥ as identity
+ * -  Dominated by ⊤
+ * -  Idempotent
+ * -  Connecting complement results in tautology
+ * -  More strict term is absorbed (A ∨ (A ∧ B) simplifies to A)
+ * 
+ * Commonly written "∨" ("⋁" if n-ary), "|", or "+"
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective OR; this can be any number
+ *              of arguments, even none; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_OR
+ * @seealso  libnormalform_or_checked
+ * @seealso  libnormalform_orl_checked
+ * @seealso  libnormalform_vor_checked
+ * @seealso  libnormalform_orl
+ * @seealso  libnormalform_vor
+ * @seealso  libnormalform_or2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_or)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * XOR: Exclusive disjunction
+ * 
+ * Also known as EOR, EXOR, NEQ, NIFF, Parity (especially when n-ary),
+ * Exclusive alternation, Exclusive or, Logical non-equivalence,
+ * Logical non-equivalence, Logical inequality, Not if and only if,
+ * or Unless and only unless
+ * 
+ * An odd number of conditions must be met
+ * 
+ * 0 ⊕ 0 = 0
+ * 0 ⊕ 1 = 1
+ * 1 ⊕ 0 = 1
+ * 1 ⊕ 1 = 0
+ * 
+ * Properties:
+ * -  Vacuous falsity
+ * -  Identity singleton
+ * -  Commutative
+ * -  Associative
+ * -  ⊥ as identity
+ * -  Complemented by ⊤
+ * -  Annihiliation by reflextion
+ * -  Connecting complement results in tautology
+ * -  A ⊕ B is reduced to (A ∨ B) ∧ (¬A ∨ ¬B) or
+ *    (A ∧ ¬B) ∨ (¬A ∧ B) in negation normal form
+ * 
+ * Commonly written "⊕" ("⨁" if n-ary), "⊻", "↮", "⇎", "≢", or "^"
+ * 
+ * Note that the name Exclusive disjunction is misleading
+ * when there are more than two terms, as the statement
+ * will not check that exactly one term is true, but rather
+ * calculate the parity of the terms.
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective XOR; this can be any number
+ *              of arguments, even none; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_XOR
+ * @seealso  libnormalform_xor_checked
+ * @seealso  libnormalform_xorl_checked
+ * @seealso  libnormalform_vxor_checked
+ * @seealso  libnormalform_xorl
+ * @seealso  libnormalform_vxor
+ * @seealso  libnormalform_xor2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_xor)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * IF: Converse implication
+ * 
+ * Also known as Converse conditional
+ * 
+ * Creates a chain where any condition must be at least
+ * as satisfied as the condition left to it (xs[0] ≤ xs[1])
+ * (Not xs[1] without xs[0]); it is false only when only
+ * the left-most term is false
+ * 
+ * 0 ← 0 = 1
+ * 0 ← 1 = 0
+ * 1 ← 0 = 1
+ * 1 ← 1 = 1
+ * 
+ * Properties:
+ * -  Identity singleton
+ * -  Non-commutative
+ * -  Left-associative: A ← B ← C = (A ← B) ← C ≠ A ← (B ← C)
+ * -  Complemented by left ⊥
+ * -  Dominated by left ⊤
+ * -  Right falsity results in tautology
+ * -  ⊤ as right identity
+ * -  Contrapositivity: A ← B = ¬B ← ¬A
+ * -  Transitive: (A ← B) ∧ (B ← C) ⊨ A ← C
+ * -  Reflexive: A ← A = ⊤
+ * -  Complete: (A ← B) ∨ (B ← A) = ⊤
+ * -  Excluded middle: (A ← B) ∨ (¬A ← B) = ⊤
+ * -  Import-export: (A ← B) ← C = A ← (B ∧ C)
+ * -  Commutativity of antecedents: (A ← B) ← C = (A ← C) ← B
+ * -  Vacuous conditional: ¬A ⊨ B ← A
+ * -  Antecedent strengthening: A ← B ⊨ A ← (B ∧ C)
+ * -  Right-distributive: (A ← B) ← C = (A ← C) ← (B ← C)
+ * -  Distributive over left AND
+ * -  Distributive over left OR
+ * -  Distributing over right AND changes AND to OR
+ * -  Distributing over right OR changes OR to AND
+ * -  A ← B is reduced to A ∨ ¬B in negation normal form
+ * 
+ * Commonly written "←", "⇐", "<-", "<=", "≤", "⩽", or "⊂"
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective IF; this can be any positive
+ *              number of arguments; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * @throws  EDOM    `xs` contains no term (but only `NULL`)
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_IF
+ * @seealso  libnormalform_if_checked
+ * @seealso  libnormalform_ifl_checked
+ * @seealso  libnormalform_vif_checked
+ * @seealso  libnormalform_ifl
+ * @seealso  libnormalform_vif
+ * @seealso  libnormalform_if2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_if)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * IMPLY: Material implication
+ * 
+ * Also known as IMPLIES, IF..THEN, NOT..WITHOUT or material conditional
+ * 
+ * Creates a chain where any condition must be at most
+ * as satisfied as the condition left to it (xs[0] ≥ xs[1])
+ * (Not xs[0] without xs[1]); it is false only when only
+ * the right-most term is false
+ * 
+ * 0 → 0 = 1
+ * 0 → 1 = 1
+ * 1 → 0 = 0
+ * 1 → 1 = 1
+ * 
+ * Properties:
+ * -  Vacuous truth
+ * -  Identity singleton
+ * -  Non-commutative
+ * -  Right-associative: A → B → C = A → (B → C) ≠ (A → B) → C
+ * -  Complemented by right ⊥
+ * -  Dominated by right ⊤
+ * -  Left falsity results in tautology
+ * -  ⊤ as left identity
+ * -  Contrapositivity: A → B = ¬B → ¬A
+ * -  Transitive: (A → B) ∧ (B → C) ⊨ A → C
+ * -  Reflexive: A → A = ⊤
+ * -  Complete: (A → B) ∨ (B → A) = ⊤
+ * -  Excluded middle: (A → B) ∨ (A → ¬B) = ⊤
+ * -  Import-export: A → (B → C) = (A ∧ B) → C
+ * -  Commutativity of antecedents: A → (B → C) = B → (A → C)
+ * -  Vacuous conditional: ¬A ⊨ A → B
+ * -  Antecedent strengthening: A → B ⊨ (A ∧ C) → B
+ * -  Left-distributive: A → (B → C) = (A → B) → (A → C)
+ * -  Distributive over right AND
+ * -  Distributive over right OR
+ * -  Distributing over left AND changes AND to OR
+ * -  Distributing over left OR changes OR to AND
+ * -  A → B is reduced to ¬A ∨ B in negation normal form
+ * 
+ * Commonly written "→", "⇒", "->", "=>", ">=", "≥", "⩾", or "⊃"
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should
+ *              be joined by the connective IMPLY; this can be any
+ *              number of arguments; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_IMPLY
+ * @seealso  libnormalform_imply_checked
+ * @seealso  libnormalform_implyl_checked
+ * @seealso  libnormalform_vimply_checked
+ * @seealso  libnormalform_implyl
+ * @seealso  libnormalform_vimply
+ * @seealso  libnormalform_imply2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_imply)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * NAND: Alternative denial
+ * 
+ * Also known as Non-conjunction, Negated conjunction,
+ * Mutual exclusion, or Sheffer stroke
+ * 
+ * Creates a left-associated NAND-chain; in NAND, the
+ * two conditions must not be met at the same time
+ * 
+ * 0 ⊼ 0 = 1
+ * 0 ⊼ 1 = 1
+ * 1 ⊼ 0 = 1
+ * 1 ⊼ 1 = 0
+ *
+ * There is no good interpretation for a NAND-chain
+ * 
+ * Commonly written "⊼", "↑", or as AND with the expression over-struck
+ * 
+ * Properties:
+ * -  Identity singleton
+ * -  Commutative (however A ⊼ B ⊼ C ≠ A ⊼ C ⊼ B due to non-associativity)
+ * -  Left-associative: A ⊼ B ⊼ C = (A ⊼ B) ⊼ C ≠ A ⊼ (B ⊼ C)
+ * -  Antireflexive: A ⊼ A = ⊥
+ * -  Annihilated by ⊥: A ⊼ ⊥ = ⊤
+ * -  Complemented by ⊤
+ * -  Distributative over AND
+ * -  A ⊼ B is reduced to ¬A ∨ ¬B in negation normal form
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective NAND; this can be any positive
+ *              number of arguments; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * @throws  EDOM    `xs` contains no term (but only `NULL`)
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_NAND
+ * @seealso  libnormalform_nand_checked
+ * @seealso  libnormalform_nandl_checked
+ * @seealso  libnormalform_vnand_checked
+ * @seealso  libnormalform_nandl
+ * @seealso  libnormalform_vnand
+ * @seealso  libnormalform_nand2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_nand)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * NOR: Joint denial
+ * 
+ * Also known as Non-disjunction, Negated disjunction, Peirce arrow,
+ * Quine dagger, or Webb operator
+ * 
+ * Creates a left-associated NOR-chain; in NOR, the
+ * two conditions must be unmet at same time
+ * 
+ * 0 ⊽ 0 = 1
+ * 0 ⊽ 1 = 0
+ * 1 ⊽ 0 = 0
+ * 1 ⊽ 1 = 0
+ * 
+ * There is no good interpretation for a NOR-chain
+ * 
+ * Commonly written "⊽", "↓", or as OR with the expression over-struck
+ * 
+ * Properties:
+ * -  Identity singleton
+ * -  Commutative (however A ⊽ B ⊽ C ≠ A ⊽ C ⊽ B due to non-associativity)
+ * -  Left-associative: A ⊽ B ⊽ C = (A ⊽ B) ⊽ C ≠ A ⊽ (B ⊽ C)
+ * -  Anti-idempotent: A ⊽ A = ¬A
+ * -  Annihilated by ⊤: A ⊽ ⊤ = ⊥
+ * -  Complemented by ⊤
+ * -  Distributing over AND changes AND to OR
+ * -  Distributing over OR changes OR to AND
+ * -  A ⊽ B is reduced to ¬A ∧ ¬B in negation normal form
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective NOR; this can be any positive
+ *              number of arguments; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * @throws  EDOM    `xs` contains no term (but only `NULL`)
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_NOR
+ * @seealso  libnormalform_nor_checked
+ * @seealso  libnormalform_norl_checked
+ * @seealso  libnormalform_vnor_checked
+ * @seealso  libnormalform_norl
+ * @seealso  libnormalform_vnor
+ * @seealso  libnormalform_nor2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_nor)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * XNOR: Logical bicondition
+ * 
+ * Also known as ENOR, EXNOR, NXOR, XAND, EQ, IFF, Exclusive NOR,
+ * Material biconditional, Logical equivalence, Biimplication,
+ * Bientailment, If and only if, Negated XOR, or Exclusive non-disjunction
+ * 
+ * Creates a left-associated XNOR-chain; in XNOR, the
+ * two conditions must equally true
+ * 
+ * 0 ⊙ 0 = 1
+ * 0 ⊙ 1 = 0
+ * 1 ⊙ 0 = 0
+ * 1 ⊙ 1 = 1
+ * 
+ * The interpretation of a XNOR-chain depends on it's length,
+ * if it's length is even, is equivalent to XOR, otherwise,
+ * it's its complement
+ * 
+ * Commonly written "⊙" ("⨀" if n-ary), "↔", "⇔", "≡", "==", or
+ * as XOR with the expression over-struck
+ * 
+ * Properties:
+ * -  Vacuous truth
+ * -  Identity singleton
+ * -  Commutative
+ * -  Associative
+ * -  ⊤ as identity
+ * -  Complemented by ⊥
+ * -  Reflexive: A ⊙ A = ⊤
+ * -  Annihilated by ⊤: A ⊽ ⊤ = ⊥
+ * -  Connecting complement results in contradiction
+ * -  A ⊙ B is reduced to (A ∨ ¬B) ∧ (¬A ∨ B) or
+ *    (A ∧ B) ∨ (¬A ∧ ¬B) in negation normal form
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should
+ *              be joined by the connective XNOR; this can be any
+ *              number of arguments; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_NXOR
+ * @seealso  libnormalform_nxor_checked
+ * @seealso  libnormalform_nxorl_checked
+ * @seealso  libnormalform_vxnor_checked
+ * @seealso  libnormalform_xnorl
+ * @seealso  libnormalform_vxnor
+ * @seealso  libnormalform_xnor2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_xnor)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * NIF: Converse nonimplication
+ * 
+ * Also known as NOT..BUT, Converse abjunction
+ * 
+ * Creates a chain where any condition must be less
+ * satisfied than the condition left to it (xs[0] > xs[1])
+ * 
+ * 0 ↚ 0 = 0
+ * 0 ↚ 1 = 1
+ * 1 ↚ 0 = 0
+ * 1 ↚ 1 = 0
+ * 
+ * Properties:
+ * -  Vacuous falsity
+ * -  Identity singleton
+ * -  Non-commutative
+ * -  Left-associative: A ↚ B ↚ C = (A ↚ B) ↚ C ≠ A ↚ (B ↚ C)
+ * -  Complemented by right ⊤
+ * -  Dominated by right ⊥
+ * -  Left truth results in contradiction
+ * -  ⊥ as left identity
+ * -  Contrapositivity: A ↚ B = ¬B ↚ ¬A
+ * -  Antireflexive: A ↚ A = ⊥
+ * -  Left-distributive: A ↚ (B ↚ C) = (A ↚ B) ↚ (A ↚ C)
+ * -  Distributive over right AND
+ * -  Distributive over right OR
+ * -  Distributing over left AND changes AND to OR
+ * -  Distributing over left OR changes OR to AND
+ * -  A ↚ B is reduced to ¬A ∧ B in negation normal form
+ * 
+ * Commonly written "↚", "⇍", "!<-", "<-~", "</-", "!<=", "<=~", "</=", "⊄", "⭉" (or "←̃"), or ">"
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective NIF; this can be any number
+ *              of arguments, even none; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_NIF
+ * @seealso  libnormalform_nif_checked
+ * @seealso  libnormalform_nifl_checked
+ * @seealso  libnormalform_vnif_checked
+ * @seealso  libnormalform_nifl
+ * @seealso  libnormalform_vnif
+ * @seealso  libnormalform_nif2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_nif)(LIBNORMALFORM_SENTENCE **xs);
+
+
+/**
+ * NIMPLY: Material nonimplication
+ * 
+ * Also known as NIMPLIES, BUT NOT or Material abjunction
+ * 
+ * Creates a chain where any condition must be more
+ * satisfied than the condition left to it (xs[0] < xs[1])
+ * 
+ * 0 ↛ 0 = 0
+ * 0 ↛ 1 = 0
+ * 1 ↛ 0 = 1
+ * 1 ↛ 1 = 0
+ * 
+ * Properties:
+ * -  Identity singleton
+ * -  Non-commutative
+ * -  Right-associative: A ↛ B ↛ C = A ↛ (B ↛ C) ≠ (A ↛ B) → C
+ * -  Complemented by left ⊤
+ * -  Dominated by left ⊥
+ * -  Right truth results in contradiction
+ * -  ⊥ as right identity
+ * -  Contrapositivity: A ↛ B = ¬B ↛ ¬A
+ * -  Antireflexive: A ↛ A = ⊥
+ * -  Right-distributive: (A ↛ B) ↛ C = (A ↛ C) ↛ (B → C)
+ * -  Distributive over left AND
+ * -  Distributive over left OR
+ * -  Distributing over right AND changes AND to OR
+ * -  Distributing over right OR changes OR to AND
+ * -  A ↛ B is reduced to A ∧ ¬B in negation normal form
+ * 
+ * Commonly written "↛", "⇏", "!->", "->~", "-/>", "!=>", "=>~", "=/>", "⊅", "⥲" (or "→̃"), or "<"
+ * 
+ * @param   xs  `NULL`-terminated list of sentences that should be
+ *              joined by the connective NIMPLY; this can be any positive
+ *              number of arguments; ownership of object in the array
+ *              (but not the array itself) is transfered to this function
+ * @return      The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * @throws  EDOM    `xs` contains no term (but only `NULL`)
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * @seealso  LIBNORMALFORM_NIMPLY
+ * @seealso  libnormalform_nimply_checked
+ * @seealso  libnormalform_nimplyl_checked
+ * @seealso  libnormalform_vnimply_checked
+ * @seealso  libnormalform_nimplyl
+ * @seealso  libnormalform_vnimply
+ * @seealso  libnormalform_nimply2
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+LIBNORMALFORM_SENTENCE *(libnormalform_nimply)(LIBNORMALFORM_SENTENCE **xs);
+
+
+
+
+
+/**
+ * THERE EXISTS: Existential quantification (unmapped)
+ * 
+ * The predicate must be met for at least one element;
+ * if no element exists, the sentence is false
+ * 
+ * Commonly written "∃" ("∃x∈d.k", "∃x∈d k(x)", or "∃ x∈d : k(x)")
+ * 
+ * The predicate is tested on `.key` in each element
+ * in the domain, and `.value` is unused
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   k  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `k` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `k` to
+ * be `NULL`)
+ * 
+ * @seealso  libnormalform_any
+ * @seealso  libnormalform_existentially
+ * @seealso  libnormalform_nexists
+ * @seealso  libnormalform_unique
+ * @seealso  libnormalform_nonempty
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_exists)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k)
+{ return libnormalform_any(d, k, libnormalform_true()); }
+
+
+/**
+ * THERE EXISTS NO: Negated existential quantification (unmapped)
+ * 
+ * The predicate must be unmet for every element;
+ * if no element exists, the sentence is true
+ * 
+ * Commonly written "∄" ("∄x∈d.k", "∄x∈d k(x)", or "∄ x∈d : k(x)"),
+ * "~∃", "¬∃", or as THERE EXISTS with overline
+ * 
+ * The predicate is tested on `.key` in each element
+ * in the domain, and `.value` is unused
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   k  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `k` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `k` to
+ * be `NULL`)
+ * 
+ * @seealso  libnormalform_all
+ * @seealso  libnormalform_exists
+ * @seealso  libnormalform_empty
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nexists)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k)
+{ return libnormalform_all(d, k, libnormalform_false()); }
+
+
+/**
+ * THERE EXISTS ONE: Unique existential quantification (unmapped)
+ * 
+ * The predicate must be met for exactly one element;
+ * if no element exists, the sentence is false
+ * 
+ * Commonly written "∃!" ("∃!x∈d.k", "∃!x∈d k(x)", or "∃! x∈d : k(x)")
+ * 
+ * The predicate is tested on `.key` in each element
+ * in the domain, and `.value` is unused
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   k  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `k` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `k` to
+ * be `NULL`)
+ * 
+ * @seealso  libnormalform_one
+ * @seealso  libnormalform_uniquely
+ * @seealso  libnormalform_exists
+ * @seealso  libnormalform_singleton
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_unique)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k)
+{ return libnormalform_one(d, k, libnormalform_true()); }
+
+
+
+
+
+/**
+ * SOMEWHERE: Existential quantification (premapped)
+ * 
+ * The predicate must be met for at least one element;
+ * if no element exists, the sentence is false
+ * 
+ * Commonly written "∃" ("∃x∈d.v", "∃x∈d v(x)", or "v(x) ∃ x∈d")
+ * 
+ * The predicate is tested on `.value` in each element
+ * in the domain, and `.key` is unused
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   v  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `v` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `v` to
+ * be `NULL`)
+ * 
+ * @seealso  libnormalform_any
+ * @seealso  libnormalform_exists
+ * @seealso  libnormalform_universally
+ * @seealso  libnormalform_uniquely
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_existentially)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v)
+{ return libnormalform_any(d, libnormalform_true(), v); }
+
+
+/**
+ * EVERYWHERE: Universal quantification (premapped)
+ * 
+ * The predicate must be unmet for every element;
+ * if no element exists, the sentence is true
+ * 
+ * Commonly written "∀" ("∀x∈d.v", "∀x∈d v(x)", or "v(x) ∀ x∈d")
+ * 
+ * The predicate is tested on `.value` in each element
+ * in the domain, and `.key` is unused
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   v  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `v` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `v` to
+ * be `NULL`)
+ * 
+ * @seealso  libnormalform_all
+ * @seealso  libnormalform_existentially
+ * @seealso  libnormalform_uniquely
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_universally)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v)
+{ return libnormalform_all(d, libnormalform_true(), v); }
+
+
+/**
+ * ONEWHERE: Unique existential quantification (premapped)
+ * 
+ * The predicate must be met for exactly one element;
+ * if no element exists, the sentence is false
+ * 
+ * Commonly written "∃!" ("∃!x∈d.v", "∃!x∈d v(x)", or "v(x) ∃! x∈d")
+ * 
+ * The predicate is tested on `.value` in each element
+ * in the domain, and `.key` is unused
+ * 
+ * @param   d  The domain of interest; ownership is retained by the caller
+ * @param   v  The predicate; ownership is transfered to this function
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * Ownership is always transfered, even on failure
+ * 
+ * If `v` is `NULL`, this function will return `NULL`
+ * (indicating failure) without modified `errno` (expecting
+ * it to be set by a function that failed, causing `v` to
+ * be `NULL`)
+ * 
+ * @seealso  libnormalform_one
+ * @seealso  libnormalform_unique
+ * @seealso  libnormalform_existentially
+ * @seealso  libnormalform_universially
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_uniquely)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v)
+{ return libnormalform_one(d, libnormalform_true(), v); }
+
+
+
+
+
+/**
+ * Create a sentence that checks whether a set is empty
+ *
+ * The sentence technically classifies as a qualification
+ * 
+ * Commonly written "X=∅" or "|X|=0"
+ * 
+ * @param   d  The set; ownership is retained by the caller
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * @seealso  libnormalform_nonempty
+ * @seealso  libnormalform_singleton
+ * @seealso  libnormalform_nexists
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_empty)(struct libnormalform_map *d)
+{ return libnormalform_all(d, libnormalform_true(), libnormalform_false()); }
+
+
+/**
+ * Create a sentence that checks whether a set is non-empty
+ *
+ * The sentence technically classifies as a qualification
+ * 
+ * Commonly written "X≠∅", "X⊃∅", "X⊋∅" "|X|≠0", or "|X|>0"
+ * 
+ * @param   d  The set; ownership is retained by the caller
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * @seealso  libnormalform_empty
+ * @seealso  libnormalform_singleton
+ * @seealso  libnormalform_exists
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nonempty)(struct libnormalform_map *d)
+{ return libnormalform_any(d, libnormalform_true(), libnormalform_true()); }
+
+
+/**
+ * Create a sentence that checks whether a set is a singleton
+ * (contains exactly one element)
+ *
+ * The sentence technically classifies as a qualification
+ * 
+ * Commonly written "|X|=1", "∃! x : X={x}", "X={x} ∃! x", or just "X={x}"
+ * 
+ * @param   d  The set; ownership is retained by the caller
+ * @return     The constructed sentence, `NULL` on failure
+ * 
+ * @throws  ENOMEM  Insufficient memory available to create the sentence
+ * 
+ * @seealso  libnormalform_empty
+ * @seealso  libnormalform_nonempty
+ * @seealso  libnormalform_unique
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_singleton)(struct libnormalform_map *d)
+{ return libnormalform_one(d, libnormalform_true(), libnormalform_true()); }
+
+
+
+
+
+/**
+ * Variant of `libnormalform_and` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_and`
+ * @return      See `libnormalform_and`
+ * @throws      See `libnormalform_and`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_and_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(and) }
+
+
+/**
+ * Variant of `libnormalform_or` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_or`
+ * @return      See `libnormalform_or`
+ * @throws      See `libnormalform_or`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_or_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(or) }
+
+
+/**
+ * Variant of `libnormalform_xor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_xor`
+ * @return      See `libnormalform_xor`
+ * @throws      See `libnormalform_xor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(xor) }
+
+
+/**
+ * Variant of `libnormalform_if` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_if`
+ * @return      See `libnormalform_if`
+ * @throws      See `libnormalform_if`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_if_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(if) }
+
+
+/**
+ * Variant of `libnormalform_imply` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_imply`
+ * @return      See `libnormalform_imply`
+ * @throws      See `libnormalform_imply`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_imply_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(imply) }
+
+
+/**
+ * Variant of `libnormalform_nand` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_nand`
+ * @return      See `libnormalform_nand`
+ * @throws      See `libnormalform_nand`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nand_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(nand) }
+
+
+/**
+ * Variant of `libnormalform_nor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_nor`
+ * @return      See `libnormalform_nor`
+ * @throws      See `libnormalform_nor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(nor) }
+
+
+/**
+ * Variant of `libnormalform_xnor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_xnor`
+ * @return      See `libnormalform_xnor`
+ * @throws      See `libnormalform_xnor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xnor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(xnor) }
+
+
+/**
+ * Variant of `libnormalform_nif` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_nif`
+ * @return      See `libnormalform_nif`
+ * @throws      See `libnormalform_nif`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nif_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(nif) }
+
+
+/**
+ * Variant of `libnormalform_nimply` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n   The number of expected non-`NULL` terms
+ * @param   xs  See `libnormalform_nimply`
+ * @return      See `libnormalform_nimply`
+ * @throws      See `libnormalform_nimply`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nimply_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
+{ LIBNORMALFORM_CHECKED__(nimply) }
+
+
+
+
+
+/**
+ * Variant of `libnormalform_andl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_andl`
+ * @throws           See `libnormalform_andl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vand)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(and) }
+
+
+/**
+ * Variant of `libnormalform_orl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_orl`
+ * @throws           See `libnormalform_orl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vor)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(or) }
+
+
+/**
+ * Variant of `libnormalform_xorl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_xorl`
+ * @throws           See `libnormalform_xorl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vxor)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(xor) }
+
+
+/**
+ * Variant of `libnormalform_ifl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_ifl`
+ * @throws           See `libnormalform_ifl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vif)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(if) }
+
+
+/**
+ * Variant of `libnormalform_implyl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_implyl`
+ * @throws           See `libnormalform_implyl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vimply)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(imply) }
+
+
+/**
+ * Variant of `libnormalform_nandl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_nandl`
+ * @throws           See `libnormalform_nandl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnand)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(nand) }
+
+
+/**
+ * Variant of `libnormalform_norl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_norl`
+ * @throws           See `libnormalform_norl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnor)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(nor) }
+
+
+/**
+ * Variant of `libnormalform_xnorl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_xnorl`
+ * @throws           See `libnormalform_xnorl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vxnor)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(xnor) }
+
+
+/**
+ * Variant of `libnormalform_nifl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_nifl`
+ * @throws           See `libnormalform_nifl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnif)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(nif) }
+
+
+/**
+ * Variant of `libnormalform_nimplyl` that uses `va_list`
+ * instead of variadic arguments
+ * 
+ * @param   a, args  `NULL`-terminated list of terms; the function
+ *                   will take ownership of each input reference,
+ *                   so the caller shall not attempt to deallocate
+ *                   or use them again.
+ * @return           See `libnormalform_nimplyl`
+ * @throws           See `libnormalform_nimplyl`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnimply)(LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST__(nimply) }
+
+
+
+
+
+/**
+ * Variant of `libnormalform_and` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_and`
+ * @throws          See `libnormalform_and`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_andl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(and) }
+
+
+/**
+ * Variant of `libnormalform_or` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_or`
+ * @throws          See `libnormalform_or`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_orl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(or) }
+
+
+/**
+ * Variant of `libnormalform_xor` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_xor`
+ * @throws          See `libnormalform_xor`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xorl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(xor) }
+
+
+/**
+ * Variant of `libnormalform_if` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_if`
+ * @throws          See `libnormalform_if`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_ifl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(if) }
+
+
+/**
+ * Variant of `libnormalform_imply` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_imply`
+ * @throws          See `libnormalform_imply`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_implyl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(imply) }
+
+
+/**
+ * Variant of `libnormalform_nand` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nand`
+ * @throws          See `libnormalform_nand`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nandl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(nand) }
+
+
+/**
+ * Variant of `libnormalform_nor` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nor`
+ * @throws          See `libnormalform_nor`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_norl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(nor) }
+
+
+/**
+ * Variant of `libnormalform_xnor` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_xnor`
+ * @throws          See `libnormalform_xnor`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xnorl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(xnor) }
+
+
+/**
+ * Variant of `libnormalform_nif` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nif`
+ * @throws          See `libnormalform_nif`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nifl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(nif) }
+
+
+/**
+ * Variant of `libnormalform_nimply` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nimply`
+ * @throws          See `libnormalform_nimply`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nimplyl)(LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS__(nimply) }
+
+
+
+
+
+/**
+ * Variant of `libnormalform_vand` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vand`
+ * @return           See `libnormalform_vand`
+ * @throws           See `libnormalform_vand`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vand_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(and) }
+
+
+/**
+ * Variant of `libnormalform_vor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vor`
+ * @return           See `libnormalform_vor`
+ * @throws           See `libnormalform_vor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(or) }
+
+
+/**
+ * Variant of `libnormalform_vxor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vxor`
+ * @return           See `libnormalform_vxor`
+ * @throws           See `libnormalform_vxor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vxor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(xor) }
+
+
+/**
+ * Variant of `libnormalform_vif` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vif`
+ * @return           See `libnormalform_vif`
+ * @throws           See `libnormalform_vif`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vif_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(if) }
+
+
+/**
+ * Variant of `libnormalform_vimply` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vimply`
+ * @return           See `libnormalform_vimply`
+ * @throws           See `libnormalform_vimply`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vimply_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(imply) }
+
+
+/**
+ * Variant of `libnormalform_vnand` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vnand`
+ * @return           See `libnormalform_vnand`
+ * @throws           See `libnormalform_vnand`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnand_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(nand) }
+
+
+/**
+ * Variant of `libnormalform_vnor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vnor`
+ * @return           See `libnormalform_vnor`
+ * @throws           See `libnormalform_vnor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(nor) }
+
+
+/**
+ * Variant of `libnormalform_vxnor` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vxnor`
+ * @return           See `libnormalform_vxnor`
+ * @throws           See `libnormalform_vxnor`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vxnor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(xnor) }
+
+
+/**
+ * Variant of `libnormalform_vnif` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vnif`
+ * @return           See `libnormalform_vnif`
+ * @throws           See `libnormalform_vnif`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnif_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(nif) }
+
+
+/**
+ * Variant of `libnormalform_vnimply` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n        The number of expected non-`NULL` terms
+ * @param   a, args  See `libnormalform_vnimply`
+ * @return           See `libnormalform_vnimply`
+ * @throws           See `libnormalform_vnimply`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_vnimply_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
+{ LIBNORMALFORM_VALIST_CHECKED__(nimply) }
+
+
+
+
+
+/**
+ * Variant of `libnormalform_andl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_andl`
+ * @return          See `libnormalform_andl`
+ * @throws          See `libnormalform_andl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_andl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(and) }
+
+
+/**
+ * Variant of `libnormalform_orl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_orl`
+ * @return          See `libnormalform_orl`
+ * @throws          See `libnormalform_orl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_orl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(or) }
+
+
+/**
+ * Variant of `libnormalform_xorl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_xorl`
+ * @return          See `libnormalform_xorl`
+ * @throws          See `libnormalform_xorl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xorl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(xor) }
+
+
+/**
+ * Variant of `libnormalform_ifl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_ifl`
+ * @return          See `libnormalform_ifl`
+ * @throws          See `libnormalform_ifl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_ifl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(if) }
+
+
+/**
+ * Variant of `libnormalform_implyl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_implyl`
+ * @return          See `libnormalform_implyl`
+ * @throws          See `libnormalform_implyl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_implyl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(imply) }
+
+
+/**
+ * Variant of `libnormalform_nandl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_nandl`
+ * @return          See `libnormalform_nandl`
+ * @throws          See `libnormalform_nandl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nandl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nand) }
+
+
+/**
+ * Variant of `libnormalform_norl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_norl`
+ * @return          See `libnormalform_norl`
+ * @throws          See `libnormalform_norl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_norl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nor) }
+
+
+/**
+ * Variant of `libnormalform_xnorl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_xnorl`
+ * @return          See `libnormalform_xnorl`
+ * @throws          See `libnormalform_xnorl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xnorl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(xnor) }
+
+
+/**
+ * Variant of `libnormalform_nifl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_nifl`
+ * @return          See `libnormalform_nifl`
+ * @throws          See `libnormalform_nifl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nifl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nif) }
+
+
+/**
+ * Variant of `libnormalform_nimplyl` that checks
+ * for unexpected `NULL` input
+ *
+ * @param   n       The number of expected non-`NULL` terms
+ * @param   a, ...  See `libnormalform_nimplyl`
+ * @return          See `libnormalform_nimplyl`
+ * @throws          See `libnormalform_nimplyl`
+ * 
+ * If the function finds any unexpected `NULL` terms,
+ * it will call `libnormalform_free` on all non-`NULL` terms
+ * and return `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nimplyl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
+{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nimply) }
+
+
+
+
+
+/**
+ * Variant of `libnormalform_and` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_and`
+ * @throws     See `libnormalform_and`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_and2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);
+
+
+/**
+ * Variant of `libnormalform_or` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_or`
+ * @throws     See `libnormalform_or`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_or2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);
+
+
+/**
+ * Variant of `libnormalform_xor` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_xor`
+ * @throws     See `libnormalform_xor`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+LIBNORMALFORM_SENTENCE *(libnormalform_xor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);
+
+
+/**
+ * Variant of `libnormalform_if` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_if`
+ * @throws     See `libnormalform_if`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_if2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(if) }
+
+
+/**
+ * Variant of `libnormalform_imply` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_imply`
+ * @throws     See `libnormalform_imply`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_imply2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(imply) }
+
+
+/**
+ * Variant of `libnormalform_nand` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_nand`
+ * @throws     See `libnormalform_nand`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nand2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(nand) }
+
+
+/**
+ * Variant of `libnormalform_nor` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_nor`
+ * @throws     See `libnormalform_nor`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(nor) }
+
+
+/**
+ * Variant of `libnormalform_xnor` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_xnor`
+ * @throws     See `libnormalform_xnor`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_xnor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(xnor) }
+
+
+/**
+ * Variant of `libnormalform_nif` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_nif`
+ * @throws     See `libnormalform_nif`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nif2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(nif) }
+
+
+/**
+ * Variant of `libnormalform_nimply` that takes exactly two terms
+ *
+ * @param   l  The left-hand term
+ * @param   r  The right-hand term
+ * @return     See `libnormalform_nimply`
+ * @throws     See `libnormalform_nimply`
+ * 
+ * If `l` or `r` is `NULL`, the function will call
+ * `libnormalform_free` on both arguments and return
+ * `NULL` (indicating failure) without setting
+ * `errno` (expected to already be set in indicate the
+ * error that caused one of the terms to be `NULL`)
+ */
+LIBNORMALFORM_USE_RESULT__
+inline LIBNORMALFORM_SENTENCE *
+(libnormalform_nimply2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
+{ LIBNORMALFORM_TWO__(nimply) }
+
+
+
+
+
+/* These are macro versions of function with the same name */
+
+/**
+ * Variant of `libnormalform_and` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_and`
+ * @throws          See `libnormalform_and`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_andl(...) (libnormalform_and((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_or` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_or`
+ * @throws          See `libnormalform_or`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_orl(...) (libnormalform_or((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_xor` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_xor`
+ * @throws          See `libnormalform_xor`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_xorl(...) (libnormalform_xor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_if` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_if`
+ * @throws          See `libnormalform_if`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_ifl(...) (libnormalform_if((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_imply` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_imply`
+ * @throws          See `libnormalform_imply`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_implyl(...) (libnormalform_imply((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_nand` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nand`
+ * @throws          See `libnormalform_nand`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_nandl(...) (libnormalform_nand((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_nor` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nor`
+ * @throws          See `libnormalform_nor`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_norl(...) (libnormalform_nor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_xnor` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_xnor`
+ * @throws          See `libnormalform_xnor`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_xnorl(...) (libnormalform_xnor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_nif` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nif`
+ * @throws          See `libnormalform_nif`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_nifl(...) (libnormalform_nif((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+/**
+ * Variant of `libnormalform_nimply` that uses variadic arguments
+ * 
+ * @param   a, ...  `NULL`-terminated list of terms; the function
+ *                  will take ownership of each input reference,
+ *                  so the caller shall not attempt to deallocate
+ *                  or use them again.
+ * @return          See `libnormalform_nimply`
+ * @throws          See `libnormalform_nimply`
+ * 
+ * Be careful not in inputing any `NULL` apart from
+ * the list terminator as the function will not be
+ * able to see them.
+ */
+#define libnormalform_nimplyl(...) (libnormalform_nimply((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))
+
+
+
+
+
+/**
+ * Macro variant of `libnormalform_andl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_andl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_AND(...) LIBNORMALFORM_MACRO__(and, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_orl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_orl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_OR(...) LIBNORMALFORM_MACRO__(or, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_xorl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_xorl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_XOR(...) LIBNORMALFORM_MACRO__(xor, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_ifl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_ifl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_IF(...) LIBNORMALFORM_MACRO__(if, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_implyl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_implyl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_IMPLY(...) LIBNORMALFORM_MACRO__(imply, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_nandl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_nandl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_NAND(...) LIBNORMALFORM_MACRO__(nand, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_norl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_norl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_NOR(...) LIBNORMALFORM_MACRO__(nor, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_xnorl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_xnorl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_XNOR(...) LIBNORMALFORM_MACRO__(xnor, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_nifl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_nifl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_NIF(...) LIBNORMALFORM_MACRO__(nif, __VA_ARGS__)
+
+
+/**
+ * Macro variant of `libnormalform_nimplyl_checked`, that
+ * will add the `NULL` to the end of the list and, before
+ * the list, the number of terms in the list
+ * 
+ * @param   ...  List of terms, _without_ `NULL`-terinator
+ * @return       See `libnormalform_nimplyl_checked`
+ *
+ * Either any argument is `NULL`, `libnormalform_free` on
+ * will be called for all non-`NULL` terms, the `NULL`
+ * with be return (indicating failure) without `errno`
+ * being modified (it is expected to already be set in
+ * indicate the error that caused one of the terms to be
+ * `NULL`)
+ */
+#define LIBNORMALFORM_NIMPLY(...) LIBNORMALFORM_MACRO__(nimply, __VA_ARGS__)
+
+
+
+
+
+#undef LIBNORMALFORM_CHECKED__
+#undef LIBNORMALFORM_VALIST__
+#undef LIBNORMALFORM_ELLIPSIS__
+#undef LIBNORMALFORM_VALIST_CHECKED__
+#undef LIBNORMALFORM_ELLIPSIS_CHECKED__
+#undef LIBNORMALFORM_TWO__
+
+#undef LIBNORMALFORM_USE_RESULT__
+#undef LIBNORMALFORM_FREE_WITH__
+#undef LIBNORMALFORM_USE_FREE__
+#undef LIBNORMALFORM_NONNULL_INPUT__
+#undef LIBNORMALFORM_ONE_NONNULL_INPUT__
+#undef LIBNORMALFORM_NULL_LAST__
+
+
+#if defined(__GNUC__)
+# pragma GCC diagnostic pop
+#endif
+
+#endif