Céline Becouze-Lareure

Christine Bazin

Philippe Namour

Pascal Breil

Yves Perrodin

Multi-Level Approach of the Ecotoxicological Impact of a Combined Sewer Overflow on a Peri-Urban Stream

Keywords: Combined Sewer Overflow, Ecotoxicity, Pollutants, Stormwater, Stream, Urban Wet-Weather Flow

In periurban zones, urban wet weather discharges have been recognized as the most significant vector of pollution in aquatic environments. The discharge of this water without treatment into the aquatic environment could present an ecotoxicological risk for biocenosis. The aim of the INVASION project is to assess the potential ecotoxicological impact of a combined sewer overflow (CSO) on a peri-urban stream. A comparative study between upstream and downstream areas of the CSO allowed observing significant effects of this overflow on the river. We studied three layers of stream: surface water, benthic layer and hyporheic layer. To characterize the potential ecotoxicological risk of water and sediments, we used a battery of 4 bioassays: Daphnia magna, Vibrio fischeri, Brachionus calyciflorus and Heterocypris incongruens. In parallel, we measured the physico-chemical parameters: ammonium ( ), chromium (Cr), copper (Cu) and lead (Pb). An ecological risk is greatest for the hyporheic zone in downstream river, particularly for the solid phase. These results corroborated with the physico-chemical data obtained.

Introduction

The general development of urban areas is generating increasing flows of pollutants in aquatic environments from urban drainage networks and stormwater management systems [START_REF] Coustumer | Temporal Evolution and Spatial Distribution of Heavy Metals in a Stormwater Infiltration Basin-Estimation of the Mass of Trapped Pollutants[END_REF]. This water that flows into aquatic environments during wet weather conditions is defined as urban wet-weather discharges (UWWD). The release of these pollutants into the natural environment has a number of consequences such as visible pollution from floating debris, increased turbidity due to suspended solids, deoxygenation of the environment from the inflow of biodegradable organic matter and nitrates, and a potential toxic effect on aquatic environments through the widespread or localised inflow of chemical substances [START_REF] Buffleben | Evaluation of Urban Non-Point Source Runoff of Hazardous Metals Entering Santa Monica Bay, California[END_REF][START_REF] Angerville | Physicochemical and Ecotoxicological Characteristics of Urban Wet Weather Effluents (UWWE) from a French Site[END_REF].

Most investigations on UWWD evaluated the quality of discharges at catchment outlet in case of separate systems or at overflow structures in case of combined systems. Concentrations and loads of main constituents and priority substances of European Water Framework Directive [START_REF]EU Water Framework Directive: Directive 2000/60/EC of the European Parliament and of the Council Establishing a Framework for Community Action in the Field of Water Policy[END_REF] have been well documented. These last years, several research projects like ESPRIT [START_REF] Becouze-Lareure | Characterisation and Estimation of Loads of Priority Pollutants in Urban Wet Weather Discharges for Two Experimental Catchments[END_REF], ScorePP [START_REF] Holten Lutzhoft | Database Presenting Basic Information about EU WFD Priority Substances[END_REF] aimed to contribute to the identification, evaluation and characterization of priority substances transported by stormwater. These effluents therefore need to be factored into plans for the management and treatment of urban wastewater. This generally proves to be an arduous task due to their strong spatiotemporal variability in terms of quality and quantity, and the high degree of uncertainty involved in their evaluation [START_REF] Willems | Bias Correction in Hydrologic GPD Based Extreme Value Analysis by Means of a Slowly Varying Function[END_REF].

In certain circumstances, the direct discharge of urban wet-weather flow into aquatic environments can lead to ecotoxicological risks, which need to be evaluated so that the appropriate processing measures can be implemented.

However, there is a shortage of data in the literature on the ecotoxicological characterisation of urban wet-weather flow [START_REF] Marsalek | Toxicity Testing for Controlling Urban Wet-Weather Pollution: Advantages and Limitations[END_REF][START_REF] Angerville | Ecotoxicological Risk Assessment Related to the Discharge of Urban Wet Weather Effluent (UWWE) in the Streams: Case Study for a French City and an Haitian City[END_REF]. In the study by [START_REF] Marsalek | Toxicity Testing for Controlling Urban Wet-Weather Pollution: Advantages and Limitations[END_REF] [START_REF] Marsalek | Toxicity Testing for Controlling Urban Wet-Weather Pollution: Advantages and Limitations[END_REF], several variants (combined/separate sewer system, several events in time, sediments, mixed samples) were tested using a battery of eight bioassays.

This work highlighted the usefulness of characterising these effluents using a battery of bioassays for a better appreciation of their intrinsic ecotoxicity.

The main objective of our study was to presented a new approach to evaluate the ecotoxicological impact of a combined sewer overflow (CSO) on the Chaudanne, a peri-urban stream situated in a peri-urban drainage basin in the Lyon area of France.

In a first time, we had tested a bioassay battery on river samples. The ecotoxicological assays realized in order to assess the sample on "representative" organisms of the ecosystem. We had been chosen to characterize the ecotoxicological risks by mono-specific assays realized in laboratory. The aquatic organisms used come from breeding in laboratory or sporocysts bough in the shop.After validation of bioassays, we evaluate three layers of stream, surface water, benthic and hyporheic layers, through a comparative study of sampling sites both upstream and downstream of the CSO and to more accurately identify the zones (surface water, benthic zone and hyporheic zone) that pose the greatest risks to aquatic organisms. Lastly, a comparison between ecotoxicological results and physico-chemical parameters ( 4 , Cr, Cu and Pb) was carried out, in order to explain the possible toxicity of the samples. NH 

Materials and Methods

Study Site

The Chaudanne is a small, 2.5 km-long stream in the western part of Lyon (Figure 1). At the outlet of the CSO of the village of Grezieu-la-Varenne, the drainage basin covers a surface area of 2.7 km 2 . It is rural, mainly pastoral. The urban downstream portion has a smaller surface area (0.44 km 2 , or 16%). The Chaudanne stream has an average flow rate of 30 L/s. This rate exceeds several hundred litres during heavy storms and can reach a rate of around 1500 L/s when there is heavy flooding in the basin. Its flow rate is generally zero during the 4 summer months, but with a permanent underflow in the hyporheic zone. Three zones characterize the stream:  A flat zone consisting of grit and certain organic elements where the flow velocity is low;  A "riffle" segment characterised by a mixture of stone, pebbles and blocks where the flow velocity is high;  A 30-cm deep pool composed of grit and stones, where the flow velocity is very lowSampling zones. For sampling sites 2 to 4 and 6 to 8, two different zones were sampled: the benthic zone (B) and the hyporheic zone (H). Surface water (SW) samples were only collected at sites 1, 5 and 9. Samples were collected in an upstream direction at each site to avoid environmental disturbance (Figure 1).

The surface water samples were collected in a plastic 5 L container. The benthic zone corresponded to the first five superficial centimetres of the streambed and collected using a flat-bottomed hand dredge developed by the Cemagref-Lyon. It was used to carefully scrape the benthic zone to a depth of around 5 cm in order to collect the sediment, which was then transferred into a 2 L polypropylene container, and preserved on ice until it arrived at the laboratory.

The hyporheic zone samples were extracted using the Bou-Rouch pumping method [START_REF] Bou | Un Nouveau Champ de Recherches sur la Faune Aquatique souterraine[END_REF], enabling them to be collected from a depth of approximately 30 cm under the streambed. This involved creating suction in order to maintain adequate interstitial flow into the holes of a pipe and to collect the samples from the hyporheic zone. For each sample, 10 L of hyporheic water were pumped from a depth of 30 cm below the spring bed, and the two last litres were sampled.

For the benthic and hyporheic zone samples, we decided to study the "water" phase and the "particle" phase separately. Each sample was homogenised and the two phases were then separated by decantation (1 h) at room temperature. The "water" phase consisted of water and the finest suspended particles. The "particle" phase consisted of larger particles that remained at the bottom of the container.

The samples were stored in a freezer at -18˚C whilst carrying out the various measurements.

Ecotoxicity Tests

The ecotoxicological characterisation of the samples was carried out using a battery of additional bioassays (or ecotoxicity tests). These tests involved exposing a population of aquatic organisms to an effluent at increasingly high concentrations in order to determine the concentration level at which toxic effects were induced. The chosen battery adapted for the evaluation of the potential ecotoxicological impact of urban and industrial effluents on aquatic environments, and previously tested in other studies various samples: urban wet weather discharge [START_REF] Angerville | Ecotoxicological Risk Assessment Related to the Discharge of Urban Wet Weather Effluent (UWWE) in the Streams: Case Study for a French City and an Haitian City[END_REF], hospital effluents [START_REF] Boillot | Daily Physicochemical, Microbiological and Ecotoxicological Fluctuations of a Hospital Effluent According to Technical and Care Activities[END_REF], dredged materials [START_REF] Perrodin | Assessment of Ecotoxicological Risks Related to Depositing Dredged Materials from Canals in Northern France on Soil[END_REF] and marine dredged materials [START_REF] Volatier | Assessment of Marine Dredged Sediments Toxicity for Their Re-Use as Fill Materials: Step 1: Comparative Responses to a Battery of Mono-Specific Bioassay[END_REF]. The battery consists of four bioassays: Daphnia magna (Dm), Vibrio fischeria (Vf), Brachionus calyciflorus (Bc) and Heterocypris incongruens (Hi). The characteristics (organism, trophic level, etc.) of these four bioassays are listed in Table 1.

Dm is a standard assay accepted to determine the acute toxicity of aqueous matrix or substances in solution [14] [15]. Vf accepted as simple, reliable and rapid assay, moreover it is normalized. The two others assays, Bc and Hi, are normalized.

The experimental data process by using adapted tool like software to determine the CE 20 values for tested samples. It should be noted that the smaller the value, the more toxic the sample to the organism in question. The Hi test no realized on dilution range, so it is not possible to determine a CE 20 value for tested sample. The results will be expresses in percent of effect observed.

Measurement of Physico-Chemical Parameters

The physico-chemical characterisation of the samples was performed in the laboratory on the 3 sampled zones (superficial, benthic and hyporheic). Based on the preliminary results of the characterisation of chemical contaminants discharged into the stream by urban wetweather flow and on our study objective [START_REF] Namour | Métrologie des Hydrosystèmes et Méthodologies D'observations-Présentation du Site de Grézieu-la-Varenne de l'Observatoire de Terrain en Hydrologie Urbaine[END_REF], a list of evaluation parameters was drawn up: 3 metals, chromium (Cr), copper (Cu) and lead (Pb), ammonium ( 4 NH  ) and total suspended solid (TSS). The Cr and Cu in trace amounts are essential for organisms but in negligible "Water" phase and "particle" phase separately quantity. Their increase in the environment can lead to the toxicity impacts. However, others metals, like Pb, are not necessary and have toxic effects. The ammonium was chosen for its presence in urban wet weather discharge. The concentration of this ion in receiving waters is dependant of pH and can lead to the formation of NH 3 which is the form the most toxic. Laboratory testing was performed in the CARSO laboratory in Lyon. Metals analysed in particle phase according to M_ST006 and NF EN ISO11885 and ammonium analysed in water phase according to NT T90-015-2.

Results

Rainfall Campaign

Samples were collected on Monday 15 th November 2010 (Figure 2). There were 4 storm events between 15/10/ 2010 and 15/12/2010. The flow rate of the stream before the samples were collected was in the region of 20 L•s -1 . At the time of sampling, the flow rate of the Chaudanne was approximately 400 L•s -1 . This peak can be attributed to the storm event due to the quantity of stormwater (I max = 19 mm•h -1 ), the surface runoff and the inflow from the CSO. The maximal flow rate measured at the CSO outlet was 72 L•s -1 .

Before the sampling period, low flow peaks were observed in the stream. These can be explained by the discharge from the CSO.

Ecotoxicological Characterisation

"Aquatic" Sample

Dm and Vf acute toxicity tests revealed no toxicity of this type in any of the samples analysed. For the chronic toxicity test (48 h Bc), the surface water samples and the "water" samples from the benthic zone downstream of the CSO revealed no toxicity for the organisms tested. However, for the "water" samples from the hyporheic zone collected upstream of the CSO, a significant level of toxicity was found in the organisms tested (EC 20 value between 20% and 70% of sample).For the Hi chronic toxicity test, we observed for surface water samples a toxicity in this order : SW9 > SW1 ≈ SW5.

The water phase of benthic zone, based on mortality of Hi, the percentages obtained are insignificant compared to the accepted reference threshold. With regard to organism growth, the size of the organisms was similar to those obtained for the control (US3BW) for the sites above the CSO. The samples downstream of the CSO can be placed in order of toxicity as follows: DS7BW ≈ DS8BW > DS6BW.

For water phase of hyporheic zone, organism mortality was not significant compared to the reference threshold (20%) for the upstream and downstream sites. On the basis of growth inhibition, the samples collected above the CSO can be classified in the following order of toxicity: US4HW ≈ US3HW > US2HW. A higher inhibition was observed for sample DS6HW collected directly below the CSO (34%). A decrease in inhibition was noted for the other two downstream samples (21% and 17%).

"Particle" Sample

The results of the 20-min Vf test performed on the benthic (particles washed through 2-mm sieve) and hyporheic samples demonstrated that they were non-toxic to this organism for the 6 stations studied. The acute toxicity test, 48 h-Bc, realized on hyporheic particle show a significant level of toxicity in the samples collected downstream of the CSO with EC 20 values ranging between 4% and 10%. This test highlighted the much higher level of toxicity of the "particle" phase compared to the "aquatic" phase.

The Hi test showed a toxicity for particle benthic and hyporheic. For benthic zone, mortality percentages in samples US4BP and US7BP were the same or slightly lower than the threshold value of 20% (28% and 20% respectively). With regard to growth inhibition, the size of the organisms in the samples collected from above the CSO was similar to those in the control. Below the CSO, a marked increase in inhibition was observed with a percentage of 34% for site DS8BP.

According to hyporheic zone, mortality was insignificant based on the reference threshold at the upstream sites. For the downstream samples, significant mortality was recorded for sample DS8HP (65%). Based on organism growth, the inhibition percentages obtained for the downstream samples were higher than those obtained for the upstream samples. Upstream, inhibition varied between 36% and 41% whereas downstream it ranged from 50% to 69%. Sample DS7HP was the most toxic to the organisms tested.

Metal Concentrations in the Particle Fraction

Benthic Zone

Figure 3 shows the results of metal concentrations in the benthic sediments, upstream and downstream of the CSO.

For the upstream sites, mass concentrations were similar for all 3 metals (Cr, Cu and Pb). Average concentrations of Cr, Pb and Cu were 16, 8 and 4 µg/g respectively. Immediately below the CSO at sampling site DS6, concentrations increased significantly (by a factor of 3 for Cr, 14 for Pb and 12 for Cu). At the other two downstream sites (DS7 and DS8), the concentrations recorded were lower compared to those measured upstream, except for Pb at site DS7 where concentrations were even higher. This peak concentration can be attributed to the direct discharge from the CSO at the time of sampling.

Hyporheic Zone

Figure 4 shows the results of the metal concentrations measured in the hyporheic zone sediments for the 6 sampling stations.

The concentrations measured in the upstream hyporheic sediments varied according to the sampling site. Behaviour differed depending on the metal in question. Chromium concentrations were measured between 70 and 49 µg/g. Copper concentrations decreased in the downstream direction, from 106 µg/g at site US2 to 60 µg/g at site US4. A significant increase in lead content was found immediately above the CSO (site US4), from 89 to 260 µg/g -1 . The accumulation of this metal at this site may be attributable to the "pool" feature favouring this process.

As with the benthic zone, the metal content measured immediately below the CSO (site DS6) was increased (by a factor of 2 compared to site US4 immediately above the CSO). These deposits must have been the result of the direct CSO discharge. At the other two down- stream sites, concentrations were even lower than those measured upstream of the CSO.

Discussion

Bioassay Ecotoxicity Battery

The results obtained from the bioassay battery showed the sensitivity of different tests used for the different samples tested. The two acute toxicity tests (Dm and Vf) revealed no toxicity. The Bc and Hi tests were complementary. The Bc tests were sensitive for water samples whereas Hi tests allowed to evaluate the potential ecotoxicological of sediment samples. The bioassay battery used in our study was the same used in Angerville study [START_REF] Angerville | Ecotoxicological Risk Assessment Related to the Discharge of Urban Wet Weather Effluent (UWWE) in the Streams: Case Study for a French City and an Haitian City[END_REF] for urban wet weather discharge sample. The ecotoxicological impact was assessed by Bc and Hi tests and allowed to determine the toxicity acute of environmental samples.

Impact of CSO on the River

We compared ecotoxicological characteristics and physico-chemical results of samples collected at sites upstream (US2, US3 and US4) and downstream (DS6, DS7 and DS8) the CSO in order to assess the potential impact of CSO discharge on the different zones of the Chaudanne stream.

Surface Water

The pollutant concentrations found in the surface water can, to a large extent, be attributed to the storm event that took place on 15th November 2010. The suspended solid concentrations in the surface water were generally high and increased slightly from upstream (441 mg/L) to immediately downstream of the CSO (546 mg/L). These high concentrations of suspended solids resulted from increased particulate transport in both directions during the storm event (surface runoff and sediment remobilisation), and from the downstream CSO discharge. Ammonium concentrations were relatively low, but increased slightly from upstream (0.10 mg/L) to immediately downstream of the CSO (0.14 mg/L). In terms of ecotoxicology, there were no differences between up-stream and downstream surface water samples in any of the bioassays.

Benthic Zone

The increased metal concentrations in the downstream sediments found in our study are consistent with the results of a previous study carried out at the same site [START_REF] Angerville | Ecotoxicological Risk Assessment Related to the Discharge of Urban Wet Weather Effluent (UWWE) in the Streams: Case Study for a French City and an Haitian City[END_REF]. By comparing the contents obtained for the benthic sediments of the Chaudanne with those of other studies (Table 2), we observed that the contents measured upstream of CSO (US4) were of the same magnitude as those measured in the UK [START_REF] Robson | Stream Quality in a Small Urbanised Catchment[END_REF]. The sediments sampled in Brazil [START_REF] Robson | Stream Quality in a Small Urbanised Catchment[END_REF] had Cu concentrations of the same magnitude as for station US6, whereas the study carried out on the Hindon river [START_REF] Suthar | Assessment of Metals in Water and Sediments of Hindon River, India: Impact of Industrial and Urban Discharges[END_REF] revealed similar Cr and Pb contents. The differences observed between all the different sites can be explained by different land uses and by river flow rates.

A comparison of the concentrations measured in the benthic sediments with the reference values available in the literature for sediments and, more specifically, for sediments that come from granitic massifs like that of the Chaudanne, revealed increased metal concentrations in the downstream zone. The comparison, facilitated by a preliminary calculation of pollution factors (pf = sediment concentration/ reference concentration) for each of the metals studied, showed that the metal concentrations in the benthic zone were similar to the reference concentrations at the upstream sites for all three metals.

However, there was a marked increase in the concentrations at site DS6, situated immediately below the CSO (pollution factor of 3.0 for lead and 4.2 for copper), indicating the contamination of the benthic sediments at this site. These high concentrations can be attributed to the CSO discharge coupled with the geomorphology of this site, located on flat ground where the flow rate is low, which encourages metal adsorption on these particles. With regard to the ecotoxicological tests carried out on the "water" and "particle" samples from benthic sediments, differences between the upstream and downstream samples were only apparent in the 6-day Hi test. Indeed, in contrast to the upstream samples, disturbed ostracod growth was observed in those collected at site DS8. This disturbance may, however, be linked to metal concentrations, which were similar at this site to upstream sites.

Hyporheic Zone

In contrast to the benthic sediments, the pollution factors (pf) exhibited by the hyporheic sediments were frequently above 2 according to Belamie's chart (1990) [START_REF] Belamie | Methodology of a Study of Sediment Contamination by Metals: Consideration of Reference Standards and of Their Variability[END_REF]. Studies on the sediments of hyporheic zones are rare as the technique used to sample sediments by Bou Rouch pumping is mostly performed by biologists. [START_REF] Feris | Hyporheic Microbial Community Development Is a Sensitive Indicator of Metal Contamination[END_REF] [START_REF] Feris | Hyporheic Microbial Community Development Is a Sensitive Indicator of Metal Contamination[END_REF] measured Cu contamination levels of about the same magnitude as those observed for station DS6 (220 and 115 µg/g respectivement) whereas the Pb contents measured were only half those of Cu (111 and 260 µg/g respectively.

The analysis of the individual stations indicated strong variations between the hyporheic sediments. The pf values confirmed the sediment contamination at station DS6 located immediately below the CSO. The pf were even higher than 6 for lead and copper, which according to this chart, is an indicator of confirmed pollution. We also noted strong pf for site US4, situated immediately above the CSO (pf lead = 5.9; pf chromium = 4.6) and site US2, the farthest upstream (pf chromium = 3.4; pf copper = 8.2). These concentrations could indicate a bias due to the pumping method used to collect the hyporheic sediment samples. Indeed over-representation of fine fractions in relation to grit, which is naturally low in metals (quartz), would artificially increase the metal content. However, an analysis of Cr/Cu and Pb/Cu concentration ratios at site DS6 (Cr/Cu = 0.65; Pb/Cu = 0.84) showed that these ratios differed greatly from the reference concentration ratios: Cr/Cu = 1.54 and Pb/Cu = 3.38 [START_REF] Suthar | Assessment of Metals in Water and Sediments of Hindon River, India: Impact of Industrial and Urban Discharges[END_REF]. Upstream station US2 therefore presented signs of copper pollution and, to a lesser extent, chromium. The high concentrations of lead and copper measured at site US4 could be linked to local contamination (drainage ditches, etc.).

The study by [START_REF] Angerville | Ecotoxicological Risk Assessment Related to the Discharge of Urban Wet Weather Effluent (UWWE) in the Streams: Case Study for a French City and an Haitian City[END_REF] [START_REF] Angerville | Ecotoxicological Risk Assessment Related to the Discharge of Urban Wet Weather Effluent (UWWE) in the Streams: Case Study for a French City and an Haitian City[END_REF] carried out at the same experimental site also showed increased concentrations of the 3 metals downstream of the CSO. However, the concentrations in our study were much higher than those measured by Angerville. This difference could be attributable to an accumulation over a long period without losses to groundwater through diffusion, and/or by the absence of morphogenic flooding before our sampling campaign, which would have shifted the sediments and evacuated them towards the downstream portion of the basin.

In terms of ecotoxicity, two bioassays differentiated the upstream from the downstream samples: Bc and Hi. The Bc test identified the toxic effect of the particle phase, which was greater directly downstream of the CSO. This was probably linked to the high metal concentrations in the sediments, particularly lead (pf = 10.9).

The Hi test was consistent with the Bc test. A marked growth inhibition was observed for sites DS6 and DS8 compared to upstream.

Conclusions

Aquatic organisms were only at risk in the two chronic toxicity tests. The benthic and hyporheic zone samples collected immediately downstream of the CSO (DS6), particularly the "particle" phase, presented an ecotoxicological risk for the organisms.

The physico-chemical comparison of the ecotoxi-cological state of the three zones of the stream (surface water, benthic zone and hyporheic zone) both upstream and downstream of the CSO revealed the significant impact of this runoff on the stream.

In terms of chemical pollution and through a compareson with the reference concentrations, we found that the benthic sediments collected directly below the CSO contained higher mass Cr, Cu and Pb concentrations than in the upstream area, and a high level of contamination. We found increased pollution factors in the downstream hyporheic samples, indicating that all 3 metals had contaminated the sediments, especially directly below the CSO. The CSO discharge could account for the strong concentrations measured at these sites but further sampling is required to confirm this.

At the end of this study, we have achieved our objecttives concerning the feasibility and the utility of our multi-level approach. Concerning the impact assessment of the CSO on the river, it is necessary to remember that these results were obtained during a single storm, and that the ecotoxicological characteristics can vary according to the storm strength, the event duration, the season sampling, etc, Therefore, we must now repeat the studies and investigate other periods of the year in order to complete the assessment. This will enable us to study the behaviour of pollutants during different hydrologic configurations (accumulation, transfer, etc.) and to identify the periods and zones of the stream most vulnerable to ecotoxicological risk. Moreover, the coupling of "physico-chemical characterisation and ecotoxicological characterisation" carried out in parallel is a good approach to obtain relevant information even though these characterisation realised with few parameters and a battery of mono-specific bioassays reduced.



Figure 1 .

 1 Figure 1. Location of sampling sites upstream (US) (left) and downstream (DS) (right) of the Grézieu-la-Varenne CSO on the Chaudanne, a peri-urban stream. Yellow circles: sampling of surface water only; red circles: samples from the run-riffle-pool sequence in the benthic and hyporheic zones.

Figure 2 .

 2 Figure 2. Rainfall and flow rate data (Chaudanne stream and CSO) for the period from 15/10/2010 to 15/12/2010 ( sampling date: 15/11/2010) (Data obtained by the Cemagref-Lyon as part of the OTHU).

Figure 3 .Figure 4 .

 34 Figure 3. Metal concentrations in the particle fraction of the benthic zone samples.

Table 1 . List of parameters evaluated in this study. Organism Trophic level Toxicity type Standard Length of exposure Fraction of sample tested

 1

	Daphnia magna (invertebrate)	Primary consumer	Acute	NF EN ISO 6341 (T 90-301)	Mobility inhibition (24 h)	"Water" phase
	Vibrio fischeri (Microtox ® ) (bacteria)	Decomposer	Acute	NF EN ISO 11348-3 Microtox ® Basic Solid Phase Test with I 0	Luminescence inhibition (30 min) Luminescence inhibition (20 min)	"Water" phase "Particle" phase
	Brachionus calyciflorus (Rotoxkit™) (invertebrate)	Decomposer	Chronic	Standard procedure guide for chronic Rotoxkit™ or Pr NF ISO 20666	Growth of population (48 h)	"Water" phase and "particle" phase separately
	Heterocypris incongruens (OstracodToxkit™) (invertebrate)	Detritivore	Chronic	Standard procedure guide for chronic OstracodToxkit™	Mortality and growth of population (6 d)

Table 2 . Comparison of Cr, Cu and Pb contents measured in benthic sediments.

 2

	Sites	Chaudanne Upstream (US4)	Chaudanne Downstream (DS6)	Charlton Brook [17] (England)	Cambé stream [18] (Brazil)	Hindon river [19] (India)
	Cr (µg/g)	18	55	18	6	76
	Cu (µg/g)	5	54	15	48	5
	Pb (µg/g)	10	130	31	1	45

Acknowledgements

This study was funded by the Urban Hydrology Field Observatory of Lyon (Observatoire de Terrain en Hydrologie Urbaine, OTHU) and the CES 2008 "Invasion" project from ANR (French National Research Agency).


Recursive Operator Denitions

Introduction

Recursive function denitions were allowed in the rst version of TLA + [START_REF] Lamport | Specifying Systems[END_REF]. The denition

f [n ∈ Nat] ∆ = if n = 0 then 1 else n * f [n -1] (1)
is an abbreviation for:

f ∆ = choose g : g = [n ∈ Nat → if n = 0 then 1 else n * g[n -1]] (2)
However, recursive operator denitions were not allowed because it wasn't known how to assign a meaning to them.

Most of the time, recursive function denitions suceeven to dene a recursively dened operator. For example, consider the operator Cardinality recursively dened as follows so Cardinality(S ) is the number of elements in a nite set S :

Cardinality(S ) ∆ =
if S = {} then 0 else 1 + Cardinality(S \ {choose x : x ∈ S })

It can be dened as follows using a recursively dened function:

Cardinality(S ) ∆ = let f [T ∈ subset S ] ∆ = if T = {} then 0 else 1 + f [T \ {choose x : x ∈ T }] in f [S ]
While not mathematically necessary, recursive operator denitions may be necessary in practice. Dening a recursive function requires dening the function's domain, but that denition may be extremely complicated and the TLC model checker may not be able to evaluate it. This was the case with a specication of the PlusCal to TLA + translationa specication that was tested by having the actual PlusCal translator call TLC to evaluate it to perform part of the translation. As of now, the TLAPS proof system handles only recursive function denitions, not recursive operator denitions.

Recursive operator denitions were added to TLA + when, in 2005, we gured out how to give them a correct semantics. This note belatedly explains that semantics and what correct means. The discussion here is informal but, we believe, rigorous. Our results are not quite expressed in TLA + because they require declarations of higher-level operator parameters, while TLA + only allows the denition of such operators. However, the meaning of those declarations should be clear. Many of our results were independently discovered by Charguéraud [START_REF] Charguéraud | The optimal xed point combinator[END_REF]. While he was concerned with recursive denitions of functions rather than operators, some of his denitions and results closely match ours.

RT n°9341 2 The Problem

To appreciate the problem posed by recursive operator denitions, consider this example:

Op(x ) ∆ = choose y : y = Op(x ) (3)
It would appear to dene Op so that Op(42) = Op(42), which is impossible since every value equals itself.

Most logic texts that discuss denitions consider them to be axioms, so the meaning of (3) would be:

axiom ∀ x : Op(x ) = choose y : y = Op(x )
Since this axiom implies the false formula Op(42) = Op(42), (3) could not be a legal denition. To be legal, a recursive denition would have to satisfy some rule, and showing that the rule is satised would essentially require proving a theorem.

In TLA + , a denition simply asserts that one expression is a syntactic abbreviation for another expression. An ordinary, non-recursive denition Op(x ) ∆ = . . . asserts that, for any expression e, the expression Op(e) is an abbreviation for the expression obtained by syntactically substituting the expression e for x in the expression to the right of the ∆ = . There is no need to prove a theorem to dene a syntactic abbreviation.

There is nothing magic in declaring denitions to be abbreviations. To use the denition (1), we will have to prove this:

theorem ∀ n ∈ Nat : f [n] = if n = 0 then 1 else n * f [n -1]
The proof of the theorem is, of course, the same proof needed to justify a recursive denition of factorial if the meaning of that denition is taken to be an axiom.

Mathematicians write proofs, so it makes little dierence to them whether they have to write a proof to make a denition or to use it. However, most TLA + users are engineers who don't write proofs. If a proof were required to write a recursive operator denition in TLA + , the recursive denitions one could write would have to be constrained so that the proof was obvious enough to be found by the parser. Such a constraint would have been unacceptably restrictive without drastically changing TLA + . In particular, it would have required complicating the language by adding some form of typing.

We therefore had to provide a semantics for recursive denitions in which any such denition is legalincluding denition (3). A denition can then be incorrect only in the sense that it doesn't mean what its writer thought it meant. That kind of error can usually be found when the dened operator is used in a specication that is checked by a tool such as the TLC model checker.

Inria 3 Simple Recursive Denitions

We begin by considering a recursive denition of a single operator with a single argument.

Such a denition has this form:

1

F (x ) ∆ = Def (x , F ) (4)
(We consider multiple-argument operators and mutually recursive denitions below.) We

x Def by writing all subsequent denitions in this section in a module that begins with this declaration: constant Def ( , ( )) (As mentioned in the introduction, TLA + doesn't allow such a higher-order operator declaration.)

The Semantics

In 2005, the second author had the idea of letting (4) assert that F (x ) equals g[x ] for some function g containing x in its domain such that g[y] equals Def (y, g) for all y in its domain. This isn't quite right, since the second argument of Def must be an operator that takes an argument. To correct it, let's dene def (y, g) to be Def (y, G) when G is the operator obtained from g: def (y, g)

∆ = Def (y, lambda z : g[z ])
The precise statement of the idea was to let F (x ) equal: 2

let f ∆ = choose g : ∧ x ∈ domain g ∧ g = [y ∈ domain g → def (y, g)] in f [x ]
(5) It's not hard to see that this denition isn't right. For example, suppose Def were dened by: Def (x , F ( ))

∆ = if x = 0 then 1 else x * F (x -1) (6)
We would expect this to dene F (n) to equal n ! (n factorial) for every natural number n. However, let g be the function with domain {3} such that g[3] = 0. The semantics of TLA + doesn't specify what the value of g[y] is if y is not in the domain of g. So, it's possible that g [START_REF] Lamport | Specifying Systems[END_REF] = 0. In that case, g[3] = 3 * g [START_REF] Lamport | Specifying Systems[END_REF], so the body of the choose statement in (5) equals true for this function g and x = 3. Thus, it's possible that the choose chooses this function g to equal f when x equals 3, thereby dening F (3) to equal 0. This 1 In TLA + , this recursive operator denition must be preceded by a recursive F ( ) declaration. We will not bother writing those declarations. 2 A sophisticated TLA + user might think that the body of the choose should also assert that g is a function, but further thought shows that's not necessary.

RT n°9341

means it's impossible to prove that F (3) does not equal 0; and therefore it's impossible to prove that it does equal 3! as it should.

The rst author came up with a way to x this problem. For the factorial denition (6), we need to x the choice of g in (5) so that, for a natural number x , the domain of g must include 0 . . x . In general, we want to require that, if the recursion uniquely determines the value of F (x ), then the domain of g is large enough so it xes (uniquely determines) the value of g on all its elements. We rst dene fdef (S , g)

∆ = [x ∈ S → def (x , g)]
and then dene the xing condition to be fix (g), where fix (g)

∆ = ∀ h : (∀ x ∈ domain g : h[x ] = g[x ]) ⇒ (g = fdef (domain g, h))
We give a semantics to the recursive denition (4) by letting it dene F to be this operator F r:

F r(x) ∆ = ( choose g : (x ∈ domain g) ∧ fix (g) ) [x ]

Inductive Denitions

Correctness of our semantics means that

Fr (x ) = Def (x , Fr ) (7)
is true for those values of x for which we expect it to be true. For example, if Def is dened by (6), then we expect (7) to be true for all x in Nat. We expect it not to be true for any x when Def is dened by (3). (In this case, Op(x ) equals (choose f : false)[x] for all x , but who cares?)

For Def dened by (6), we expect (7) to be true when x ∈ Nat because Def is inductive on Nat. Intuitively, this means that it allows the value of F (n) for any n ∈ Nat to be computed by a nite number of applications of the denition (4). For example, we can compute F (27) by applying the denition once to see that it equals 27 * F (26), applying it a second time to see that it equals 27 * 26 * F (25), and so on until we get to F (0) = 1. In general, Def is inductive on Nat i for every n ∈ Nat, the value of Def (n, F ) depends only on the values of Def (i , F ) for i ∈ 0 . . (n -1).

We can generalize from the set Nat to any set with a well-founded order relation on the set. An (irreexive) partial order ≺ on a set S is well-founded i there does not exist any innite sequence . . . ≺ s 3 ≺ s 2 ≺ s 1 of elements of S . We x the relation ≺ by making it a parameter of our module, declaring it with: constant ≺ It's convenient to dene LT so LT (x , S ) is the set of elements of the set S that are ≺ x :

LT (x , S ) ∆ = {y ∈ S : y ≺ x }

Inria

We dene WellFounded (S ) as follows to mean that ≺ is a well-founded partial order on S :

WellFounded (S ) ∆ = ∧ ∀ x , y, z ∈ S : (x ≺ y) ∧ (y ≺ z ) ⇒ (x ≺ z ) ∧ ∀ T ∈ (subset S ) \ { } : ∃ x ∈ T : LT (x , S ) = { }
Proof by mathematical induction on the set of natural numbers is generalized to the following proof rule:

theorem GeneralInduction ∆ = assume new S , WellFounded (S ), new P ( ) ∀ x ∈ S : (∀ y ∈ LT (x , S ) : P (y)) ⇒ P (x ) prove ∀ x ∈ S : P (x )
The natural denition of what it means for Def to be inductive on a set S with wellfounded order ≺ is that, for any operator G, the value of Def (x , G) for any x ∈ S depends only on the values of G(y) for y ∈ LT (x , S ). More precisely, dene Def inductive on S to mean that the following condition holds for any operators G and H :

(∀ y ∈ LT (x , S ) : G(y) = H (y)) ⇒ (Def (x , G) = Def (x , H )) (8)
When Def is inductive on S , we expect (7) to be true for all x ∈ S . We can't write this denition of inductive in TLA + , since stating that (8) is true for all operators G and H mean quantifying over operators, which requires higher-order logic. However, we can write it as the following assume/prove, which can appear as the hypothesis of a theorem:

assume new G( ), new H ( ) prove ∀ x ∈ S : (∀ y ∈ LT (x , S ) : G(y) = H (y)) ⇒ (Def (x , G) = Def (x , H )) (9)
We will prove that this hypothesis and WellFounded (S ) imply that (7) holds for all x ∈ S . To do that, we dene Def to be contractive on S i (8) holds when G and H are obtained from functions. The precise denition is:

Contractive(S ) ∆ = ∀ g, h : ∀ x ∈ S : (∀ y ∈ LT (x , S ) : g[y] = h[y]) ⇒ (def (x , g) = def (x , h))

Correctness for Inductive Denitions

We will show that (7) holds if Def is contractivemore precisely, that Def contractive on S implies:

∀ x ∈ S : Fr (x ) = Def (x , Fr ) (10)
We begin our proof with the following lemma.

RT n°9341

Lemma 1 ∀ S , f , g, x : ∧ WellFounded (S )

∧ Contractive(S ) ∧ fix (f ) ∧ fix (g) ∧ x ∈ (domain f ) ∩ (domain g) ∩ S ⇒ (f [x ] = g[x ]) 1 define h ++ k ∆ = [y ∈ (domain h) ∪ (domain k ) → if y ∈ domain h then h[y] else k [y] ] 1 1. assume new h, new k , fix (h) prove h = fdef (domain h, h ++ k ) Proof: By the assumption fix (h), since h[z ] = (h ++ k )[z ] for all z in domain h. 1 2. suffices assume new S , new f , new g, Contractive(S ), fix (f ), fix (g) prove ∀ x ∈ (domain f ) ∩ (domain g) ∩ S : f [x ] = g[x ]
Proof: By simple logic.

1 define Sfg ∆ = (domain f ) ∩ (domain g) ∩ S 1 3. suffices assume new x ∈ Sfg, ∀ y ∈ LT (x , Sfg) : f [y] = g[y] prove f [x ] = g[x ] Proof: Sfg ⊆ S implies WellFounded (Sfg), so to prove f [x ] = g[x ]
, by GeneralInduction, it suces to prove it under the assumption that f [y] = g[y] for all y ∈ LT (x , Sfg). Proof: Since LT (x , S ) ⊆ S , if y is in (domain f ) ∩ (domain g) then it is also in Sfg,

so 1 3 implies (f ++ g)[y] = (g ++ f )[y]. If y is not in (domain f ) ∩ (domain g), then the denition of + + implies (f ++ g)[y] = (g ++ f )[y]. 1 5. def (x , f ++ g) = def (x , g ++ f )
Proof: By 1 4 and Contractive(S ) (from 1 2).

1 6. Q.E.D. Proof: f [x ] = def (x , f ++ g) [by 1 1, fix (f ) (from 1 2), and x ∈ domain f (from 1 3)] = def (x , g ++ f ) [by 1 5] = g[x ]
[by 1 1, fix (g) (from 1 2), and

x ∈ domain g (from 1 3)]

We now dene fr (S ) to be the function with domain S that agrees with Fr on that set:

fr (S ) ∆ = [x ∈ S → Fr (x )]

Inria

The next theorem shows that if Def is contractive on S , then fr (S ) equals fdef (S , fr (S )), and this equality uniquely determines the function fr (S ).

Theorem 1 ∀ S :

WellFounded (S ) ∧ Contractive(S ) ⇒ (∀ f : (f = fdef (S , f )) ≡ (f = fr (S ))) 1 1. assume new S , WellFounded (S ), Contractive(S ), new f , f = fdef (S , f ) prove fix (f ) ∧ (domain f = S ) 2 1. domain f = S
Proof: By the 1 1 assumption and the denition of fdef . 2 2. suffices assume new g, ∀ x ∈ S : g

[x ] = f [x ]
prove fdef (S , g) = f Proof: By 2 1 it suces to prove fix (f ), which by 2 1 and the denition of fix means proving that the 2 2 assume implies f = fdef (S , g).

2 3. ∀ x ∈ S : ∀ y ∈ LT (x , S ) : g[x ] = f [x ]
Proof: By the 2 2 assumption, since LT (x , S ) ⊆ S by denition of LT . Proof: 2 3 and the assumption Contractive(S ) (from 1 1) imply ∀ x ∈ S : def (x , g) = def (x , f ), which by denition of fdef implies fdef (S , g) = fdef (S , f ). By the 1 1 assumption, this is equivalent to the current goal. Proof: By 2 1, since its assume formula is equivalent to the assume/prove of 1 3, and its prove formula is the goal introduced by 1 2. Proof: 1 2 implies WellFounded (S ) and Contractive(S ). Proof:

1 define LE (x , T ) ∆ = {y ∈ T : (y ≺ x ) ∨ (y = x )}
Fr (x ) = gx [x ]
[denitions of Fr and gx ] = fx [x ]

[Lemma 1, 1 6, 1 7, and 1 3] = def (x , fr (S )) [denition of fx and 1 7] Theorem 1 has the following corollary:

Corollary 1 ∀ S : WellFounded (S ) ∧ Contractive(S ) ⇒ ∀ x ∈ S : Fr (x ) = def (x , fr (S ))
Proof: Theorem 1 implies fr (S ) = fdef (S , fr (S )), and the result then follows from the denitions of fr and fdef . The conclusion of Corollary 1 is very close to our goal, which is proving (10); but it doesn't imply that goal. In fact, the following example shows that Contractive(S ) is too weak a condition to imply (10). Dene fromFcn(G( ))

∆ = ∃ g : ∀ x : G(x ) = g[x ]
and suppose Def is dened by Def (x , G) ∆ = if fromFcn(G) then 1 else 0 For any function f and any x ∈ domain f , the denition of def implies def (x , f ) = 1 for this operator Def . This implies Def is contractive on any partially ordered set S . For any x , let f x be the function [y ∈ {x } → 1]. It's easy to see that fix (f x ) is true, and that this implies Fr (x ) = 1 for all x . However, for a function f , the semantics of TLA + says nothing about the value of f [y] for y / ∈ domain f . Therefore, there may be no function g such that ∀ x : g[x ] = 1 is true. In that case, fromFcn(Fr ) equals false, so Def (x , Fr ) equals 0 for all x , and therefore Fr (x ) = Def (x , Fr ) for all x .

The reason we can't derive (10) from the hypothesis that Def is contractive on S is that this hypothesis still allows the value of Def (x , Fr ) to depend on values of Fr (y) for y / ∈ S even though x ∈ S . This possibility is eectively ruled out by the condition that

Fr is representable on S , where representable is dened by: Representable(G( ), S )

∆ = ∀ x ∈ S : Def (x , G) = def (x , [y ∈ S → G(y)])

RT n°9341

The following theorem shows that Def contractive on S and Fr representable on S implies (10), and that any operator satisfying the recurrence condition equals Fr on S . Theorem 2 assume new S , WellFounded (S ),

Contractive(S ), new G( ), Representable(G, S ) prove (∀ x ∈ S : G(x ) = Def (x , G)) ≡ (∀ x ∈ S : G(x ) = Fr (x )) Proof: Let f ∆ = [x ∈ S → G(x )]. Then: (∀ x ∈ S : G(x ) = Def (x , G))) ≡ (f = fdef (S , f ))
[denitions of f and fdef , and the Representable(G, S ) assumption] ≡ (f = fr (S ))

[Theorem 1] ≡ (∀ x ∈ S : G(x ) = Fr (x )) [denitions of f and fr (S )]
The following corollary to Theorem 2 asserts that Def contractive and representable on S implies (10).

Corollary 2

∀ S : WellFounded (S ) ∧ Contractive(S ) ∧ Representable(Fr ) ⇒ (∀ x ∈ S : Fr (x ) = Def (x , Fr ))
Proof: By Theorem 2 applied to Fr .

Our goal is to prove that WellFounded (S ) and Def inductive on S imply (10). We have proved that WellFounded (S ) and Def implies (10). To complete the proof of our goal, we have to show that WellFounded (S ) and Def inductive on S imply Def is contractive and representable on S . Since Def inductive on S is expressed by (9), this is done by the following theorem.

Theorem 3 assume new S , WellFounded (S ), new G( ), assume new H ( ), new J ( ) prove ∀ x ∈ S : (∀ y ∈ LT (x , S ) :

H (y) = J (y)) ⇒ (Def (x , H ) = Def (x , J )) prove Contractive(S ) ∧ Representable(G, S ) 1 1. assume new g, new h, new x ∈ S , (∀ y ∈ LT (x , S ) : g[y] = h[y]) prove def (x , g) = def (x ,
⇒ (Def (x , G) = Def (x , H ))
prove ∀ x ∈ S : Fr (x ) = Def (x , Fr ) Proof: By Theorem 3, substituting Fr for G, and Corollary 2.

In practice, for any v , the value of Def (v , F ) is dened in terms of v and F (v 1 ), . . . , F (v k ) for some nite set {v 1 , . . . , v k }. There is then an obvious recursive algorithm for computing F (v ). Our results imply that if this algorithm terminates, then it computes F (v ) equal to Fr (v ). To prove this, let S equal the set of all values x for which the algorithm computes F (x ), and dene the relation ≺ on S so x ≺ y is true i the algorithm computes F (x ) when computing F (y). Termination of the algorithm implies that ≺ is an irreexive partial order on S and that S is nite, so ≺ is well-founded on S . Let G(x ) be the value computed by the algorithm for all x ∈ S . Theorem 3 implies Representable(G, S ) and Theorem 2 then implies G(v ) = Fr (v ).

Our theorems and corollaries cannot be expressed in TLA + because Def needs to be declared as constant, and TLA + does not support declarations of operators with an operator argument. To state these results in a more easy to use way, we would write them as assume /proof statements with Def declared in a new clause, which TLA + also does not permit. Our results should be provable now with TLAPS by writing an arbitrary denition of Def and proving them without using that denition.

4 Multiple Arguments TLA + permits recursive denitions of operators that take multiple arguments. We must therefore assign a meaning to this denition, for all n ∈ Nat:

F (x 1 , . . . , x n ) ∆ = Def (x 1 , . . . , x n , F ) (11)
where F is declared by constant F ( , . . . , , ( , . . . , ))

For n = 0, in which (11) is F ∆ = Def (F ), its obvious meaning is:

F ∆ = choose G : G = Def (G)

RT n°9341

We've already dened (11) for n = 1. For n > 1, we dene F (x 1 , . . . , x n ) to equal G( x 1 , . . . , x n ) for an operator G that has a single argument. To simplify things, we introduce some notation. Let x stand for x 1 , . . . , x n , so we can therefore write (11) as

F (x) ∆ = Def (x, F )
We will dene the operator G such that F (x) equals G( x ). For any expression z and any operator H of a single argument, we dene

n z ∆ = z [1], . . . z [n] n H (x) ∆ = H ( x )
We dene G by the recursive denition

G(z ) ∆ = Def G (z , G) (12)
where Def G is dened by

Def G (z , H ) ∆ = Def ( n z , n H ) (13)
Let fix G and Fr G be the operators fix and Fr dened in Section 3, when Def G is substituted for Def . In that section we dened G to be this operator:

Fr G (x ) ∆ = ( choose g : (x ∈ domain g) ∧ fix G (g) ) [x ]
Expanding denitions, we obtain:

fix G (g) ≡ ∀ h : (∀ x ∈ domain g : h[x ] = g[x ]) ⇒ (g = [x ∈ domain g → Def ( n x , n (lambda y : g[y]) ) ] )
We then dene F to equal n Fr G . Applying Corollary 3 to Def G and Fr G and expanding denitions, we get this result: assume new S , WellFounded (S ), assume new G( , . . . , ), new H ( , . . . , ) prove ∀ x ∈ S : (∀ y ∈ LT (x , S ) :

G(y) = H (y)) ⇒ (Def ( n x , G) = Def ( n x , H )) prove ∀ x ∈ S : F (x) = Def (x, F ) (14)
Like Corollary 3 of Section 3, the theorem ( 14) is the correctness condition for the meaning we assign to the denition (11).

We cannot write (11) in TLA + because we cannot express . . ., as in G( , . . . , ).

(Neither can we write the denition (14).) We can view (14) as a collection of theorems, one for each number n. A TLAPS library le could contain perhaps the rst dozen of those theorems. Alternatively, instead of dening F by (11), we can rst dene G by ( 12) and (13) and then dene F (x 1 , . . . , x n ) to equal G( x 1 , . . . , x n ). We can then deduce the desired property of F by applying Corollary 3 to G.

Inria 5 Mutual Recursion

In TLA + , an operator not declared in a recursive statement cannot be used before (or in) its denition. In dening the meaning of a module, all occurrences of such an operator can be eliminated by expanding the operator's denition. What remains is a sequence of sets of denitions of recursive operator denitions, each set having this form for some k :

(Each Def i need not actually depend on all the F i .) For k > 1, this is called a set of mutually recursive denitions. We dene the meaning of (15) in terms of a recursive denition of a single operator G taking a single argument by:

F i (x 1 , . . . , x n i ) ∆ = G( i , x 1 , . . . , x n i ) (16)
We dene G by this recursive denition of the form (4): RT n°9341

G(z ) ∆ = Def G (z , G) (17)

1 4 .

 4 ∀ y ∈ LT (x , S ) : (f ++ g)[y] = (g ++ f )[y]

2 4 .

 4 Q.E.D.

1 2 .

 2 suffices assume new S , WellFounded (S ), Contractive(S ) prove fr (S ) = fdef (S , fr (S )) 2 1. assume new S , WellFounded (S ), Contractive(S ),fr (S ) = fdef (S , fr (S )), new f , f = fdef (S , f ) prove f = fr (S )Proof: 1 1 and the assumptions imply fix (f ), fix (fr (S )), and both domain f and domain fr (S ) equal S . By Lemma 1, this implies f = fr (S ). 2 2. assume new S , WellFounded (S ), Contractive(S ), fr (S ) = fdef (S , fr (S )), new f , f = fr (S ) prove f = fdef (S , f ) Proof: The conclusion follows immediately from the hypotheses fr (S ) = fdef (S , fr (S )) and f = fr (S ).

2 3 .

 3 Q.E.D. Proof: By simple logic, 2 1 and 2 2 show that the assume/prove of 1 2 implies the theorem. RT n°9341 1 3. suffices assume new x ∈ S , ∀ y ∈ LT (x , S ) : Fr (y) = def (y, fr (S )) prove Fr (x ) = def (x , fr (S )) 2 1. assume ∀ x ∈ S : (∀ y ∈ LT (x , S ) : Fr (y) = def (y, fr (S )) ⇒ (Fr (x ) = def (x , fr (S ))) prove fr (S ) = fdef (S , fr (S )) 3 1. ∀ x ∈ S : Fr (x ) = def (x , fr (S )) Proof: By WellFounded (S ) (by 1 2), the 2 1 assumption and GeneralInduction. 3 2. Q.E.D. Proof: For all x ∈ S : fr (S ) = [x ∈ S → Fr (x )] [by denition of fr (S )] = [x ∈ S → def (x , fr (S ))] [by 3 1] = fdef (S , fr (S )) [by denition of fdef ] 2 2. Q.E.D.

fx∆= 1 .

 1 fdef (LE (x , S ), fr (S )) 1 4. fx = fdef (LE (x , S ), fx ) 2 suffices assume new y ∈ LE (x , S ) prove def (y, fr (S )) = def (y, fx ) Proof: By the denitions of fx and fdef . 2 2. suffices assume new z ∈ LT (y, S )prove fr (S )[z ] = fx [z ] Proof: Contractive(S ) (assumed in 1 2) implies that 2 2 implies the current goal (introduced by 2 1).2 3. z ∈ S ∧ z ∈ LT (x , S ) ∧ z ∈ LE (x , S )Proof: By 2 1, 2 2, the denitions of LE and LT , and the transitivity of ≺ (implied by WellFounded (S )).

2 4 .

 4 Q.E.D. Proof: fr (S )[z ] = Fr (z ) [denition of fr and 2 3] = def (z , fr (S )) [ 1 3 and 2 3] = fx [z ] [denitions of fx and fdef , and 2 3] 1 5. WellFounded (LE (x , S )) ∧ Contractive(LE (x , S ))

  h) Proof: Apply the theorem's assumption with H (y) ∆ = g[y] and J (y) ∆ = h[y].

1 2 .

 2 Representable(G, S)Proof: Dene h ∆ = [y ∈ S → G(y)] H (x ) ∆ = h[x ]. By denition of Representable, it suces to assume x ∈ S and prove Def (x , G) = def (x , h), which is done as follows:Inria Def (x , G) = Def (x , H ) [By the assume/prove assumption] = def (x , h) [By denition of def ] 1 3. Q.E.D.By 1 1, which is the denition of Contractive(S ), and 1 2.Our goal is now a simple corollary of Corollary 2 and Theorem 3. Corollary 3 assume new S , WellFounded (S ), assume new G( ), new H ( ) prove ∀ x ∈ S : (∀ y ∈ LT (x , S ) : G(y) = H (y))

F 1 (∆==

 1 x 1 , . . . , x n 1 ) Def 1 (x 1 , . . . , x n 1 , F 1 , . . . , F k ) . . . F k (x 1 , . . . , x n k ) ∆ Def k (x 1 , . . . , x n k , F 1 , . . . , F k )

  The denition of LE im-Inria plies LE (x , S ) ⊆ S . That and WellFounded (S ) imply WellFounded (LE (x , S )). From x ∈ S and the transitivity of ≺ on S (by WellFounded (S )), we have LT (y, LE (x , S )) = LT (y, S ) for all y ∈ LE (x , S ). This and Contractive(S ) imply Contractive(LE (x , S )). 1 6. fix (fx ) ∧ (x ∈ domain fx )Proof: By 1 5, 1 1 (with LE (x , S ) substituted for S ), and 1 4.1 define gx ∆ = choose g : (x ∈ domain g) ∧ fix (g) 1 7. (x ∈ domain gx ) ∧ fix (gx )Proof: By 1 6 the dening property of gx is satised by fx .

1 8. Q.E.D.

  Def G (x , J )) prove ∀ i , x 1 , . . . , x n i ∈ S : (i ∈ 1 . . k ) ⇒ F i (x 1 , . . . , x n i ) = Def i (x 1 , . . . , x n i , F 1 , . . . , F k ) Def G in terms of the F i .As with (14), formula (19) is not expressible in TLA + . It is a collection of formulas, one for each choice of the numbers k , n 1 , . . . , n k . Unlike the k = 1 case, writing these as separate theorems in a TLAPS library le does not seem feasible. We can use the alternative approach of not writing (15), but instead rst dening G by (17) and (18), and then dening the F i by (16).

	(19)
	where (18) denes

with Def G dened by

Def G (z , H ) ∆ = case z [1] = 1 → Def 1 ( z [2][1], . . . , z [2][n 1 ], H 1 , . . . , H k ) . . . 2 z [1] = k → Def k (z [2][1], . . . , z [2][n k ], H 1 , . . . , H k ) where H i (x 1 , . . . , x n i ) ∆ = H (i , x 1 , . . . , x n i ) (18)

Just as we obtained (14) for the case k = 1, we can apply Corollary 3 to G and expand denitions to get this result: assume new S , WellFounded (S ), assume new H ( ), new J ( ) prove ∀ x ∈ S : (∀ y ∈ LT (x , S ) : H (y) = J (y))

⇒ (Def G (x , H ) =

rue Honoré d'Estienne d'Orves Bâtiment Alan Turing Campus de l'École Polytechnique 91120 Palaiseau Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-0803