1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoids".
19 include "CoRN_notation.ma".
21 (* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *)
23 (*#* printing [=] %\ensuremath{\equiv}% #≡# *)
25 (*#* printing [~=] %\ensuremath{\mathrel{\not\equiv}}% #≠# *)
27 (*#* printing [#] %\ensuremath{\mathrel\#}% *)
29 (*#* printing ex_unq %\ensuremath{\exists^1}% #∃<sup>1</sup># *)
31 (*#* printing [o] %\ensuremath\circ% #⋅# *)
33 (*#* printing [-C-] %\ensuremath\diamond% *)
38 Definition of a constructive setoid with apartness,
39 i.e.%\% a set with an equivalence relation and an apartness relation compatible with it.
42 include "algebra/CLogic.ma".
44 include "tactics/Step.ma".
46 inline "cic:/CoRN/algebra/CSetoids/Relation.con".
51 Implicit Arguments Treflexive [A].
55 Implicit Arguments Creflexive [A].
61 Implicit Arguments Tsymmetric [A].
65 Implicit Arguments Csymmetric [A].
69 Implicit Arguments Ttransitive [A].
73 Implicit Arguments Ctransitive [A].
79 Set Implicit Arguments.
83 Unset Strict Implicit.
88 (*#* **Relations necessary for Setoids
89 %\begin{convention}% Let [A:Type].
92 Notice that their type depends on the main logical connective.
96 Section Properties_of_relations.
99 inline "cic:/CoRN/algebra/CSetoids/A.var".
101 inline "cic:/CoRN/algebra/CSetoids/irreflexive.con".
103 inline "cic:/CoRN/algebra/CSetoids/cotransitive.con".
105 inline "cic:/CoRN/algebra/CSetoids/tight_apart.con".
107 inline "cic:/CoRN/algebra/CSetoids/antisymmetric.con".
110 End Properties_of_relations.
120 Unset Implicit Arguments.
125 (*#* **Definition of Setoid
127 Apartness, being the main relation, needs to be [CProp]-valued. Equality,
128 as it is characterized by a negative statement, lives in [Prop]. *)
130 inline "cic:/CoRN/algebra/CSetoids/is_CSetoid.ind".
132 inline "cic:/CoRN/algebra/CSetoids/CSetoid.ind".
134 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/cs_crr.con" 0 (* compounds *).
137 Implicit Arguments cs_eq [c].
141 Implicit Arguments cs_ap [c].
146 inline "cic:/CoRN/algebra/CSetoids/cs_neq.con".
149 Implicit Arguments cs_neq [S].
153 %\begin{nameconvention}%
154 In the names of lemmas, we refer to [ [=] ] by [eq], [ [~=] ] by
155 [neq], and [ [#] ] by [ap].
156 %\end{nameconvention}%
159 We want concrete lemmas that state the axiomatic properties of a setoid.
165 (* Begin_SpecReals *)
168 Section CSetoid_axioms.
171 inline "cic:/CoRN/algebra/CSetoids/S.var".
173 inline "cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con".
175 inline "cic:/CoRN/algebra/CSetoids/ap_irreflexive.con".
177 inline "cic:/CoRN/algebra/CSetoids/ap_symmetric.con".
179 inline "cic:/CoRN/algebra/CSetoids/ap_cotransitive.con".
181 inline "cic:/CoRN/algebra/CSetoids/ap_tight.con".
189 (*#* **Setoid basics%\label{section:setoid-basics}%
190 %\begin{convention}% Let [S] be a setoid.
194 (* Begin_SpecReals *)
197 Section CSetoid_basics.
200 inline "cic:/CoRN/algebra/CSetoids/S.var".
205 In `there exists a unique [a:S] such that %\ldots%#...#', we now mean unique with respect to the setoid equality. We use [ex_unq] to denote unique existence.
208 inline "cic:/CoRN/algebra/CSetoids/ex_unq.con".
210 inline "cic:/CoRN/algebra/CSetoids/eq_reflexive.con".
212 inline "cic:/CoRN/algebra/CSetoids/eq_symmetric.con".
214 inline "cic:/CoRN/algebra/CSetoids/eq_transitive.con".
217 %\begin{shortcoming}%
218 The lemma [eq_reflexive] above is convertible to
219 [eq_reflexive_unfolded] below. We need the second version too,
220 because the first cannot be applied when an instance of reflexivity is needed.
221 (``I have complained bitterly about this.'' RP)
224 %\begin{nameconvention}%
225 If lemma [a] is just an unfolding of lemma [b], the name of [a] is the name
226 [b] with the suffix ``[_unfolded]''.
227 %\end{nameconvention}%
230 inline "cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con".
232 inline "cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con".
234 inline "cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con".
236 inline "cic:/CoRN/algebra/CSetoids/eq_wdl.con".
238 (* Begin_SpecReals *)
240 inline "cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con".
244 inline "cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con".
246 inline "cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con".
249 %\begin{shortcoming}%
250 We would like to write
252 Lemma eq_equiv_not_ap : forall (x y:S), x [=] y Iff ~(x [#] y).
254 In Coq, however, this lemma cannot be easily applied.
255 Therefore we have to split the lemma into the following two lemmas [eq_imp_not_ap] and [not_ap_imp_eq].
259 inline "cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con".
261 inline "cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con".
263 inline "cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con".
265 inline "cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con".
267 inline "cic:/CoRN/algebra/CSetoids/ap_imp_neq.con".
269 inline "cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con".
271 inline "cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con".
273 (* Begin_SpecReals *)
282 Section product_csetoid.
285 (*#* **The product of setoids *)
287 inline "cic:/CoRN/algebra/CSetoids/prod_ap.con".
289 inline "cic:/CoRN/algebra/CSetoids/prod_eq.con".
291 inline "cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con".
293 inline "cic:/CoRN/algebra/CSetoids/ProdCSetoid.con".
300 Implicit Arguments ex_unq [S].
304 Hint Resolve eq_reflexive_unfolded: algebra_r.
308 Hint Resolve eq_symmetric_unfolded: algebra_s.
312 Declare Left Step eq_wdl.
316 Declare Right Step eq_transitive_unfolded.
319 (* Begin_SpecReals *)
321 (*#* **Relations and predicates
322 Here we define the notions of well-definedness and strong extensionality
323 on predicates and relations.
325 %\begin{convention}% Let [S] be a setoid.
328 %\begin{nameconvention}%
329 - ``well-defined'' is abbreviated to [well_def] (or [wd]).
330 - ``strongly extensional'' is abbreviated to [strong_ext] (or [strext]).
332 %\end{nameconvention}%
336 Section CSetoid_relations_and_predicates.
339 inline "cic:/CoRN/algebra/CSetoids/S.var".
345 At this stage, we consider [CProp]- and [Prop]-valued predicates on setoids.
347 %\begin{convention}% Let [P] be a predicate on (the carrier of) [S].
352 Section CSetoidPredicates.
355 inline "cic:/CoRN/algebra/CSetoids/P.var".
357 inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext.con".
359 inline "cic:/CoRN/algebra/CSetoids/pred_wd.con".
362 End CSetoidPredicates.
365 inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind".
367 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csp_pred.con" 0 (* compounds *).
369 inline "cic:/CoRN/algebra/CSetoids/csp_wd.con".
371 (*#* Similar, with [Prop] instead of [CProp]. *)
374 Section CSetoidPPredicates.
377 inline "cic:/CoRN/algebra/CSetoids/P.var".
379 inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con".
381 inline "cic:/CoRN/algebra/CSetoids/pred_wd'.con".
384 End CSetoidPPredicates.
387 (*#* ***Definition of a setoid predicate *)
389 inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind".
391 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csp'_pred.con" 0 (* compounds *).
393 inline "cic:/CoRN/algebra/CSetoids/csp'_wd.con".
395 (* Begin_SpecReals *)
399 Let [R] be a relation on (the carrier of) [S].
400 %\end{convention}% *)
403 Section CsetoidRelations.
406 inline "cic:/CoRN/algebra/CSetoids/R.var".
408 inline "cic:/CoRN/algebra/CSetoids/rel_wdr.con".
410 inline "cic:/CoRN/algebra/CSetoids/rel_wdl.con".
412 inline "cic:/CoRN/algebra/CSetoids/rel_strext.con".
416 inline "cic:/CoRN/algebra/CSetoids/rel_strext_lft.con".
418 inline "cic:/CoRN/algebra/CSetoids/rel_strext_rht.con".
420 inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con".
422 inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con".
424 inline "cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con".
426 (* Begin_SpecReals *)
429 End CsetoidRelations.
432 (*#* ***Definition of a setoid relation
433 The type of relations over a setoid. *)
435 inline "cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind".
437 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csr_rel.con" 0 (* compounds *).
439 (*#* ***[CProp] Relations
441 Let [R] be a relation on (the carrier of) [S].
446 Section CCsetoidRelations.
449 inline "cic:/CoRN/algebra/CSetoids/R.var".
451 inline "cic:/CoRN/algebra/CSetoids/Crel_wdr.con".
453 inline "cic:/CoRN/algebra/CSetoids/Crel_wdl.con".
455 inline "cic:/CoRN/algebra/CSetoids/Crel_strext.con".
459 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con".
461 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con".
463 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con".
465 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con".
467 inline "cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con".
469 (* Begin_SpecReals *)
472 End CCsetoidRelations.
475 (*#* ***Definition of a [CProp] setoid relation
477 The type of relations over a setoid. *)
479 inline "cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind".
481 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/Ccsr_rel.con" 0 (* compounds *).
483 inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con".
485 inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con".
489 inline "cic:/CoRN/algebra/CSetoids/ap_wdr.con".
491 inline "cic:/CoRN/algebra/CSetoids/ap_wdl.con".
493 inline "cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con".
495 inline "cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con".
497 inline "cic:/CoRN/algebra/CSetoids/ap_strext.con".
499 inline "cic:/CoRN/algebra/CSetoids/predS_well_def.con".
501 (* Begin_SpecReals *)
504 End CSetoid_relations_and_predicates.
508 Declare Left Step ap_wdl_unfolded.
512 Declare Right Step ap_wdr_unfolded.
517 (*#* **Functions between setoids
518 Such functions must preserve the setoid equality
519 and be strongly extensional w.r.t.%\% the apartness, i.e.%\%
520 if [f(x,y) [#] f(x1,y1)], then [x [#] x1 + y [#] y1].
521 For every arity this has to be defined separately.
523 Let [S1], [S2] and [S3] be setoids.
526 First we consider unary functions. *)
528 (* Begin_SpecReals *)
531 Section CSetoid_functions.
534 inline "cic:/CoRN/algebra/CSetoids/S1.var".
536 inline "cic:/CoRN/algebra/CSetoids/S2.var".
538 inline "cic:/CoRN/algebra/CSetoids/S3.var".
541 Section unary_functions.
545 In the following two definitions,
546 [f] is a function from (the carrier of) [S1] to
547 (the carrier of) [S2]. *)
549 inline "cic:/CoRN/algebra/CSetoids/f.var".
551 inline "cic:/CoRN/algebra/CSetoids/fun_wd.con".
553 inline "cic:/CoRN/algebra/CSetoids/fun_strext.con".
557 inline "cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con".
559 (* Begin_SpecReals *)
565 inline "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind".
567 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csf_fun.con" 0 (* compounds *).
569 inline "cic:/CoRN/algebra/CSetoids/csf_wd.con".
573 inline "cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con".
575 (* Begin_SpecReals *)
578 Section binary_functions.
582 Now we consider binary functions.
583 In the following two definitions,
584 [f] is a function from [S1] and [S2] to [S3].
587 inline "cic:/CoRN/algebra/CSetoids/f.var".
589 inline "cic:/CoRN/algebra/CSetoids/bin_fun_wd.con".
591 inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext.con".
595 inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con".
597 (* Begin_SpecReals *)
600 End binary_functions.
603 inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind".
605 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csbf_fun.con" 0 (* compounds *).
607 inline "cic:/CoRN/algebra/CSetoids/csbf_wd.con".
609 inline "cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con".
611 inline "cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con".
613 inline "cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con".
616 End CSetoid_functions.
622 Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.
626 Implicit Arguments fun_wd [S1 S2].
630 Implicit Arguments fun_strext [S1 S2].
633 (* Begin_SpecReals *)
635 (*#* **The unary and binary (inner) operations on a csetoid
636 An operation is a function with domain(s) and co-domain equal.
638 %\begin{nameconvention}%
639 The word ``unary operation'' is abbreviated to [un_op];
640 ``binary operation'' is abbreviated to [bin_op].
641 %\end{nameconvention}%
649 Section csetoid_inner_ops.
652 inline "cic:/CoRN/algebra/CSetoids/S.var".
654 (*#* Properties of binary operations *)
656 inline "cic:/CoRN/algebra/CSetoids/commutes.con".
658 inline "cic:/CoRN/algebra/CSetoids/associative.con".
660 (*#* Well-defined unary operations on a setoid. *)
662 inline "cic:/CoRN/algebra/CSetoids/un_op_wd.con".
664 inline "cic:/CoRN/algebra/CSetoids/un_op_strext.con".
666 inline "cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con".
668 inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con".
672 inline "cic:/CoRN/algebra/CSetoids/id_strext.con".
674 inline "cic:/CoRN/algebra/CSetoids/id_pres_eq.con".
676 inline "cic:/CoRN/algebra/CSetoids/id_un_op.con".
680 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/un_op_fun.con" 0 (* compounds *).
684 (* Begin_SpecReals *)
686 inline "cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con".
690 inline "cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con".
692 inline "cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con".
694 (*#* Well-defined binary operations on a setoid. *)
696 inline "cic:/CoRN/algebra/CSetoids/bin_op_wd.con".
698 inline "cic:/CoRN/algebra/CSetoids/bin_op_strext.con".
700 (* Begin_SpecReals *)
702 inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con".
704 inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con".
708 inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con".
710 inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con".
712 (* Begin_SpecReals *)
716 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/bin_op_bin_fun.con" 0 (* compounds *).
722 inline "cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con".
724 inline "cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con".
726 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con".
728 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con".
730 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con".
732 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con".
734 inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con".
736 inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con".
738 (* Begin_SpecReals *)
741 End csetoid_inner_ops.
747 Implicit Arguments commutes [S].
750 (* Begin_SpecReals *)
753 Implicit Arguments associative [S].
759 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
762 (*#* **The binary outer operations on a csetoid
764 Let [S1] and [S2] be setoids.
769 Section csetoid_outer_ops.
772 inline "cic:/CoRN/algebra/CSetoids/S1.var".
774 inline "cic:/CoRN/algebra/CSetoids/S2.var".
777 Well-defined outer operations on a setoid.
780 inline "cic:/CoRN/algebra/CSetoids/outer_op_well_def.con".
782 inline "cic:/CoRN/algebra/CSetoids/outer_op_strext.con".
784 inline "cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con".
786 inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con".
788 inline "cic:/CoRN/algebra/CSetoids/csoo_wd.con".
790 inline "cic:/CoRN/algebra/CSetoids/csoo_strext.con".
794 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/outer_op_bin_fun.con" 0 (* compounds *).
798 inline "cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con".
801 End csetoid_outer_ops.
805 Hint Resolve csoo_wd_unfolded: algebra_c.
808 (* Begin_SpecReals *)
812 Let [S] be a setoid, and [P] a predicate on the carrier of [S].
820 inline "cic:/CoRN/algebra/CSetoids/S.var".
822 inline "cic:/CoRN/algebra/CSetoids/P.var".
824 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind".
826 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/scs_elem.con" 0 (* compounds *).
828 (*#* Though [scs_elem] is declared as a coercion, it does not satisfy the
829 uniform inheritance condition and will not be inserted. However it will
830 also not be printed, which is handy.
833 inline "cic:/CoRN/algebra/CSetoids/restrict_relation.con".
835 inline "cic:/CoRN/algebra/CSetoids/Crestrict_relation.con".
837 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con".
839 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con".
843 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con".
845 (* Begin_SpecReals *)
847 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con".
849 inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con".
853 (*#* ***Subsetoid unary operations
855 Let [f] be a unary setoid operation on [S].
860 Section SubCSetoid_unary_operations.
863 inline "cic:/CoRN/algebra/CSetoids/f.var".
865 inline "cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con".
869 Assume [pr:un_op_pres_pred].
870 %\end{convention}% *)
872 inline "cic:/CoRN/algebra/CSetoids/pr.var".
874 inline "cic:/CoRN/algebra/CSetoids/restr_un_op.con".
876 inline "cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con".
878 inline "cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con".
880 inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con".
883 End SubCSetoid_unary_operations.
886 (*#* ***Subsetoid binary operations
888 Let [f] be a binary setoid operation on [S].
893 Section SubCSetoid_binary_operations.
896 inline "cic:/CoRN/algebra/CSetoids/f.var".
898 inline "cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con".
902 Assume [bin_op_pres_pred].
906 inline "cic:/CoRN/algebra/CSetoids/pr.var".
908 inline "cic:/CoRN/algebra/CSetoids/restr_bin_op.con".
910 inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con".
912 inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con".
914 inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con".
916 inline "cic:/CoRN/algebra/CSetoids/restr_f_assoc.con".
919 End SubCSetoid_binary_operations.
922 (* Begin_SpecReals *)
933 Ltac Step_final x := apply eq_transitive_unfolded with x; Algebra.
939 Tactic Notation "Step_final" constr(c) := Step_final c.
945 inline "cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con".
948 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
951 inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con".
953 inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con".
956 Implicit Arguments nat_less_n_fun [S n].
960 Implicit Arguments nat_less_n_fun' [S n].