Free variable in a Formula or iteration variable in a Set or constant.

Creates a constant with a given value

Creates a variable with a given name.

Returns the name of the variable.

First order formula with free variables and relations between variables.

Creates the tautology formula.

Creates the contradiction formula.

Creates a formula based on a given Bool value.

Creates a logical conjunction of two given formulas, e.g.

f /\ false == false
f /\ true  == f
f /\ g     == g /\ f

Creates a logical conjunction of a given list of formulas.

Creates a logical disjunction of two given formulas, e.g.

f \/ true  == true
f \/ false == f
f \/ g     == g \/ f

Creates a logical disjunction of a given list of formulas.

Creates a negation of a given formula, e.g.

not true    == false
not false   == true
not (not f) == f

Creates an implication of given formulas, e.g.

false ==> f    == true
f     ==> true == true
f     ==> g    == g <== f

Creates an implication of given formulas, e.g.

f    <== false == true
true <== f     == true
f    <== g     == g ==> f

Creates a implication of given formulas, equivalent to ==>.

Creates a formula representing "if and only if" relation between given formulas, e.g.

f <==> f     == true
f <==> not f == false
f <==> g     == (f /\ g \/ not f /\ not g)

Equivalent to <==>.

Creates a formula representing ∃x.f

Equivalent to existsVar.

Creates a formula representing ∀x.f

Equivalent to forAllVars.

Checks whether the formula is a tautology.

Checks whether the formula is a contradiction.

Simplify given formula.

Returns:

• Just True if formula is a tautology,
• Just False if formula is a contradiction,
• Nothing otherwise.

Variables scope.

Map function for variables from a scope.

Fold function for variables from a scope.

Basic type in NLambda required by most of functions in the module (without Ord class).

Basic type in NLambda required by most of functions in the module.

Checks whether two elements are not equivalent.

Class of types implementing conditional statements.

if ... then ... else ... with condition solving.

Class of types of expressions to evaluating with a given context.

Evaluates an expression in the context of a true formula. In practice all formulas in expressions are solved.

simplify = when true

Storing values under various conditions, which could not be solved as true or false. Is often the result of ite or iteV functions.

Creates a single variant.

Returns value of a single variant.

If ... then ... else ... for types that are not instances of Conditional class.

Variants of variables.

Creates atom with the given name.

Creates atom representing given constant

Creates a formula that describes the "<" relation between given atoms.

lt a a == false
lt a b == gt b a

Creates a formula that describes the "≤" relation between given atoms.

le a a == true
le a b == ge b a

Creates a formula that describes the ">" relation between given atoms.

gt a a == false
gt a b == lt b a

Creates a formula that describes the "≥" relation between given atoms.

ge a a == true
ge a b == le b a

Space with free atoms names.

Creates a new atom with a previously unused name.

Evaluates given value having newAtom commands.

Variants of Either values.

Creates a single variant with a Left value.

Creates a single variant with a Right value.

Transforms Left variants to values variants, crashes if variants contain a Right value.

Transforms Right variants to values variants, crashes if variants contain a Left value.

Transforms Either variants to values variants.

Returns a formula describing the condition of occurrence of Left values in variants.

Returns a formula describing the condition of occurrence of Right values in variants.

Variants of Maybe values.

Creates a single variant with Nothing.

Creates a single variant with Just value.

Transforms Just variants to values variants, crashes if variants contain a Nothing value.

Takes a default value and Maybe variants and returns a variants of values from Just and default value instead of Nothing.

Takes a default value, function and Maybe variants and applies function to the values inside the Just or returns the default value instead of Nothing.

Returns a condition under which the variants have a Just value.

Returns a condition under which the variants have a Nothing value.

If a given condition is satisfied returns Just value otherwise returns Nothing.

The set of elements, can be infinite.

Returns an empty set.

Returns the set of all atoms.

Create a set from a list of elements.

Create a set with one given element.

Insert an element to a set.

Insert all elements from a list to a set.

Delete an element from a set.

Delete all elements from a list from a set.

Checks whether the set is empty.

Checks whether the set is not empty.

Applies function to all elements of a set and returns a new set.

Filter all elements that satisfy the predicate.

Applies function to all elements of a set and extract value from Just results and remove elements with Nothing results.

For a set of sets returns the union of these sets.

Returns a formula describing the membership of an element that satisfy the predicate.

Returns a formula describing the condition that all elements of a set satisfy the predicate.

Partition the set into two sets, one with all elements that satisfy the predicate and one with all elements that don't satisfy the predicate.

Returns a formula describing the membership of an element in a set.

Returns a formula describing the lack of an element in a set.

Returns a formula describing the membership of an element in a set.

Returns a formula describing the lack of an element in a set.

Returns a formula describing that the first set is a subset of the second set.

Returns a formula describing that the first set is not a subset of the second set.

Returns a formula describing that the first set is a proper subset of the second set.

Returns a formula describing that the first set is not a proper subset of the second set.

Returns union of two given sets.

Returns union of sets from a list.

Returns an intersetion of two sets.

Checks whether two sets intersect.

Checks whether two sets are disjoint.

Returns a difference of two sets.

See difference.

Creates a set of pairs of elements from two sets.

Creates a set of results of applying a function to elements from two sets.

The composition of pairsWith and mapFilter.

Creates a set of all pairs of elements from a set.

Creates a set of all atoms pairs.

Creates a set of all pairs of different atoms.

Creates a set of triples of elements from three sets.

Creates a set of results of applying a function to elements from three sets.

The composition of triplesWith and mapFilter.

Creates a set of all atoms triples.

Applies a function to all lists of elements from a list of sets, e.g.

>>> mapList id [atoms, fromList [a,b]]
{[a₁,a] : for a₁ ∊ 𝔸, [a₁,b] : for a₁ ∊ 𝔸}

Creates a set of lists of a given length of elements from a set, e.g.

>>> replicateSet 3 atoms
{[a₁,a₂,a₃] : for a₁,a₂,a₃ ∊ 𝔸}

Creates a set of lists up to a given length of elements from a set, e.g.

>>> replicateSetUntil 3 atoms
{[], [a₁] : for a₁ ∊ 𝔸, [a₁,a₂] : for a₁,a₂ ∊ 𝔸, [a₁,a₂,a₃] : for a₁,a₂,a₃ ∊ 𝔸}

replicateAtoms n = replicateSet n atoms

replicateAtomsUntil n = replicateSetUntil n atoms

Returns a formula describing condition that a set has a size less than a given number. It is an inefficient function for large sets and will not return the answer for the infinite sets.

Returns a formula describing condition that a set has a given size. It is an inefficient function for large sets and will not return the answer for the infinite sets.

Returns a variants of numbers of the size of a list.

Returns a variants of numbers of the size of a list with given equality relation.

Returns the maximum size of a list for all free atoms constraints.

Returns the maximum size of a list for all free atoms constraints with given equality relation.

Returns a variants of numbers of the size of a set. It is an inefficient function for large sets and will not return the answer for the infinite sets.

Returns a variants of numbers of the size of a set with given equality relation. It will not return the answer for the infinite sets.

Returns the maximum size of a set for all free atoms constraints. It is an inefficient function for large sets and will not return the answer for the infinite sets.

Returns the maximum size of a set for all free atoms constraints with given equality relation. It will not return the answer for the infinite sets.

Returns a formula describing condition that a set has exacly one element.

The closed interval of atoms with given minimum and maximum.

The open interval of atoms with given infimum and suprememum.

Checks whether a given atom is the lower bound of a set.

Checks whether a set has the lower bound.

Checks whether a given atom is the upper bound of a set.

Checks whether a set has the upper bound.

Checks whether an atom is the minimum of a set.

Checks whether a set has the minimum.

Checks whether an atom is the maximum of a set.

Checks whether a set has the maximum.

Checks whether an atom is the infumum of a set.

Checks whether an atom is the supremum of a set.

Checks whether a set is connected.

Checks whether a set is open.

Checks whether a set is closed.

Checks whether a set is compact.

Returns all free atoms of an element. The result list is also support of an element, but not always the least one.

Returns the least support of an element. From the result of support function it removes atoms and check if it is still support.

Checks whether a list of atoms supports an element.

Checks whether an element is equivariant, i.e. it has empty support.

Applies permutations of atoms to all atoms in an element.

Returns an orbit of an element with a given support.

For a given list of atoms and a set returns the closure of the set under all automorphisms of atoms that fix every element of the list.

Returns an orbit of an element in a set.

Returns all orbits of a set.

Returns a number of orbits of a set. It uses size function which is inefficient for large sets and will not return the answer for the infinite sets.

Returns a maximum number of orbits of a set. It uses maxSize function which is inefficient for large sets and will not return the answer for the infinite sets.

Checks whether two elements are in the same orbit with a given support.

Checks whether two elements are in the same orbit of a set.

Returns a set of all equivariant subsets of a given set

A directed graph with vertices of type a and set of pairs representing edges.

A graph constructor.

An empty graph.

A graph with atoms vertices.

An empty graph with an Atom type of vertices.

A graph with complete set of edges. Every pair of vertices are connected.

A complete graph with atoms vertices.

A clique without loops.

A clique with atoms vertices and without loops.

A group with atoms vertices where two atoms are connected if the first one is smaller than the second one.

Adds vertex to a graph.

Removes vertex from a graph.

Adds an edge to a graph

Removes an edge from a graph

Add loops for all vertices in a graph.

Removes all loops from a graph.

Reverses all edges in a graph.

Produces a set of edges containing edges that are obtained by composition of edges in a given set.

Produces a graph with edges that are obtained by composition of edges in a given graph.

Adds all reverse edges to existing edges in a graph.

Returns a subgraph limited to a set of vertices.

Checks whether a graph has a loop.

Checks whether a graph does not have a loop

Checks whether a graph has a given edge.

Returns all predecessors of a vertex.

Returns all successors of a vertex.

Returns all neighbours of an element in a graph.

Returns a transitive closure of a graph.

Checks whether there is a path from one vertex to the second one in a graph.

Checks whether a graph is strongly connected.

Checks whether a graph is weakly connected.

Checks whether a graph has a cycle.

Checks whether a graph has a even-length cycle.

Checks whether a graph has a odd-length cycle.

Checks whether a graph (treated as undirected) is bipartite in the sense that it does not have odd-length cycle

Returns all vertices reachable from a vertex in a graph.

Returns all vertices reachable from a set of vertices in a graph.

Returns a weakly connected component of a graph containing a vertex.

Returns all weakly connected components of a graph.

Returns a strongly connected component of a graph containing a vertex.

Returns all strongly connected components of a graph.

Checks whether a given function is the proper coloring of a graph.

Checks whether a graph has an equivariant k-coloring.

An automaton with a set of state with type q accepting/rejecting words from an alphabet with type a.

An automaton constructor.

An automaton constructor with additional not accepting state.

Checks whether an automaton accepts a word.

Checks whether an automaton accepts any word.

Checks whether an automaton rejects all words.

Returns an automaton that accepts the union of languages accepted by two automata.

Returns an automaton that accepts the intersection of languages accepted by two automata.

Returns a minimal automaton accepting the same language as a given automaton.

The constructor of a deterministic automaton.

The constructor of a deterministic automaton with additional not accepting state.

The constructor of a deterministic automaton with atoms as states.

The constructor of a deterministic automaton with atoms as states with additional not accepting state.

Checks whether an automaton is deterministic.

Returns a deterministic automaton that accepts the union of languages accepted by two deterministic automata.

Returns a deterministic automaton that accepts only words rejected by a given automaton.

Returns a deterministic automaton that accepts only words accepted by the first automaton and rejeceted by the second.

Checks whether two automata accepts the same languages.

The constructor of a nondeterministic automaton.

The constructor of a nondeterministic automaton with additional not accepting state.

The constructor of a nondeterministic automaton with atoms as states.

The constructor of a nondeterministic automaton with atoms as states with additional not accepting state.

Checks whether an automaton is nondeterministic.