Theory Prod_Ultrametric_Restriction_Spaces

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Benjamin Puyobro, Université Paris-Saclay,
           IRT SystemX, CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Product›

(*<*)
theory Prod_Ultrametric_Restriction_Spaces
  imports Ultrametric_Restriction_Spaces Restriction_Spaces
begin
  (*>*)

text ‹
The product type typ‹'a × 'b› of to metric spaces is already instantiated as
a metric space by setting @{thm dist_prod_def[no_vars]}.
Unfortunately, this definition is not compatible with the distance required
by the class‹non_decseq_restriction_space›..
We first have to define a new product type with a trivial ⬚‹typedef›.
›

subsection ‹Isomorphic Product Construction›

subsubsection ‹Definition and First Properties›

typedef ('a, 'b) prodmax (‹(_ ×max/ _)› [21, 20] 20) = ‹UNIV :: ('a × 'b) set›
  morphisms from_prodmax to_prodmax by simp

―‹Simplifications because the ⬚‹typedef› is trivial.›

declare from_prodmax_inject  [simp]
  from_prodmax_inverse [simp]

lemmas to_prodmax_inject_simplified [simp] = to_prodmax_inject [simplified]
  and to_prodmax_inverse_simplified[simp] = to_prodmax_inverse[simplified]

(* useful ? *)
lemmas to_prodmax_induct_simplified = to_prodmax_induct[simplified]
  and to_prodmax_cases_simplified  = to_prodmax_cases [simplified]
  and from_prodmax_induct_simplified = from_prodmax_induct[simplified]
  and from_prodmax_cases_simplified  = from_prodmax_cases [simplified]


setup_lifting type_definition_prodmax

lift_definition Pairmax :: ‹'a ⇒ 'b ⇒ 'a ×max 'b› is Pair .


free_constructors case_prodmax for Pairmax fstmax sndmax
  by (metis Pairmax.abs_eq from_prodmax_inverse surjective_pairing)
    (metis Pairmax.rep_eq prod.inject)


lemma fstmax_def : ‹fstmax ≡ map_fun from_prodmax id fst›
  by (intro eq_reflection ext, simp add: fstmax_def,
      metis Pairmax.rep_eq from_prodmax_inverse fstmax_def prod.collapse prodmax.sel(1))
lemma fstmax_rep_eq : ‹fstmax x = fst (from_prodmax x)›
  by (metis Pairmax.rep_eq fst_conv prodmax.collapse)

lemma fstmax_abs_eq [simp] : ‹fstmax (to_prodmax y) = fst y›
  by (metis Pairmax.abs_eq prod.exhaust_sel prodmax.sel(1))

lemma fstmax_transfer [transfer_rule]: ‹rel_fun (pcr_prodmax (=) (=)) (=) fst fstmax›
  by (metis (mono_tags) Pairmax.rep_eq cr_prodmax_def fst_conv prodmax.collapse prodmax.pcr_cr_eq rel_funI)


lemma sndmax_def : ‹sndmax ≡ map_fun from_prodmax id snd›
  by (intro eq_reflection ext, simp add: sndmax_def,
      metis Pairmax.rep_eq from_prodmax_inverse prod.collapse prodmax.case)

lemma sndmax_rep_eq : ‹sndmax x = snd (from_prodmax x)›
  by (metis Pairmax.rep_eq prodmax.collapse snd_conv)

lemma sndmax_abs_eq [simp] : ‹sndmax (to_prodmax y) = snd y›
  by (metis Pairmax.abs_eq prod.exhaust_sel prodmax.sel(2))

lemma sndmax_transfer [transfer_rule] : ‹rel_fun (pcr_prodmax (=) (=)) (=) snd sndmax›
  by (metis (mono_tags, lifting) Pairmax.rep_eq cr_prodmax_def
      prodmax.collapse prodmax.pcr_cr_eq rel_funI snd_conv)


lemma case_prodmax_def : ‹case_prodmax ≡ map_fun id (map_fun from_prodmax id) case_prod›
  by (intro eq_reflection ext, simp add: prodmax.case_eq_if fstmax_rep_eq sndmax_rep_eq split_beta)

lemma case_prodmax_rep_eq : ‹case_prodmax f p = (case from_prodmax p of (x, y) ⇒ f x y)›
  by (simp add: fstmax_rep_eq prodmax.case_eq_if sndmax_rep_eq split_beta)

lemma case_prodmax_abs_eq [simp] : ‹case_prodmax f (to_prodmax q) = (case q of (x, y) ⇒ f x y)›
  by (simp add: prodmax.case_eq_if split_beta)

lemma case_prodmax_transfer [transfer_rule] : ‹rel_fun (=) (rel_fun (pcr_prodmax (=) (=)) (=)) case_prod case_prodmax›
  by (simp add: cr_prodmax_def fstmax_rep_eq prodmax.case_eq_if prodmax.pcr_cr_eq rel_fun_def sndmax_rep_eq split_beta)



subsection ‹Syntactic Sugar›

text ‹The following syntactic sugar is of course recovered from the theory theory‹HOL.Product_Type›.›

nonterminal tuple_argsmax and patternsmax
syntax
  "_tuplemax"      :: "'a ⇒ tuple_argsmax ⇒ 'a ×max 'b"        (‹(1⦉_,/ _⦊)›)
  "_tuple_argmax"  :: "'a ⇒ tuple_argsmax"                   (‹_›)
  "_tuple_argsmax" :: "'a ⇒ tuple_argsmax ⇒ tuple_argsmax"   (‹_,/ _›)
  "_patternmax"    :: "pttrn ⇒ patternsmax ⇒ pttrn"         (‹⦉_,/ _⦊›)
  ""              :: "pttrn ⇒ patternsmax"                  (‹_›)
  "_patternsmax"   :: "pttrn ⇒ patternsmax ⇒ patternsmax"    (‹_,/ _›)
translations
  "⦉x, y⦊" ⇌ "CONST Pairmax x y"
  "_patternmax x y" ⇌ "CONST Pairmax x y"
  "_patternsmax x y" ⇌ "CONST Pairmax x y"
  "_tuplemax x (_tuple_argsmax y z)" ⇌ "_tuplemax x (_tuple_argmax (_tuplemax y z))"
  "λ⦉x, y, zs⦊. b" ⇌ "CONST case_prodmax (λx ⦉y, zs⦊. b)"
  "λ⦉x, y⦊. b" ⇌ "CONST case_prodmax (λx y. b)"
  "_abs (CONST Pairmax x y) t" ⇀ "λ⦉x, y⦊. t"
  ― ‹This rule accommodates tuples in ‹case C … ⦉x, y⦊ … ⇒ …›:
     The ‹⦉x, y⦊› is parsed as ‹Pairmax x y› because it is ‹logic›,
     not ‹pttrn›.›

text ‹With this syntactic sugar, one can write
term‹case a of ⦉b, c, d, e⦊ ⇒ ⦉c, d⦊›, term‹λ⦉y, u⦊. a›,
term‹λ⦉a, b⦊. ⦉a, b, c , d ,e⦊›, term‹λ⦉a, b, c⦊. a›, ‹…›
as for the type typ‹'a × 'b›.›


― ‹Conversions between ‹_tuple› and ‹_tuplemax›.›
lemmas to_prodmax_tuple     [simp] = Pairmax.abs_eq[symmetric]
  and from_prodmax_tuplemax [simp] = Pairmax.rep_eq



subsection ‹Product›

text ‹We first redo the work of theory‹Restriction_Spaces.Restriction_Spaces_Prod›.›

instantiation prodmax :: (restriction, restriction) restriction
begin

lift_definition restriction_prodmax :: ‹'a ×max 'b ⇒ nat ⇒ 'a ×max 'b› is ‹(↓)› .

lemma restriction_prodmax_def' : ‹p ↓ n = ⦉fstmax p ↓ n, sndmax p ↓ n⦊›
  by transfer (simp add: restriction_prod_def)

instance by (intro_classes, transfer, simp)

end


instance prodmax :: (restriction_space, restriction_space) restriction_space
  by (intro_classes; transfer) (simp_all add: ex_not_restriction_related)



instantiation prodmax :: (restriction_σ, restriction_σ) restriction_σ
begin

definition restriction_σ_prodmax :: ‹('a ×max 'b) itself ⇒ nat ⇒ real›
  where ‹restriction_σ_prodmax _ n ≡
         max (restriction_σ TYPE('a) n) (restriction_σ TYPE('b) n)›

instance by intro_classes
end


instantiation prodmax :: (non_decseq_restriction_space, non_decseq_restriction_space)
  non_decseq_restriction_space
begin

definition dist_prodmax :: ‹['a ×max 'b, 'a ×max 'b] ⇒ real›
  where ‹dist_prodmax f g ≡ INF n ∈ restriction_related_set f g. restriction_σ TYPE('a ×max 'b) n›

definition uniformity_prodmax :: ‹(('a ×max 'b) × 'a ×max 'b) filter›
  where ‹uniformity_prodmax ≡ INF e∈{0 <..}. principal {(x, y). dist x y < e}›

definition open_prodmax :: ‹('a ×max 'b) set ⇒ bool›
  where ‹open_prodmax U ≡ ∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity›


instance
proof intro_classes
  show ‹restriction_σ TYPE('a ×max 'b) ⇢ 0›
    by (rule real_tendsto_sandwich
        [of ‹λn. 0› _ _ ‹λn. restriction_σ TYPE('a) n + restriction_σ TYPE('b) n›])
      (simp_all add: order_less_imp_le restriction_σ_prodmax_def max_def
        restriction_σ_tendsto_zero tendsto_add_zero)
qed (simp_all add: uniformity_prodmax_def open_prodmax_def
    restriction_σ_prodmax_def max_def dist_prodmax_def)

end

instance prodmax :: (decseq_restriction_space, decseq_restriction_space) decseq_restriction_space
proof intro_classes
  show ‹decseq (restriction_σ TYPE('a ×max 'b))›
  proof (intro decseq_SucI)
    show ‹restriction_σ TYPE('a ×max 'b) (Suc n) ≤ restriction_σ TYPE('a ×max 'b) n› for n
      using decseq_SucD[of ‹restriction_σ TYPE('a)› n]
        decseq_SucD[of ‹restriction_σ TYPE('b)› n]
      by (auto simp add: restriction_σ_prodmax_def decseq_restriction_σ)
  qed
qed

instance prodmax :: (strict_decseq_restriction_space, strict_decseq_restriction_space) strict_decseq_restriction_space
proof intro_classes
  show ‹strict_decseq (restriction_σ TYPE('a ×max 'b))›
  proof (intro strict_decseq_SucI)
    show ‹restriction_σ TYPE('a ×max 'b) (Suc n) < restriction_σ TYPE('a ×max 'b) n› for n
      using strict_decseq_SucD[of ‹restriction_σ TYPE('a)› n]
        strict_decseq_SucD[of ‹restriction_σ TYPE('b)› n]
      by (auto simp add: restriction_σ_prodmax_def strict_decseq_restriction_σ)
  qed
qed


instantiation prodmax :: (restriction_δ, restriction_δ) restriction_δ
begin

definition restriction_δ_prodmax :: ‹('a ×max 'b) itself ⇒ real›
  where ‹restriction_δ_prodmax _ ≡ max (restriction_δ TYPE('a)) (restriction_δ TYPE('b))›

instance by intro_classes (simp_all add: restriction_δ_prodmax_def max_def)

end

instance prodmax :: (at_least_geometric_restriction_space, at_least_geometric_restriction_space)
  at_least_geometric_restriction_space
proof intro_classes
  show ‹0 < restriction_σ TYPE('a ×max 'b) n› for n by simp
next
  show ‹restriction_σ TYPE('a ×max 'b) (Suc n)
        ≤ restriction_δ TYPE('a ×max 'b) * restriction_σ TYPE('a ×max 'b) n› for n
    by (auto intro: order_trans[OF restriction_σ_le]
        simp add: restriction_δ_prodmax_def mult_mono' restriction_σ_prodmax_def)
next
  show ‹dist p1 p2 = Inf (restriction_σ_related_set p1 p2)› for p1 p2 :: ‹'a ×max 'b›
    by (simp add: dist_prodmax_def)
qed


instance prodmax :: (geometric_restriction_space, geometric_restriction_space) geometric_restriction_space
proof intro_classes
  show ‹restriction_σ TYPE('a ×max 'b) n = restriction_δ TYPE('a ×max 'b) ^ n› for n
    by (simp add: restriction_σ_prodmax_def restriction_σ_is restriction_δ_prodmax_def max_def)
      (meson nle_le power_mono zero_le_restriction_δ)
next
  show ‹dist p1 p2 = Inf (restriction_σ_related_set p1 p2)› for p1 p2 :: ‹'a ×max 'b›
    by (simp add: dist_prodmax_def)
qed



lemma max_dist_projections_le_dist_prodmax :
  ‹max (dist (fstmax p1) (fstmax p2)) (dist (sndmax p1) (sndmax p2)) ≤ dist p1 p2›
proof (unfold dist_restriction_is max_def, split if_split, intro conjI impI)
  show ‹Inf (restriction_σ_related_set (sndmax p1) (sndmax p2)) ≤ Inf (restriction_σ_related_set p1 p2)›
  proof (rule cINF_superset_mono[OF nonempty_restriction_related_set])
    show ‹bdd_below (restriction_σ_related_set (sndmax p1) (sndmax p2))›
      by (meson bdd_belowI2 zero_le_restriction_σ)
  qed (simp_all add: subset_iff add: restriction_prodmax_def' restriction_σ_prodmax_def)
next
  show ‹Inf (restriction_σ_related_set (fstmax p1) (fstmax p2)) ≤ Inf (restriction_σ_related_set p1 p2)›
  proof (rule cINF_superset_mono[OF nonempty_restriction_related_set])
    show ‹bdd_below (restriction_σ_related_set (fstmax p1) (fstmax p2))›
      by (meson bdd_belowI2 zero_le_restriction_σ)
  qed (simp_all add: subset_iff add: restriction_prodmax_def' restriction_σ_prodmax_def)
qed


subsection ‹Completeness›

subsubsection ‹Preliminaries›

default_sort non_decseq_restriction_space ―‹Otherwise we should always specify.›

lemma restriction_σ_prodmax_commute :
  ‹restriction_σ TYPE('b ×max 'a) = restriction_σ TYPE('a ×max 'b)›
  unfolding restriction_σ_prodmax_def by (rule ext) simp

definition dist_left_prodmax :: ‹('a ×max 'b) itself ⇒ 'a ⇒ 'a ⇒ real›
  where ‹dist_left_prodmax _ x y ≡ INF n ∈ restriction_related_set x y. restriction_σ TYPE('a ×max 'b) n›

definition dist_right_prodmax :: ‹('a ×max 'b) itself ⇒ 'b ⇒ 'b ⇒ real›
  where ‹dist_right_prodmax _ x y ≡ INF n ∈ restriction_related_set x y. restriction_σ TYPE('a ×max 'b) n›

lemma dist_right_prodmax_is_dist_left_prodmax :
  ‹dist_right_prodmax TYPE('b ×max 'a) = dist_left_prodmax TYPE('a ×max 'b)›
  unfolding dist_left_prodmax_def dist_right_prodmax_def
  by (subst restriction_σ_prodmax_commute) simp


lemma dist_le_dist_left_prodmax : ‹dist x y ≤ dist_left_prodmax TYPE('a ×max 'b) x y›
proof (unfold dist_left_prodmax_def dist_restriction_is,
    rule cINF_mono[OF nonempty_restriction_related_set[of x y]])
  show ‹bdd_below (restriction_σ_related_set x y)›
  by (meson bdd_belowI2 zero_le_restriction_σ)
next
  show ‹m ∈ restriction_related_set x y ⟹
        ∃n∈restriction_related_set x y. σ↓ TYPE('a) n ≤ σ↓ TYPE('a ×max 'b) m› for m
    by (metis max.cobounded1 restriction_σ_prodmax_def)
qed

lemma dist_le_dist_right_prodmax : ‹dist x y ≤ dist_right_prodmax TYPE('b ×max 'a) x y›
  by (simp add: dist_le_dist_left_prodmax dist_right_prodmax_is_dist_left_prodmax)



lemma 
  fixes p1 p2 :: ‹'a :: decseq_restriction_space ×max 'b :: decseq_restriction_space›
  shows dist_prodmax_le_max_dist_left_prodmax_dist_right_prodmax : 
    ‹dist p1 p2 ≤ max (dist_left_prodmax  TYPE('a ×max 'b) (fstmax p1) (fstmax p2))
                           (dist_right_prodmax TYPE('a ×max 'b) (sndmax p1) (sndmax p2))›
proof -
  interpret left  : DecseqRestrictionSpace ‹(↓)› ‹(=)› ‹UNIV›
    ‹restriction_σ TYPE('a ×max 'b)› ‹dist_left_prodmax TYPE('a ×max 'b)›
    by unfold_locales
      (simp_all add: restriction_σ_tendsto_zero dist_left_prodmax_def decseq_restriction_σ)

  interpret right : DecseqRestrictionSpace ‹(↓)› ‹(=)› ‹UNIV :: 'b set›
    ‹restriction_σ TYPE('a ×max 'b)› ‹dist_right_prodmax TYPE('a ×max 'b)›
    by unfold_locales
      (simp_all add: restriction_σ_tendsto_zero dist_right_prodmax_def decseq_restriction_σ)

  show ‹dist p1 p2 ≤ max (dist_left_prodmax  TYPE('a ×max 'b) (fstmax p1) (fstmax p2))
                          (dist_right_prodmax TYPE('a ×max 'b) (sndmax p1) (sndmax p2))›
    by (auto simp add: dist_restriction_is_bis left.dist_restriction_is_bis
        right.dist_restriction_is_bis prodmax.expand restriction_prodmax_def')
      (smt (verit, best) Collect_cong nle_le restriction_related_le)
qed


default_sort type ―‹Back to normal.›



subsubsection ‹Complete Restriction Space›

text ‹When the instances typ‹'a› and typ‹'b› of class‹decseq_restriction_space›
      are also instances of class‹complete_space›,
      the type typ‹'a ×max 'b› is an instance of class‹complete_space›.›

lemma restriction_chain_prodmax_iff :
  ‹restriction_chain σ ⟷ restriction_chain (λn. fstmax (σ n)) ∧
                              restriction_chain (λn. sndmax (σ n))›
  by (simp add: restriction_chain_def, transfer)
    (metis fst_conv prod.collapse restriction_prod_def snd_conv)

lemma restriction_tendsto_prodmax_iff :
  ‹σ ─↓→ Σ ⟷ (λn. fstmax (σ n)) ─↓→ fstmax Σ ∧ (λn. sndmax (σ n)) ─↓→ sndmax Σ›
  by (simp add: restriction_tendsto_def, transfer, simp add: restriction_prod_def)
    (meson nle_le order.trans)

lemma restriction_convergent_prodmax_iff :
  ‹restriction_convergent σ ⟷ restriction_convergent (λn. fstmax (σ n)) ∧
                                restriction_convergent (λn. sndmax (σ n))›
  by (simp add: restriction_convergent_def restriction_tendsto_prodmax_iff)
    (metis prodmax.sel)


instance prodmax :: (complete_decseq_restriction_space, complete_decseq_restriction_space)
  complete_decseq_restriction_space
proof (intro_classes, transfer)
  fix σ :: ‹nat ⇒ 'a ×max 'b› assume ‹chain↓ σ›
  hence ‹chain↓ (λn. fstmax (σ n))› ‹chain↓ (λn. sndmax (σ n))›
    by (simp_all add: restriction_chain_prodmax_iff)
  hence ‹convergent↓ (λn. fstmax (σ n))› ‹convergent↓ (λn. sndmax (σ n))›
    by (simp_all add: restriction_chain_imp_restriction_convergent)
  thus ‹convergent↓ σ›
    by (simp add: restriction_convergent_prodmax_iff)
qed    



instance prodmax :: (complete_strict_decseq_restriction_space, complete_strict_decseq_restriction_space)
  complete_strict_decseq_restriction_space
  by intro_classes (simp add: restriction_chain_imp_restriction_convergent)

instance prodmax :: (complete_at_least_geometric_restriction_space, complete_at_least_geometric_restriction_space)
  complete_at_least_geometric_restriction_space
  by intro_classes (simp add: restriction_chain_imp_restriction_convergent)

instance prodmax :: (complete_geometric_restriction_space, complete_geometric_restriction_space)
  complete_geometric_restriction_space
  by intro_classes (simp add: restriction_chain_imp_restriction_convergent)


text ‹When the types typ‹'a› and typ‹'b› share the same restriction sequence,
      we have the following equality.›


lemma same_restriction_σ_imp_restriction_σ_prodmax_is [simp] :
  ‹restriction_σ TYPE('b :: non_decseq_restriction_space) =
   restriction_σ TYPE('a :: non_decseq_restriction_space) ⟹
   restriction_σ TYPE('a ×max 'b) = restriction_σ TYPE('a)›
  unfolding restriction_σ_prodmax_def by simp


lemma same_restriction_σ_imp_dist_prodmax_eq_max_dist_projections :
  ‹dist p1 p2 = max (dist (fstmax p1) (fstmax p2)) (dist (sndmax p1) (sndmax p2))›
  if same_restriction_σ [simp] : ‹restriction_σ TYPE('b) = restriction_σ TYPE('a)›
  for p1 p2 :: ‹'a :: decseq_restriction_space ×max 'b :: decseq_restriction_space›
proof (rule order_antisym)
  have ‹dist_left_prodmax TYPE('a ×max 'b) (fstmax p1) (fstmax p2) = dist (fstmax p1) (fstmax p2)›
    by (simp add: dist_left_prodmax_def dist_restriction_is)
  moreover have ‹dist_right_prodmax TYPE('a ×max 'b) (sndmax p1) (sndmax p2) = dist (sndmax p1) (sndmax p2)›
    by (simp add: dist_right_prodmax_def dist_restriction_is)
  ultimately show ‹dist p1 p2 ≤ max (dist (fstmax p1) (fstmax p2)) (dist (sndmax p1) (sndmax p2))›
    by (metis dist_prodmax_le_max_dist_left_prodmax_dist_right_prodmax)
next
  show ‹max (dist (fstmax p1) (fstmax p2)) (dist (sndmax p1) (sndmax p2)) ≤ dist p1 p2›
    by (fact max_dist_projections_le_dist_prodmax)
qed



text ‹Now, one can write things like term‹υ ⦉x, y⦊ . f ⦉x, y⦊›.›


text ‹We could of course imagine more support for typ‹'a ×max 'b› type,
      but as restriction spaces are intended to be used without recourse
      to metric spaces, we have not undertaken this task for the time being.›




(*<*)
end
  (*>*)