graph.cppm File Reference

The graph of a function as a relation: the analytic arrow f and its set of pairs are one object. A graph is a dyadic (binary) relation (functional \(R\subseteq A\times B\) for \(f:A\to B\); an endorelation only when \(A=B\)), so it lives with the relations (dedekind.relational), not in :sets. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <ranges>
#include <type_traits>
#include <utility>
import dedekind.relational:dyadic;
import dedekind.sets;
import dedekind.category;

Include dependency graph for graph.cppm:

Classes
struct	dedekind::relational::GraphPredicate< F >
	The membership predicate of a functional graph \(\Gamma_f\): \((a,b)\mapsto b = f(a)\). More...
struct	dedekind::relational::GraphArrow< A, B, P >
	The arrow a function's graph atom names, the converse of graph: a relation A×B | (π_2 == t) certified a function is the arrow a ↦ t(a), t read at a pair whose first coordinate is a. More...
struct	dedekind::relational::PreimagePredicate< F, S >
	The preimage predicate \(a \mapsto f(a)\in S\): the subobject S pulled back along the functional arrow f ( \(\chi_S\circ f\)). More...
struct	dedekind::relational::Fixed< K, C, c, T >
	The arrow that fixes one factor of a pair: \(x \mapsto (c, x)\) (K = 1) or \(x \mapsto (x, c)\) (K = 2). Substitution along it is one case of Shannon's expansion. More...
struct	dedekind::relational::Image< F, L >
	\(\exists_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the image along \(f : A \to B\): \(a \mapsto f[a] = \{f(x) \mid x \in a\}\). Partial: defined where image_along eliminates the \(\exists\). Monotone; the left adjoint of Preimage. More...
struct	dedekind::relational::Preimage< F, L >
	\(f^{-1} : \mathrm{Sub}(B, L) \to \mathrm{Sub}(A, L)\), substitution along \(f\): \(b \mapsto \{x \mid f(x) \in b\}\) (preimage, \(\chi_b \circ f\)). Total, a lattice homomorphism, monotone; the right adjoint of Image and the left adjoint of Dual. More...
struct	dedekind::relational::Dual< F, L >
	\(\forall_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the dual image: \(a \mapsto \{y \mid \forall x.\ f(x) = y \Rightarrow x \in a\}\), which is \(\neg\,\exists_f\,\neg\) (De Morgan: the logic is an Ockham algebra), a composite of three arrows on presented objects. The right adjoint of Preimage; monotone, as anti∘co∘anti. More...
struct	dedekind::category::monotone_trait< dedekind::relational::Image< F, L >, std::less_equal<> >
	The hyperdoctrine, stated once for every arrow F: the three operations preserve inclusion, and \(\exists_f \dashv f^{-1} \dashv \forall_f\) — \(f[a] \subseteq b \iff a \subseteq f^{-1}(b)\) and \(f^{-1}(b) \subseteq a \iff b \subseteq \forall_f a\) (Lawvere; in Set, for every \(f\)). More...
struct	dedekind::category::monotone_trait< dedekind::relational::Preimage< F, L >, std::less_equal<> >
struct	dedekind::category::monotone_trait< dedekind::relational::Dual< F, L >, std::less_equal<> >
struct	dedekind::category::is_adjoint< dedekind::relational::Image< F, L >, dedekind::relational::Preimage< F, L >, std::less_equal<> >
struct	dedekind::category::is_adjoint< dedekind::relational::Preimage< F, L >, dedekind::relational::Dual< F, L >, std::less_equal<> >
struct	dedekind::relational::detail_hyperdoctrine_witness::Code
struct	dedekind::relational::detail_hyperdoctrine_witness::Seven
struct	dedekind::relational::detail_graph::AgreesAt< R, G, A >
	Whether r and the graph g agree on the pair (a, b). More...
struct	dedekind::relational::detail_graph::AgreesOnRow< R, G, CodRange >
	Whether r and the graph g agree on every pair of the row a: ∀ b ∈ cod. More...
struct	dedekind::relational::detail_hyperdoctrine_witness::Copy< A >
	Copy (comonoid comultiplication) Δ:A→A×A, a↦(a,a). The left adjoint of the meet; the fan-out of a cartesian bicategory. More...
struct	dedekind::relational::detail_hyperdoctrine_witness::Injection< K, A, B >
	The injection ι_K : A → A + B as an arrow: monic (it is injective, and its image is disjoint from the other summand's), the ground of a sum's strength reduction (a set inside one injection's image pulls back along it without loss). More...
struct	dedekind::relational::detail_hyperdoctrine_witness::Inject< K, UA, UB >
	\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict. More...
struct	dedekind::relational::detail_hyperdoctrine_witness::Restrict< K, UA, UB >
	\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::relational::IsFunctional
concept	dedekind::relational::IsEntire
concept	dedekind::relational::IsFunction
concept	dedekind::relational::IsGraph

Typedefs
template<typename F>
using	dedekind::relational::Graph
	Graph<F> — the type of graph(f): the Set<pair> relation \(\Gamma_f=\{(a,b)\mid b=f(a)\}\subseteq A\times B\) of F : A→B.
using	dedekind::relational::detail_hyperdoctrine_witness::P2 = Π<2, std::pair<bool, int>>
using	dedekind::relational::detail_hyperdoctrine_witness::Ex = Image<P2>
using	dedekind::relational::detail_hyperdoctrine_witness::Sb = Preimage<P2>
using	dedekind::relational::detail_hyperdoctrine_witness::Al = Dual<P2>
using	dedekind::relational::detail_hyperdoctrine_witness::Dg = Image<Copy<int>>
using	dedekind::relational::detail_hyperdoctrine_witness::Dr = Preimage<Copy<int>>
using	dedekind::relational::detail_hyperdoctrine_witness::I1 = Injection<1, bool, int>
using	dedekind::relational::detail_hyperdoctrine_witness::Ix = Image<I1>
using	dedekind::relational::detail_hyperdoctrine_witness::Ip = Preimage<I1>
using	dedekind::relational::set_is_function_witness::Five = std::remove_cvref_t<decltype(five)>
template<std::size_t K, typename P>
using	dedekind::relational::detail_hyperdoctrine_witness::Π
	π_k read at the product P, as a MORPHISM (Domain = P, Codomain the k-th part): the building block of IsArrowProduct. Π<0, P> is Identity

Functions
template<typename F> requires dedekind::category::IsArrow<F> && std::equality_comparable<typename std::remove_cvref_t<F>::Codomain>
constexpr Graph< std::remove_cvref_t< F > >	dedekind::relational::graph (F f)
	graph(f) — the graph of a function f : A → B as the Set of pairs \(\{\,(a,b) \mid b = f(a)\,\} \subseteq A\times B\).
template<typename R> requires dedekind::sets::IsGraphAtom<std::remove_cvref_t< decltype(std::declval<const R&>().predicate)>> && IsFunctional<R> && IsEntire<R>
constexpr auto	dedekind::relational::arrow_of (const R &r)
	arrow_of(R): the arrow of a relation certified a function (a graph atom, functional and entire), the converse of graph: graph(arrow_of(R)) is R and arrow_of(graph(f)) is f.
template<typename U, typename F>
constexpr F	dedekind::relational::arrow_of (const Comprehension< U, GraphPredicate< F > > &g)
	arrow_of(graph(f)): the graph keeps its arrow, so it is f itself.
template<typename F, typename G> requires IsFunctional<Graph<F>> && IsFunctional<Graph<G>> && std::same_as<typename F::Codomain, typename G::Domain>
constexpr auto	dedekind::relational::operator>> (const Graph< F > &r, const Graph< G > &s)
	Relative product of two functional relations (graphs), over any intermediate: \(\Gamma_f\,;\,\Gamma_g = \Gamma_{f;g}\).
template<typename F, typename S> requires dedekind::category::IsArrow<F> && (!dedekind::category::IsLSet<std::remove_cvref_t<F>>) && requires(const S& s, const typename std::remove_cvref_t<F>::Codomain& b) { typename std::remove_cvref_t<S>::logic_species; { s(b) } -> std::same_as<typename std::remove_cvref_t<S>::logic_species::Ω>; }
constexpr auto	dedekind::relational::preimage (F f, S s)
	preimage(f, S) = \(\{\,a \mid f(a)\in S\,\}\) — the subobject S ⊆ B pulled back along f : A → B, i.e. S's classifier composed with f ( \(\chi_S\circ f\); every mono is a pullback of true, so a preimage IS such a pullback).
template<std::size_t K, typename C, C c, typename T, typename R> requires std::equality_comparable<C> && dedekind::sets::IsSetObject<R>
constexpr auto	dedekind::relational::detail_hyperdoctrine::shannon (const R &r)
	\(\exists c \in C.\ R(\ldots c \ldots)\) over a finite chain: the join of the substitutions at every value, from c upward.
template<std::size_t K, typename X, typename Y, dedekind::sets::IsSetObject S>
constexpr auto	dedekind::relational::image_along (const dedekind::category::Injection< K, X, Y > &, const S &s)
	\(\exists_\iota\) along an injection: the sum's pushforward.
template<typename X, dedekind::sets::IsSetObject S>
constexpr auto	dedekind::relational::image_along (const dedekind::category::Copy< X > &, const S &s)
	\(\exists_\Delta\) along the diagonal: the coreflexive \(\Delta_S = \{(x, x) \mid x \in S\}\), diag.
template<dedekind::category::IsPairProjection< 1 > F, dedekind::sets::IsSetObject R> requires dedekind::category::IsFiniteChain< typename dedekind::category::Dom<F>::second_type> && dedekind::category::HasNNOStep< typename dedekind::category::Dom<F>::second_type>
constexpr auto	dedekind::relational::image_along (const F &, const R &r)
	\(\exists_{\pi_1}\), the second factor a finite chain: Shannon.
template<dedekind::category::IsPairProjection< 2 > F, dedekind::sets::IsSetObject R> requires dedekind::category::IsFiniteChain< typename dedekind::category::Dom<F>::first_type> && dedekind::category::HasNNOStep< typename dedekind::category::Dom<F>::first_type>
constexpr auto	dedekind::relational::image_along (const F &, const R &r)
	\(\exists_{\pi_2}\), the first factor a finite chain: Shannon.
template<typename R, typename F, std::ranges::input_range DomRange, std::ranges::input_range CodRange> requires dedekind::category::IsArrow<F> && std::same_as<std::ranges::range_value_t<DomRange>, dedekind::category::Dom<F>> && std::same_as<std::ranges::range_value_t<CodRange>, dedekind::category::Cod<F>>
constexpr auto	dedekind::relational::is_graph_of (const R &r, F f, const DomRange &dom, const CodRange &cod)
	is_graph_of(r, f, dom) — the finite witness that a relation r is the graph of the arrow f, by pointwise agreement with graph(f) over the enumerable domain dom.

Variables
template<typename F>
constexpr bool	dedekind::category::is_left_total_v< dedekind::relational::Graph< F > > = true
template<typename F>
constexpr bool	dedekind::category::is_right_unique_v< dedekind::relational::Graph< F > > = true
constexpr auto	dedekind::relational::detail_hyperdoctrine_witness::R = graph(Code{})
constexpr auto	dedekind::relational::detail_hyperdoctrine_witness::three = 𝔸<int>{} & (π == 3)
constexpr auto	dedekind::relational::detail_hyperdoctrine_witness::t = 𝔸<bool>{} & (π == true)
constexpr auto	dedekind::relational::Γ_id = graph(dedekind::category::Identity<int>{})
constexpr auto	dedekind::relational::graph_compose_witness::dbl
constexpr auto	dedekind::relational::graph_compose_witness::inc
constexpr auto	dedekind::relational::graph_compose_witness::Γ_dbl_inc = graph(dbl) >> graph(inc)
constexpr auto	dedekind::relational::set_is_function_witness::five = dedekind::sets::𝔸<unsigned>{} & (π == 5u)
constexpr Projection< 0 >	dedekind::relational::detail_hyperdoctrine_witness::π
	The unary projection, the identity: the variable of a comprehension over one carrier.
constexpr Projection< 0 >	dedekind::relational::set_is_function_witness::π
	The unary projection, the identity: the variable of a comprehension over one carrier.

Detailed Description

The graph of a function as a relation: the analytic arrow f and its set of pairs are one object. A graph is a dyadic (binary) relation (functional \(R\subseteq A\times B\) for \(f:A\to B\); an endorelation only when \(A=B\)), so it lives with the relations (dedekind.relational), not in :sets.

@partition :graph

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

graph__The_Graph_of_a_Function

By the function-as-graph definition (Bourbaki; Lawvere and Rosebrugh, Sets for Mathematics, §2), a function \(f : A \to B\) is its graph

\[ \Gamma_f = \{\, (a,b) \in A\times B \mid b = f(a) \,\} \subseteq A\times B, \]

a functional (total, single-valued) binary relation. In a Cartesian closed category with a subobject classifier — which IsSet reifies — the analytic arrow and its graph are the same object (currying together with the classifier). graph(f) exhibits that identity at the type level: it lifts any IsArrow into the Set<std::pair> relation form of :expressions, so the arrow participates mechanically in the relational algebra of :relational.

graph__The_Graph_Is_An_Equalizer

Categorically \(\Gamma_f\) is the equalizer subobject of \(A\times B\) of the parallel pair \((f\circ\pi_A,\ \pi_B) : A\times B \to B\): exactly the members where the two coincide, \(f(a)=b\). Hence a graph is a category::IsEqualizer (an IsSubobject of pair<A,B>), not an IsIsomorphism arrow (its Set-domain is the product pair<A,B>, not A). The function it carries is the triple IsFunction<Graph<F>, A, B> = (domain A, codomain B, predicate), and the predicate slot (the equalizing \(f(a)=b\)) is the categorically-honest home of the function-ness: derived properties such as retractability and decidable image pin on that predicate, not on any pair<A,B> → Ω view of the Set. Pinned concretely for the affine translation graph by static_assert(category::IsEqualizer<...>) in algebra:halfspace_transport (#876).

graph__Single_Source_Of_Truth

The membership predicate delegates to category::arrow_as_relation<F> (the two-argument indicator \((a,b) \mapsto f(a)=b\), which already registers the left-total / right-unique traits). The Set<pair> graph and the binary-relation form therefore share one definition of \(f(a)=b\) and cannot drift: a future divergence between the two encodings is a compile error, not a silent fork. graph generalises sequences::as_relation (the graph of path.at) from a Path to an arbitrary arrow.

graph__Decidability

Membership \(\Gamma_f(a,b)\) is decidable exactly when B has decidable equality (std::equality_comparable — the std::regular codomain, the same carrier discipline IsSet roots). Enumerating the graph, or deciding that a given relation is a graph, additionally needs a finite / enumerable domain; past that boundary the honest answer is Unknown (Rice's theorem). That finite witness is is_graph_of below: a value-level pointwise check over an enumerable domain, expressed with the range-generic forall. It is not a type-level concept precisely because deciding "this relation is that function's graph" is undecidable in general (Rice); the codebase keeps single-valuedness value-level (is_single_valued_at) for the same reason.

@build_order after dedekind.sets (:expressions, :quantifier) @dependency :category, dedekind.sets

See also

dedekind.sequences:path (as_relation — the Path special case)

dedekind.category:cartesian (arrow_as_relation — the 2-arg form)

Typedef Documentation

Π

template<std::size_t K, typename P>

using dedekind::category::Π

π_k read at the product P, as a MORPHISM (Domain = P, Codomain the k-th part): the building block of IsArrowProduct. Π<0, P> is Identity

. It forwards to π_k, so it copies nothing where the component is a reference (a reducer node's operand).

Template Parameters

K	the slot.
P	the product.

Graph

template<typename F>

using dedekind::relational::Graph

export

Initial value:

 
    Comprehension<𝔸<std::pair<typename F::Domain, typename F::Codomain>,
                    dedekind::category::Boole>,
                  GraphPredicate<F>>

Graph<F> — the type of graph(f): the Set<pair> relation \(\Gamma_f=\{(a,b)\mid b=f(a)\}\subseteq A\times B\) of F : A→B.

Function Documentation

arrow_of() [1/2]

template<typename U, typename F>

F dedekind::relational::arrow_of ( const Comprehension< U, GraphPredicate< F > > & g )

constexprexport

arrow_of(graph(f)): the graph keeps its arrow, so it is f itself.

Parameters

g	the graph.

arrow_of() [2/2]

template<typename R>
requires dedekind::sets::IsGraphAtom<std::remove_cvref_t< decltype(std::declval<const R&>().predicate)>> && IsFunctional<R> && IsEntire<R>

auto dedekind::relational::arrow_of ( const R & r )

constexprexport

arrow_of(R): the arrow of a relation certified a function (a graph atom, functional and entire), the converse of graph: graph(arrow_of(R)) is R and arrow_of(graph(f)) is f.

Parameters

r	the relation over A×B.

graph()

template<typename F>
requires dedekind::category::IsArrow<F> && std::equality_comparable<typename std::remove_cvref_t<F>::Codomain>

Graph< std::remove_cvref_t< F > > dedekind::relational::graph ( F f )

constexprexport

graph(f) — the graph of a function f : A → B as the Set of pairs \(\{\,(a,b) \mid b = f(a)\,\} \subseteq A\times B\).

Template Parameters

F	An IsArrow whose Codomain has decidable equality.

Parameters

f	The analytic arrow.

Returns

A Graph<F> (a :expressions Relation) whose GraphPredicate<F> membership carries f for composition.

Note

Not part of the Trsk grammar (Listing~6), on purpose: lifting an arrow to a relation forces image / preimage to be inferred from f rather than spelled point-free, which is the source of the lambda-opacity these reifications (GraphPredicate, FibrePredicate, PreimagePredicate) exist to contain. Prefer building relations point-free (the restricted product S*T|relpred and the Tarski operators); graph stays available for the arrow-composition path but is kept out of the grammar surface. Sibling of the doc-deprecated element scout.

Related surfaces (#824). The point-free arrow lift now exists as ap(f, π_I) → ProjApplyEq (the 𝑦 == f(𝑥) relpred) in :order, and image-membership decidability is read off the arrow's certificate in :category:image (ImageChi specialised for IsRetractableArrow → Boole / decidable, else the default Ternary::Unknown). Redefining graph itself as sugar over ap (graph(f) := 𝔸<X>*𝔸 <Y> | (𝑦==ap(f,𝑥))) is parked: the lift plus the decidability seam capture the value without the DSL relocation. The group-derived mileage — IsGroup ⟹ translations retractable ⟹ free decidable image — is #875. Corrections retained from the #870 CP review: forward membership \(b=f(a)\) gates on equality_comparable (not monicity); the pre-image capability gates on IsRetractableArrow / iso (monicity gives a single-valued pre-image, the retract a computable one).

is_graph_of()

template<typename R, typename F, std::ranges::input_range DomRange, std::ranges::input_range CodRange>
requires dedekind::category::IsArrow<F> && std::same_as<std::ranges::range_value_t<DomRange>, dedekind::category::Dom<F>> && std::same_as<std::ranges::range_value_t<CodRange>, dedekind::category::Cod<F>>

auto dedekind::relational::is_graph_of ( const R & r, F f, const DomRange & dom, const CodRange & cod )

constexprexport

is_graph_of(r, f, dom) — the finite witness that a relation r is the graph of the arrow f, by pointwise agreement with graph(f) over the enumerable domain dom.

The mechanical form of "the compiler knows @c r and @c f are one and the same function": over the finite dom it compares r against the canonical graph(f) at every (a,b) in dom × dom, via the range-generic forall (the ¬∃¬ set-operation over a domain). Value-level, not a concept: deciding graph-equality of two independently given presentations is undecidable in general (Rice), so the honest witness is bounded to an enumerable domain. (When r is graph(f) by construction no check is needed — provenance is the proof; this is for an r obtained independently, e.g. an enumerated / materialised list.) The domain is a plain std::ranges::input_range of the arrow's Domain — the general concept, reached through the std iterator interface, not a container.

Template Parameters

R	A relation callable on std::pair.
F	An IsArrow.
DomRange	A std::ranges::input_range of the arrow's Domain.
CodRange	A std::ranges::input_range of the arrow's Codomain — the second factor of A × B, distinct from dom whenever Domain and Codomain differ.

operator>>()

template<typename F, typename G>
requires IsFunctional<Graph<F>> && IsFunctional<Graph<G>> && std::same_as<typename F::Codomain, typename G::Domain>

auto dedekind::relational::operator>> ( const Graph< F > & r, const Graph< G > & s )

constexprexport

Relative product of two functional relations (graphs), over any intermediate: \(\Gamma_f\,;\,\Gamma_g = \Gamma_{f;g}\).

The general relative product \((R;S)(a,c)=\exists b.\,R(a,b)\wedge S(b,c)\) needs \(\exists b\) decidable — which is why the dyadic ; (:dyadic) is Boolean-middle only. Gating on IsFunctional (this partition's own concept) is exactly the property that lifts that restriction: a single-valued relation has \(b=f(a)\) unique, so \(\exists b\) is discharged and \((\Gamma_f;\Gamma_g)(a,c)=(c=g(f(a)))\) composes decidably over \(\mathbb{Z}/\mathbb{Q}/\mathbb{R}\), letting arithmetic arrows sit between inclusion relations. This is the allegory-arrow composition on the function subcategory; it recovers the two arrows (via GraphPredicate) and re-graphs their composite under the general arrow ∘ — the general-carrier sibling of the translation graphs' >> in :halfspace (which adds shifts).

Note

No overload clash: for a non-bool intermediate the dyadic ; (requires same_as<B,bool>) is non-viable; on a bool middle this overload is strictly more specialised (GraphPredicate ⊂ any PR); the categorical arrow >> (:morphism) is non-viable on Set<pair> operands.

preimage()

template<typename F, typename S>
requires dedekind::category::IsArrow<F> && (!dedekind::category::IsLSet<std::remove_cvref_t<F>>) && requires(const S& s, const typename std::remove_cvref_t<F>::Codomain& b) { typename std::remove_cvref_t<S>::logic_species; { s(b) } -> std::same_as<typename std::remove_cvref_t<S>::logic_species::Ω>; }

auto dedekind::relational::preimage ( F f, S s )

constexprexport

preimage(f, S) = \(\{\,a \mid f(a)\in S\,\}\) — the subobject S ⊆ B pulled back along f : A → B, i.e. S's classifier composed with f ( \(\chi_S\circ f\); every mono is a pullback of true, so a preimage IS such a pullback).

The DEFAULT preimage: apply-and-test, decided by single-valuedness alone (an IsArrow is functional), so it reads the \(\pi_A\) side and never leaves the domain (§4, the relation-quantifier table). The domain type is the clip: the predicate ranges over A, so a bound outside A's range (e.g. {≤−3} pulled to unsigned) is ∅ by construction — there is no out-of-range witness to test, and no negative-pivot halfspace is ever built. No enumeration: membership is the composite \(\chi_S\circ f\), a point-free apply-and-test.

Closed-form specialisations refine this where a TYPED result adds collapse-visible structure: the bound-MOVING affine maps (:halfspace_transport translate/scale, the contravariant inverse of image) — certified to AGREE with this default pointwise. A bound-PRESERVING residue-class sibling (a Congruence rotation) is the morphologies analogue (FIXME(#797)).

S must be a SET over f's codomain: constrained to a set-shaped argument (one exposing logic_species) whose classifier accepts F::Codomain, so the documented \(S \subseteq B\) contract is checked during overload resolution — a bare callable without logic_species, or one over an unrelated ambient, is rejected here rather than hard-erroring in the body.

Variable Documentation

Γ_id

auto dedekind::relational::Γ_id = graph(dedekind::category::Identity<int>{})

inlineconstexpr

graph__Formal_Verification

dbl

auto dedekind::relational::graph_compose_witness::dbl

inlineconstexpr

Initial value:

=
    dedekind::category::arrow<int, int>([](const int& n) { return 2 * n; })

inc

auto dedekind::relational::graph_compose_witness::inc

inlineconstexpr

Initial value:

=
    dedekind::category::arrow<int, int>([](const int& n) { return n + 1; })