Wissem Dhahbi

Karim Chamari

Laurence Cheze

David G Behm

PhD, HDR Anis Chaouachi
email: anis.chaouachi@email.ati.tn

Laurence Chèze

External Responsiveness and Intra-session Reliability of the Rope-Climbing Test

Keywords: Military, Field testing, Intra-session error, Discriminant ability

HAL is

Introduction

The analysis of physical requirements of special forces soldiers (4) clearly shows that aerobic endurance, agility, muscle strength, power and endurance of the upper limbs are required [START_REF] Harman | Prediction of simulated battlefield physical performance from fieldexpedient tests[END_REF]. During the diverse operations performed by military, police and emergency (e.g. emergency medical technicians, fire fighters) personnel in their daily activities, these individuals must control their mass and their relatively heavy equipment with their upper limbs. This physical requirement is therefore of paramount importance for their overall physical performance, personal safety and safety of others. The inability to transport themselves and their equipment rapidly and reliably over or around obstacles can result in injury and possibly death. Similarly, many athletes can only perform optimally if they have sufficient relative strength and power to maneuver their body mass (e.g. gymnasts, rock climbers) as well as equipment (e.g. hockey goalies). Hence appropriate training, reliable testing and valid testing are necessary to prepare and identify those personnel that are ready to perform challenging operations and activities.

Historically, the typical methods for assessing upper limb power have been pull-ups [START_REF] Sporis | Effects of a training program for special operations battalion on soldiers' fitness characteristics[END_REF], push-ups (7), bench press power test (6) and medicine ball put tests [START_REF] Sharp | Physical fitness and body composition after a 9-month deployment to Afghanistan[END_REF]. To assess the power of the upper limbs, Execution Time (ET) and Relative Power Output (RPO) indices are widely used in specific tests in different sports [START_REF] Laffaye | Upper-limb power test in rockclimbing[END_REF], standard field tests (6) and standard laboratory tests (28). In the context of military, police, emergency medical personnel and athletes, a strong individual with lower body mass has the advantage in weight bearing tests

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

and activities (e.g. pull-up or rope climb tests) [START_REF] Bishop | Impact of body weight on performance of a weight-supported motor fitness test in men[END_REF]. Compared to individuals with greater muscle mass, the lighter individual is disadvantaged when required to pull, push, lift or carry an object with greater absolute mass (e.g. a victim, goalie equipment). Dhahbi et al. [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF] reported that RPO was a more convenient parameter than ET in the specific Rope Climbing Test (RCT). The latter test has been recently validated for assessment of power of the upper limbs of Commando soldiers [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF].

The concurrent validity, reliability and responsiveness are basic attributes used for evaluating the validity of any test in sport physiology [START_REF] Aaronson | Assessing health status and quality-of-life instruments: attributes and review criteria. Quality of life research : an international journal of quality of life aspects of treatment[END_REF][START_REF] Impellizzeri | Test validation in sport physiology: lessons learned from clinimetrics[END_REF]. The external responsiveness and intra-session reliability of RCT have not been reported. Dhahbi et al. [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF] only considered the inter-session reliability and the criterion-related validity of RCT. External responsiveness determines the discriminative ability of a test and usually is assessed by testing differences between two groups of individuals with different performance profiles [START_REF] Impellizzeri | Test validation in sport physiology: lessons learned from clinimetrics[END_REF]. One of the most important aims of the RCT test is to select soldiers. Thus, the external responsiveness of the RCT should discriminate between soldiers of different specialty operations levels (e.g. Commandos vs. Intervention-Brigade). The intra-session error is free of methodological errors, cannot be reduced, and thereby serves as an appropriate baseline for comparisons, remaining independent of other error sources [START_REF] Mcginley | The reliability of three-dimensional kinematic gait measurements: a systematic review[END_REF]. An unreliable or invalid test could allow for the placement of incapable professionals (or athletes), which could impact the safety of the individual and the dependent individuals (e.g. victims in a fire, injured victim in a car accident). This theoretical background reveals the lack of knowledge on the assessment of the RCT to distinguish performance profiles and its intra-session reliability. Therefore, the aims of this study were to (1) investigate the discriminant ability of RCT (Commandos vs. Intervention-Brigade) and (2) to examine the absolute and relative intra-session reliabilities of RCT.

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

Methods

Experimental Approach to the Problem

The external responsiveness of the RCT was determined by comparing ET, Absolute Power Output (APO) and RPO between two groups of soldiers of different specialty operations levels (Commandos vs. Intervention-Brigade). During the second study phase, which aimed to establish the relative and absolute intra-session reliabilities of RCT, the experimental protocol consisted of performing 3 trials of RCT in a single session.

Subjects

Forty male soldiers belonging to the special units of the National Guard voluntarily participated (Table 1). Twenty-one Commandos soldiers were employed to investigate the All participants were free from any injury or pain that would prevent maximal effort during performance testing. All the participants gave their written informed consent to the study after receiving a thorough explanation about the protocol. This protocol conformed to

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

internationally accepted policy statements regarding the use of human subjects and was approved by the University Ethics Committee in accordance with the Helsinki declaration.

Procedures

Participants were requested to follow their normal diet, eat a light meal at least 3 hours before each session, keep their usual sleep schedule, and stop any strenuous activity during the last 24 hours before the test. Seven days before baseline testing, one session was carried out to familiarize the participants with the measurement protocol. Before starting the tests, the participants achieved 15 min of standardized specific warm-up with 5 min of rest. Data were collected from participants at approximately the same time of day (between: 9:00 and 11:00 a.m.) in order to eliminate any influence of circadian variations on performance [START_REF] Drust | Circadian rhythms in sports performance--an update[END_REF].

The session was performed outdoors in the following conditions (measurements monitored by a digital environmental station: VaisalaOyj, Helsinki, Finland; every 30 min during the experiment): temperature ranged from 15°C-17°C, humidity ranged from 55%-56% and the wind velocity was light (under 10 km/h). Participants performed the tests wearing the army combat uniform without a bulletproof vest and tactical foot wear (the mass of the equipment was ~5 kg). The protocol consisted of performing 3 trials of RCT, with 5 min rest between trials. The experimenter provided strong verbal encouragement during the tests so as to obtain maximum efforts. The Rate of Perceived Exertion (RPE) was recorded immediately after the RCT using the Borg scale (RPE, 1-10) [START_REF] Haddad | Validity and psychometric evaluation of the French version of RPE scale in young fit males when monitoring training loads[END_REF].

m Rope Climbing Test (RCT)

The RCT test was performed using the criteria outlined in the investigation of Dhahbi et al. [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF]. The participant was instructed to climb the rope as fast as possible and hit the finish mark (see description below). The manual timer was triggered at the signal of the assessor and stopped when the participant touched the mark that was situated at a height of 5

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

m above the starting mark. Dhahbi et al. [START_REF] Deyo | Assessing the responsiveness of functional scales to clinical change: an analogy to diagnostic test performance[END_REF] showed excellent concurrent validity of hand timing with no significant difference between the stopwatch and video timer with a low systematic bias (0.18 sec) and very little difference in Standard Errors of Measurement (SEM) value (<5%). Moreover, Dhahbi et al. [START_REF] Deyo | Assessing the responsiveness of functional scales to clinical change: an analogy to diagnostic test performance[END_REF] found high agreement both within and between the two timing methods with the coefficient of correlation at r=0.99 (p<0.001) and the Intraclass Correlation Coefficient (ICC) at 0.98. The Rope Climbing Test began with the participant sitting on his buttocks with the rope between his legs, both hands placed on the rope without exceeding the starting mark situated at 1 m above the ground. The climbing was performed without skipping (without momentum), without the use of any gloves and without using lower limbs (i.e. the legs and feet were not allowed to touch the rope to help climbing) (see Figure 1).

The Execution Time (ET) was defined as the time between the starting signal and the noise of the slap of the hand hitting the finish mark. Both visual and auditory cues were used by the assessor to ensure that substantial and solid contact was made with the finish mark. The two best attempts out of the 3 trials were kept for analysis. The removal of the worst trial was an attempt to ensure that a single poor performance did not substantially affect the analysis.

To provide greater reproducibility of measurement, only one assessor measured the ET (no inter-assessor differences in reaction and movement time). The measurement of ET allowed for the estimation of the Absolute (APO) and Relative Power Output (RPO), which were calculated using the following equations:

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

Statistical Analyses

Data analyses were performed using SPSS version 18.0 for Windows. Means and standard deviations (SD) were calculated after verifying the normality of distributions using Kolmogorov-Smirnov statistics. Estimates of effect size, mean differences, and 95% confidence intervals (CIs) protected against type 2 errors. Independent t-tests were used to evaluate the equality of means for Commandos and Intervention-Brigade soldiers' RCT ET, APO, RPO and RPE. The external responsiveness of the RCT was analyzed using the receiver operator characteristics (ROC) curve [START_REF] Impellizzeri | Test validation in sport physiology: lessons learned from clinimetrics[END_REF]. The latter analysis determines the sensitivity and specificity of a tool to classify individuals according to a fixed criterion (9). The relative intrasession reliability (i.e. the degree to which individuals maintain their position in a sample over repeated measurements (2)) of the ET, APO and RPO were determined by calculating the ICC (ICC [START_REF] Bishop | Impact of body weight on performance of a weight-supported motor fitness test in men[END_REF][START_REF] Aaronson | Assessing health status and quality-of-life instruments: attributes and review criteria. Quality of life research : an international journal of quality of life aspects of treatment[END_REF]), and the absolute intra-session reliability (i.e. the degree to which repeated measurements vary for individuals (2)) was expressed in terms of SEM and Coefficients of Variation (CV). Heteroscedasticity was examined. Significance for all the statistical tests was accepted at p≤0.05 a priori.

Results

Discriminant ability of RCT

Separate group (Commandos and Intervention-Brigade) anthropometric characteristics and RCT indices (ET, APO, RPO and RPE) are displayed in Tables 1 and2

Absolute and relative intra-session reliability of RCT

Absolute and relative intra-session reliability indices are expressed in Table 3.

Dependent t-tests evaluating the equality of means showed no significant test-retest bias for ET (sec) (t=-0.62, p=0.55, dz=0.13 [trivial]); APO (W) (t=0.78, p=0.44, dz=0.17

Discussion

The inability to provide reliable and valid strength and power testing to identify and progressively train athletes, military, police and emergency medical personnel could result in serious personal injury or injuries to individuals who are dependent upon them. Hence, this study assessed the discriminant ability of RCT to distinguish soldiers' specialty level as well as to establish the absolute and relative intra-session reliability. The main findings of this

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

study showed that RCT is a highly reliable intra-session and sensitive tool to differentiate upper limb power between two groups of soldiers of different operational capacity levels.

One of the main characteristics of the RCT is its discriminant ability. A significant difference was found between ET, APO and RPO performance of Commandos and Intervention-Brigade groups. Impellizzeri and Marcora [START_REF] Impellizzeri | Test validation in sport physiology: lessons learned from clinimetrics[END_REF] suggested that the ROC curve is an appropriate tool to validate the discriminant ability (and responsiveness) of physiological and performance tests and can determine test sensitivity and specificity to classify individuals according to a fixed criterion (5). The area under the ROC curve (AUC) was interpreted as the probability to correctly discriminate Commandos from Intervention-Brigade soldiers using the RCT protocol. An AUC value of 0.5 is interpreted as no discriminatory ability and 1.0 as complete discriminatory ability (9) with an AUC>0.70 considered to indicate good discriminative ability [START_REF] Deyo | Assessing the responsiveness of functional scales to clinical change: an analogy to diagnostic test performance[END_REF][START_REF] Mannion | Outcome assessment in low back pain: how low can you go? European spine journal : official publication of the European Spine Society, the European Spinal Deformity[END_REF]. In the present study, the AUC values were: 0.91, 0.85 and 0.90 for ET, APO and RPO, respectively [START_REF] Deyo | Assessing the responsiveness of functional scales to clinical change: an analogy to diagnostic test performance[END_REF]. The test scores (ET, APO and RPO) able to differentiate between groups of soldiers of different operational capacity levels were ≥20.14 sec, ≥185.64 W and ≥2.43 W•kg -1 , respectively. ROC consists of a plot of "true positive rate" (sensitivity) vs. "false positive rate" (1-specificity) for each of several possible cut-off points in changing the score [START_REF] Deyo | Assessing the responsiveness of functional scales to clinical change: an analogy to diagnostic test performance[END_REF]. These cut-off values give a true positive rate of 73.7%, for ET, APO and RPO; and a false positive rate of 95.2%, 85.7% and 95.2% for ET, APO and RPO, respectively (figure2). Therefore, RCT has excellent discriminant ability if its purpose is to differentiate between Commandos and other specialty soldiers. These results are complementary with those of Dhahbi et al. [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF] who included the same group of Commandos that participated in this study. They assessed the internal responsiveness (i.e. the ability to detect longitudinal changes) of the RCT by calculating the likelihood that differences in RCT outcomes were substantial (i.e., the Smallest Worthwhile Change larger than the SEM) [START_REF] Liow | Velocity specificity of weight training for kayak sprint performance[END_REF]. This was the case for all ET, APO and RPO [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF], indicating that such data have a good Although the typical methods for assessing upper limb power have been pull-ups [START_REF] Sporis | Effects of a training program for special operations battalion on soldiers' fitness characteristics[END_REF], push-ups (7), bench press power test (6) and medicine ball put tests [START_REF] Sharp | Physical fitness and body composition after a 9-month deployment to Afghanistan[END_REF], few studies provide data on their discriminant ability. For example, there was no data reported for the discriminant ability of 15 sec pull-ups ( 23), 15 sec push-ups [START_REF] Negrete | Reliability, minimal detectable change, and normative values for tests of upper extremity function and power[END_REF], bench press (6, 26), medicine ball puts or throws (6, 27) or single arm seated shop puts [START_REF] Negrete | Reliability, minimal detectable change, and normative values for tests of upper extremity function and power[END_REF]. Using a laboratory Wingate test rather than a field test, Koutedakis et al. [START_REF] Koutedakis | A modified Wingate test for measuring anaerobic work of the upper body in junior rowers[END_REF] had excellent discrimination as they could classify 91.8% of their subjects. A good level of discrimination was reported for bench press repeated power test ( 13) and a medicine ball throw test (8) with youth basketball players and children of 5-7 years respectively. A rock climbing specific test (arm jump board test) could discriminate between novice and experienced climbers [START_REF] Laffaye | Upper-limb power test in rockclimbing[END_REF]. Hence, the excellent discriminant ability scores, that substantiated by a powerful statistical tool as the ROC curve, for a simple field test such as the RCT should be considered an important tool for professionals and practitioners in the field. Moreover, no significant difference was found between groups in RPE responses. This strongly suggests that both groups of participants did comparable efforts, most probably maximal efforts. The absence of a significant anthropometric and age differences between groups ensures these variables did affect performance.

The variability between trials may be considered as "intrinsic variation", as it provides a basic indication of the variation independent from other sources of error. Intra-session reliability of RCT performance is critically important to ensure that observed differences between testing trials are not due to systematic bias, such as a learning effect, fatigue, or

Copyright ª 2016 National Strength and Conditioning Association

A C C E P T E D

random error due to possible biological or mechanical variations. This variability is usually caused by the emotional state of the subject between the trials and his level of adaptation with the measuring system [START_REF] Mcginley | The reliability of three-dimensional kinematic gait measurements: a systematic review[END_REF]. The results demonstrated a very high level of relative reliability of RCT. Other upper limb field tests such as 15 sec pull-ups (0.99) [START_REF] Negrete | Reliability, minimal detectable change, and normative values for tests of upper extremity function and power[END_REF], 15 sec push-ups (0.96) [START_REF] Negrete | Reliability, minimal detectable change, and normative values for tests of upper extremity function and power[END_REF], bench press (0.92-0.98) (6, 13), medicine ball throws (0.92-0.97) (6, 8) and rock climbing specific test (0.98) [START_REF] Laffaye | Upper-limb power test in rockclimbing[END_REF] have also reported excellent ICC reliability scores. However, one of the weaknesses of ICC as a measure of relative repeatability is that it is affected by sample heterogeneity (29). Therefore an examination of the SEM, which provides an absolute index of reliability in conjunction with the ICC is needed to confirm the ICC's results [START_REF] Looney | When is the intraclass correlation coefficient misleading?[END_REF].

The SEM is not affected by inter-subject variability (29) and provides an estimate of measurement error. In addition, if data are homoscedastic, which is the case in the current study (r=0.01, r=0.40 and r=0.43; p>0.05 for ET, APO and RPO, respectively), SEM index is more appropriate than CV to establish the absolute reliability [START_REF] Atkinson | Statistical methods for assessing measurement error (reliability) in variables relevant to sports medicine[END_REF]29). In this study, SEMs were low for all parameters, under 5%, thereby confirming the excellent absolute intra-session reliability of RCT. Similarly, Dhahbi et al. [START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF] found an excellent inter-session reliability of RCT: for ET, APO and RPO; ICC [START_REF] Bishop | Impact of body weight on performance of a weight-supported motor fitness test in men[END_REF][START_REF] Aaronson | Assessing health status and quality-of-life instruments: attributes and review criteria. Quality of life research : an international journal of quality of life aspects of treatment[END_REF] values were all higher than 0.90, SEM% all under 5% and CV% all under 10%. Thus, it can be concluded that the RCT has excellent intra-and inter-session reliability.

In conclusion, the RCT has excellent relative and absolute intra-session reliability and a good discriminant ability to detect difference in power performance of upper limbs between two groups of soldiers of different operational capacity levels. A score of 20.14 sec, ≥185.64 W and ≥2.43 W⋅kg -1 for ET, APO and RPO respectively were the cut-off points discriminating elite Commandos from less trained Intervention-Brigade soldiers. While these scores were reliable and discriminant in the current study population, these cut-off points may not be the same in other populations and that this should be examined in future studies.

  discriminant ability of RCT. The inclusion criteria of Commandos soldiers was having regularly trained for at least 4 months in the National Guard School of Commandos, for ~32 h/week. Training was divided into ~14 h/week for fitness training and ~18 h/week dedicated to technical and tactical training. Another group of 19 soldiers participated from an Intervention-Brigade. The inclusion criteria of Intervention-Brigade was having trained for at least 8 weeks in the National Guard School of Intervention-Brigade/Commandos, for 4 sessions per week (1 session for strength and conditioning and 3 sessions per week for technical and tactical training), for approximately 2 hours in duration each. Both groups were used to establish external responsiveness, whereas only the anti-terrorism Commandos participated in the intra-session reliability study.

  , respectively. Residual data for anthropometric characteristics and RCT indices were normally distributed (p = 0.052-0.200). Independent sample t-test revealed no difference between groups for age (years) (t=-0.188, p=0.852, dz=0.06[trivial]); body mass (kg) (t=-1.018, p=0.315, dz=0.32[moderate]); height (cm) (t=-0.043, p=0.966, dz=0.01[trivial]); body mass index (BMI: kg . m -2 ) (t=-0.921, p=0.363, dz=0.29 [moderate]); or RPE (t=-0.269, p=0.789, dz=0.09 [trivial]). However, ET (t=-5.918, dz=1.87[large]), APO (t=4.255, dz=1.33[large]) and RPOCopyright ª 2016 National Strength and Conditioning Association 122, dz=1.52[large]) were significantly higher for Commandos compared to Intervention-Brigade group (p<0.001). A ROC analysis was performed between Commandos and Intervention-Brigade soldiers: very good discriminant ability was found for RCT. The areas under the ROC curves of ET, APO and RPO were of 0.91, 0.85 and 0.90, respectively (95% confidence intervals [CI]: 0.77 to 0.98, 0.70 to 0.94 and 0.77 to 0.98, respectively; p<0.001) (Figure2).

  [trivial]); RPO (W•kg -1 ) (t=0.85, p=0.41, dz=0.21 [moderate]) and RPE (t=0.17, p=0.87, dz=0.05[trivial]). The ET, APO and RPO showed a high degree of relative reliability between the testretest trials (ICC[START_REF] Bishop | Impact of body weight on performance of a weight-supported motor fitness test in men[END_REF][START_REF] Aaronson | Assessing health status and quality-of-life instruments: attributes and review criteria. Quality of life research : an international journal of quality of life aspects of treatment[END_REF] ranging from 0.96 to 0.97). The SEM of ET, APO and RPO were 0.23 sec, 3.25 W and 0.05 W•kg -1 , respectively. The CVs of ET, APO and RPO were all under 10%. Heteroscedasticity coefficients for ET, APO, RPO and RPE were all small and statistically non-significant (r=0.01 [p=0.96], r=0.40 [p=0.08], r=0.43 [p=0.06] and r=-0.31 [p=0.16], respectively).

  potential to detect real changes in the power output of upper limbs. As well as, in the Dhabbi et al.[START_REF] Dhahbi | Five Meters Ropeclimbing Test: Commando-specific Power Test of the Upper-Limbs[END_REF] study, the Minimal Detectable Change (2) was used to find the score threshold corresponding to a true change in the performance. They showed that 1.62 sec, 31.45 W and 0.41 W•kg -1 or more of ET, APO and RPO, respectively were necessary to be 95% confident that a true change has occurred in Commandos soldiers.

RCT = 5 mFigure 1 :Figure 2 :

 512 Figure 1: The 5 m Rope Climbing Test from the starting to the finishing position. A = starting position, B = execution and C = finishing position.

Table 1 :

 1 Descriptive data and comparison of the characteristics of Commandos and Intervention Brigade groups

	E P T E D
	A C C
	Copyright ª 2016 National Strength and Conditioning Association

Copyright ª 2016 National Strength and Conditioning Association Copyright ª 2016 National Strength and Conditioning Association Copyright ª 2016 National Strength and Conditioning Association

Table 2 :

 2 Descriptive data and comparison of the RCT indices of Commandos and Intervention Brigade groups Rope Climbing Test; ET = Execution Time; APO = Absolute Power Output; RPO = Relative Power Output; RPE= Rating of Perceived Exertion; *Significant difference between groups (p < 0.001); Values are given as mean ± SD.

	Variables	Commandos (n=21) Intervention Brigade (n=19)	p-values	Effect size
	ET	(sec)	15.55±3.48	22.11±3.53*	<0.001	1.87
	APO	(W)	251.13±73.55	174.59±35.41*	<0.001	1.33
	RPO	(W•kg -1 )	3.33±0.85	2.28±0.39*	<0.001	1.52
	RPE		8.07±1.04	8.16±0.99	0. 789	0.09
	RCT = 5 m

Table 3 :

 3 Relative and Absolute intra-session reliability indices of the RCT (n=21)

			Mean±SD
		Variables			p-values	ICC 3,1 (95%) ¶	SEM (%) †	CV †
			Trial 1	Trial 2
	ET	(sec)	15.55±3.48	15.41±3.65	0. 545	0.96 (0.89-0.98)	0.23 (1.47%)	6.92
	APO	(W)	251.13±73.55	254.28±74.40	0.443	0.97 (0.93-0.99)	3.25 (1.29%)	7.30
	RPO	(W•kg -1 )	3.33±0.85	3.38±0.88	0.407	0.96 (0.91-0.98)	0.05 (1.46%)	7.30
	RPE		8.07±1.04	8.10±0.94	0.871	0.78 (0.53-0.90)	0.31 (3.84%)	8.18

Acknowledgments

The authors are grateful to all the participants for their enthusiasm and commitment to the completion of this study. They also wish to express their sincere gratitude to Colonel Imed Mekki, director of the Tunisian Commandos' School, for advice and cooperation in this study.

Practical Applications:

The RCT is a fitness-specific field test designed to evaluate the power of the upper limbs performance of Commando soldiers. The results showed that this test has a good absolute and relative reliability and successfully discriminates soldiers by operational level.

Considering that (i) reliability and (ii) discriminant ability of a test are two important aspects, RCT can therefore be recommended for similar professionals such as the military, police, fire fighters and emergency medical personnel.

Copyright ª 2016 National Strength and Conditioning Association


Thi-Bich-Hanh Dao

Khalil Djelloul

Solving First-Order Constraints in the Theory of the Evaluated Trees

We describe in this paper a general algorithm for solving first-order constraints in the theory T of the evaluated trees which is a combination of the theory of finite or infinite trees and the theory of the rational numbers with addition, subtraction and a linear dense order relation. It transforms a first-order formula ϕ, which can possibly contain free variables, into a disjunction φ of solved formulas which is equivalent in T , without new free variables and such that φ is either true or false or a formula having at least one free variable and being equivalent neither to true nor to false in T .

Introduction

The theory of finite or infinite trees plays a fundamental role in computer science. There exists algorithms for eliminating quantifiers which can decide the validity of propositions in these theories [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF][START_REF] Comon | Résolution de contraintes dans des algèbres de termes[END_REF]. We have extended this theory by giving a complete first-order axiomatization T of the evaluated trees [START_REF] Djelloul | About the combination of trees and rational numbers in a complete first-order theory[END_REF] which are combination of finite or infinite trees with construction operations and the rational numbers with addition, subtraction and a linear dense order relation. This theory reflects essentially to Prolog III and IV which have been modeled using combination of trees, rational numbers, booleans and intervals [START_REF] Colmerauer | An introduction to Prolog III[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF]. In this paper we describe a general algorithm for solving first-order constraints in T , i.e. in all models of T . Our aim is not only to decide the validity of the propositions, but to be able to express solutions of constraints in T , which can possibly contain free variables, in a simple and explicit way.

Description of the algorithm

The algorithm is not simply a combination of an algorithm over trees with one over rational numbers, but a powerful mechanism which is able to solve any firstorder constraint containing typed/untyped variables and presents the solutions on the free variables in a clear and explicit way. One of the major difficulty resides in the fact that the theory of trees does not accept full elimination of quantifiers and the function symbols + and -of T have two different behaviors whether they are applied on trees or on rational numbers. The main points of the algorithm are (full description of the algorithm can be found in [START_REF] Dao | Solving First-Order Constraints in the Theory of the Evaluated Trees[END_REF]):

-We define basic formulas, which are conjunctions of formulas of the forms true, false, num x, tree x , x = y, x = f y 1 ...y n , Σ n i=1 a i x i = a 0 1, Σ n i=1 a i x i < a 0 1, with x i , y j variables and a i ∈ Z and give a mechanism to derive typing constraints in basic formulas.

-We define blocks, which are basic formulas where all the variables are typed and where there is no type conflict and define solved blocks.

-We give the definition of working formulas, which are formulas written by using only existentially quantified blocks and their negation. To be able to the rewriting rules, which are the heart of the algorithm, we give to each negation symbol ¬ a number, which will present properties of the corresponding working formula. Using these number, we define initial, final formulas, and solving formulas.

-We give a set of 28 rewriting rules, which transform an initial working formula into a conjunction of final working formulas, which can be directly transformed into a disjunction of solving formulas, which is either true or false or a formula ϕ having at least one free variable such that neither T |= ϕ nor T |= ¬ϕ. These rules make top-down local solvings and propagations and bottom-up quantifier eliminations and distributions. We show that these rules are correct and terminating.

Conclusion

The non-elementarity of the decision in the theory of trees is known [START_REF] Vorobyov | An Improved Lower Bound for the Elementary Theories of Trees[END_REF], i.e the complexity of the decision cannot be bounded by a tower of powers of 2's with a fixed height. Thus our algorithm must not escape this kind of complexity in the worst case. We have programmed a similar algorithm on the theory of trees and nevertheless could be able to solve formulas of winning positions in two partner games, having 160 nested quantifiers [START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis[END_REF]. Actually we try to extend our algorithm to any combination of a theory T with the theory of finite or infinite trees.


Khalil Djelloul

Thi-Bich-Hanh Dao

Complete First-Order Axiomatization of Finite or Infinite M-extended Trees

  L'archive ouverte pluridisciplinaire

Introduction

Recall that a tree built on a set E is essentially a hierarchized set of nodes labelled by the elements of E. To each element e of E corresponds an operation f , called construction operation, which, starting from a sequence a 1 , . . . , a n of trees, builds the tree whose top node is labelled e and whose sequence of immediate children is a 1 , . . . , a n .

The algebra of finite or infinite trees plays a fundamental act in computer science: it is a model for composed data known as record in Pascal or structure in C. The construction operation corresponds to the creation of a new record, i.e. of a cell containing an elementary information possibly followed by n cells, each one pointing to a record. Circuit of pointers correspond to infinite trees.

As early as 1976, G. Huet proposed an algorithm for unifying infinite terms, that is solving equations in that algebra [START_REF] Huet | Resolution d'equations dans les langages d'ordre 1[END_REF]. B. Courcelle has studied the properties of infinite trees in the scope of recursive program schemes [START_REF] Courcelle | Equivalences and Transformations of Regular Systems applications to Program Schemes and Grammars[END_REF]. A. Colmerauer has described the execution of Prolog II, III and IV programs in terms of solving equations and disequations in that algebra [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Colmerauer | An introduction to Prolog III[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF]. The unification of finite terms, i.e. solving conjunctions of equations in the theory of finite trees has first been studied by A. Robinson [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF]. Some better algorithms with better complexities has been proposed after by M.S. Paterson and M.N.Wegman [START_REF] Paterson | Linear unification[END_REF] and A. Martelli and U. Montanari [START_REF] Matelli | An efficient unification algorithm[END_REF]. Solving conjunctions of equations in the theory of infinite trees has been studied by G. Huet [START_REF] Huet | Resolution d'equations dans les langages d'ordre 1[END_REF], by A. Colmerauer [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF] and by J. Jaffar [START_REF] Jaffar | Efficient unification over infinite terms[END_REF]. Solving conjunctions of equations and disequations in the theory of possibly infinite trees has been studied by A. Colmerauer [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF] and H.J. Bürckert [START_REF] Bürckert | Solving disequations in equational theories[END_REF]. An incremental algorithm for solving conjunctions of equations and disequations on rational trees has been proposed after by V.Ramachandran and P. Van Hentenryck [START_REF] Ramachandran | Incremental algorithms for constraint solving and entailment over rational trees[END_REF]. On the other hand, there exists a quantification elimination algorithm which transforms a first-order formula into a boolean combination of simple ones. In the case of infinite trees with a finite set of function symbols we can refer to the work of M.J. Maher [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF] and H. Comon [START_REF] Comon | Unification et disunification : Théorie et applications[END_REF]. M.J. Maher has summarized all these cases and proposed a complete axiomatizations for different sets of trees equipped with construction operations [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF].

In this paper, we give and justify an axiomatization of the structure of finite or infinite M -extended trees. This structure is an intuitive combination of the structure of trees with another structure M and can be seen semantically as an extension to trees of the model M . Having a structure M = (D M , F M , R M ) together with its domain D M , its set of operations F M and its set of relations R M , we define the M -extended tree structure Ext M = (D, F, R) whose domain D consists of trees labelled by elements of D M ∪ F , where F is an infinite set of function symbols containing F M and another infinite set of function symbols disjoint from F M . For each n-ary function f ∈ F , the operation f (a 1 , ..., a n ) is evaluated in M and produces an element of D M if f ∈ F M and all the a i are elements of D M , or is a tree whose root is labelled by f and whose immediate children are a 1 , ..., a n otherwise. The set of relations R is built essentialy from R M . In the case where M is the set of rational numbers together with the operations of addition and substraction and a linear dense order relation we can refer to Prolog III and IV whose execution has been modelized by A. Colmerauer [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF] using this M -extended trees.

The paper is organized in four sections followed by a conclusion. This introduction is the first section. In the second section we recall the Maher's structure of finite or infinite trees and introduce the M -extended trees structure for any model M . In the third section, we present our general sufficient conditions for the completeness of any first-order theory. Then, having a first-order axiomatization T of M , we give a first-order axiomatization T of finite or infinite M -extended trees. Finally we present in the fourth section a new class of theories that we call flexible and show that if T is flexible then T is complete. To show the completeness of T for any flexible theory T we use the general sufficient conditions presented in the third section. The definition of the M -extended trees, the axiomatization of T , the definition of flexible theories and the proof of the completeness of T for every flexible theory T are our main contribution in this paper.

Extension to trees of a model M

Finite or infinite trees

Let F be an infinite set of function symbols and R be a set of relation symbols.

To each element of F ∪ R is associated an integer, its arity. The arities are nonnegative for elements of F and are positive for elements of R. An n-ary symbol is a symbol with arity n. A constant is a 0-ary symbol.

Let N be a set of words of positive integers, including the empty word . Let "." denote concatenation of word. A tree built on F is a mapping a : E → F , for some non-empty subset E of N such that each element i

1 . . . i k (with k ≥ 0) satisfies two conditions: (1) if k > 0 then i 1 . . . i k-1 ∈ E and (2) if a(i 1 . . . i k ) = f and f has arity n, then i 1 . . . i k i k+1 ∈ E if and only if 1 ≤ i k+1 ≤ n.
The subtree of the tree a at n ∈ E is the mapping a : E → F where

D = {d|n.d ∈ E} and a (d) = a(n.d).
The set of all trees built on F is denoted A. To each n-ary function symbol f we associate a function from A n to A also denoted f such that f (a 1 , . . . , a n ) = a where a( ) = f and a(i.d) = a i (d) for 1 ≤ i ≤ n and d a node. These functions are called construction operations. The set of trees A with these construction operations forms the tree structure or tree algebra.

Finite or infinite M -extended tree structure

We are given now once for all a structure M = (D M , F M , R M ) with its domain D M , its set of functions F M and its set of relations R M . Let F be an infinite set of function symbols containing the set F M and another infinite set of function symbols disjoint from F M . Let R be the set of relation symbols R M ∪ {p}, with p a unary relation symbols which does not belong to R M . The extension to trees of the model M , quite simply called M -extended trees model is the model Ext M = (D, F, R) defined as follows:

-the domain D is the set of the trees built on F ∪ D M where each element f ∈ F of arity n is considered as a label of arity n and each element of D M is considered as a label of arity 0, -to each n-ary element f of F is associated a function f : An occurrence of a variable x in a formula is bound if it occurs in a subformula of the form (∃xϕ) or (∀xϕ). It is free otherwise. The free variables of a formula are those which have at least a free occurrence in the formula. For each formula ϕ, we denote by var(ϕ) the set of all free variables of ϕ.

D n → D such that f (a 1 , .., a n ) is the result of f on (a 1 , .., a n ) in D M , if f ∈ F M and a i ∈ D M for all i,
We call instantiation of a formula ϕ by individuals of D M the obtained formula from ϕ in which for each free variable x in ϕ, we replace each free occurrence of x by the same individual i of D M .

Theory and complete theory

Let x = x 1 . . . x n and ȳ = y 1 . . . y n be two vectors of variables of the same length. Let ψ, φ, ϕ and ϕ(x) be formulae. We write

∃x ϕ for ∃x 1 ...∃x n ϕ, ∀x ϕ for ∀x 1 ...∀x n ϕ, ∃?x ϕ(x) for ∀x∀ȳ ϕ(x) ∧ ϕ(ȳ) → i∈{1,...,n} x i = y i , ∃!x ϕ for (∃x ϕ) ∧ (∃?x ϕ).
Note that the formulae ∃?εϕ and ∃!εϕ are respectively equivalent to true and to ϕ in any model M . Theses quantifiers are just convenient notations and can be expressed in the first-order level.

Definition 3.1.1 Let Ψ (u) be a set of formulas having at most u as a free variable. We write M |= ∃

Ψ (u)
o ∞ x ϕ(x), iff for any instantiation ∃x ϕ (x) of ∃x ϕ(x) by individuals of D M one of the following properties holds:

-the set of the individuals i of D M such that M |= ϕ (i), is empty, -for all finite sub-set {ψ 1 (u), .., ψ n (u)} of elements of Ψ (u), the set of the individuals i of D M such that M |= ϕ (i) ∧ j∈{1,...,n} ¬ψ j (i) is infinite.

A theory is a set of propositions. We say that the model

M is a model of T iff for each element ϕ of T , M |= ϕ. If ϕ is a formula, we write T |= ϕ iff for each model M of T , M |= ϕ. A theory T is complete if for each proposition ϕ, either T |= ϕ or T |= ¬ϕ. A complete axiomatization of a structure M is a recursive set T of propositions such that for each proposition ϕ, T |= ϕ iff M |= ϕ.
In what follows we use the abbreviation wnfv for "without new free variables". By saying a formula ϕ is equivalent to a wnfv formula ψ in T we mean T |= ϕ ↔ ψ and ψ does not contain other free variables than those of ϕ. The following theorem states general sufficient conditions for the completeness of a theory T .

Theorem 3.1.2 [9, 10] A theory T is complete if there exists a set Ψ (u) of formulas, having at most u as free variable, a set A of formulas, closed under conjunction and renaming, a set A of formulas of the form ∃xα with α ∈ A, and a sub-set

A of A such that:

1. every flat atomic formula is equivalent in T to a wnfv Boolean combination of basic formulas of the form ∃xα with α ∈ A, 2. every formula without free variables of the form ∃x α ∧ α with ∃x α ∈ A and α ∈ A is equivalent either to false or to true in T , 3. every formula of the form ∃x α ∧ ψ, with α ∈ A and ψ any formula, is equivalent in T to a wnfv formula of the form:

∃x α ∧ (∃x α ∧ (∃x α ∧ ψ)), with ∃x α ∈ A , α ∈ A , α ∈ A and T |= ∀x α → ∃!x α , 4. if ∃x α ∈ A then T |= ∃?
x α and for each free variable y in ∃x α , at least one of the following properties holds:

-T |= ∃?y x α , -there exists ψ(u) ∈ Ψ (u) such that T |= ∀y (∃x α ) → ψ(y), 5. if α ∈ A then -the formula ¬α is equivalent in T to a wnfv formula of the form i∈I α i with α i ∈ A, -for each x , the formula ∃x α is equivalent in T to a wnfv formula which belongs to A , -for each x , T |= ∃ Ψ (u) o ∞ x α .

Axiomatization of the structure of M -extended trees

M. Maher has introduced a complete axiomatization of the structure of finite or infinite trees built on an infinite set F [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF]. The axiomatization is the set of propositions of the following forms:

1 ∀x∀ȳ f x = f ȳ → i x i = y i , 2 ∀x∀ȳ ¬f x = g ȳ, 3 ∀x∃!z i z i = t i (z, x),
where f, g ∈ F , x, y, z are variables, x is vector of variables x i , ȳ is vector of variables y i , z is vector of distinct variables z i and where t i (x, z) is a term which begins by an element of F followed by variables taken from x or z.

The first axiom is called axiom of explosion, the second axiom of conflict of symbols and the third axiom of unique solution.

Let T be an axiomatization of the structure M = (D M , F M , R M ). Using this axiomatization, let us now define an axiomatization T of the structure of finite or infinite M -extended trees together with the sets F and R (defined in section 2.2) as function and relation symbols.

Definition 3.2.1 An axiomatization T of the structure of finite or infinite Mextended trees is the set of propositions of the following forms where x, ȳ are vectors of variables x i , y i .

explosion: for each

f ∈ F ∀x∀ȳ ¬pf x ∧ ¬pf ȳ ∧ f x = f ȳ → i x i = y i 2. conflict of symbols: for f and g distinct symbols in F ∀x∀ȳ f x = g ȳ → pf x ∧ pg ȳ 3. unique solution ∀x∀ȳ ( i px i ) ∧ ( j ¬py j ) → ∃!z k (pz i ∧ z k = t k (x, ȳ, z))
where z is a vector of distinct variables z i , t k (x, ȳ, z) is a term expressed by a function symbol f k followed by variables taken from x, ȳ, z, moreover, if

f k ∈ F M , the term t k (x, ȳ, z) contains at least one variable from ȳ or z 4. relations of R M : for each r ∈ R M , ∀x rx → i px i 5. operations of F M : for each f ∈ F M , ∀x pf x ↔ i px i (this axiom, in the case of f a constant in F M , becomes pf ) 6. elements not in M : for each f ∈ F -F M , ∀x ¬pf x 7.
existence of at least one element satisfying p (only if F M does not contains 0-arity function symbols):

∃x px, 8. the extension of axioms of T : all axioms obtained by the following transformation of an axiom ϕ of T : While it is possible replace all sub-formula of ϕ which is of the form ∃x ψ, but not of the form ∃x ( px i ) ∧ ψ , by ∃x ( px i ) ∧ ψ and all sub-formula of ϕ which is of the form ∀x ψ, but not of the form ∀x

( px i ) → ψ , by ∀x ( px i ) → ψ.
Example 3.2.2 Let M be the structure of the rational numbers together with the operations of addition, substraction and a linear dense order relation without endpoints. In this case D M is the set of the rational numbers, F M = {+, -, 0, 1} and R M = {<}. Let a be a positive integer and let t 1 , ..., t n be terms. Let us denote by:

-t 1 < t 2 , the term < t 1 t 2 , -t 1 + t 2 , the term +t 1 t 2 , -t 1 + t 2 + t 3 , the term +t 1 (+t 2 t 3 ), --at 1 , the term (-t 1 ) + • • • + (-t 1 ) a , -0t 1 , the term 0, -at 1 , the term t 1 + • • • + t 1 a , -a the term 1 + • • • + 1 a .
The axiomatization T of the structure M is of the form

1 ∀x∀y x + y = y + x, 2 ∀x∀y∀z x + (y + z) = (x + y) + z, 3 ∀x x + 0 = x, 4 ∀x x + (-x) = 0, 5 n ∀x nx = 0 → x = 0, 6 n ∀x ∃!yny = x, (n = 0) 7 ∀x ¬x < x, 8 ∀x∀y∀z (x < y ∧ y < z) → x < z, 9 ∀x∀y (x < y ∨ x = y ∨ y < x), 10 ∀x∀y x < y → (∃z x < z ∧ z < y),
11 ∀x ∃y x < y, 12 ∀x ∃y y < x, 13 ∀x ∀y ∀z x < y → (x + z < y + z), 14 0 < 1. Using the transformations of Definition 3.2.1, the axiomatization T of the Mextended trees theory is of the form:

1 ∀x∀ȳ ((¬p f x) ∧ (¬p f ȳ) ∧ f x = f ȳ) → i x i = y i , 2 ∀x∀ȳ f x = g ȳ → p f x ∧ p g ȳ, 3 ∀x∀ȳ ( i∈I p x i ) ∧ ( j∈J ¬p y j ) → (∃!z k∈K (¬p z k ∧ z k = t k (x, ȳ, z))), 4 p0, 5 p1, 6 ∀x∀y x < y → (p x ∧ p y), 7 ∀x∀y p x + y ↔ p x ∧ p y, 8 ∀x p -x ↔ p x, 9 ∀x ¬p hx , 10 ∀x∀y (p x ∧ p y) → x + y = y + x, 11 ∀x∀y∀z (p x ∧ p y ∧ p z) → x + (y + z) = (x + y) + z, 12 ∀x p x → x + 0 = x, 13 ∀x p x → x + (-x) = 0, 14 n ∀x p x → (nx = 0 → x = 0), 15 n ∀x p x → ∃!yp y ∧ ny = x, (n = 0) 16 ∀x p x → ¬x < x , 17 ∀x∀y∀z p x ∧ p y ∧ p z → ((x < y ∧ y < z ) → x < z ), 18 ∀x∀y (p x ∧ p y) → (x < y ∨ x = y ∨ y < x ), 19 ∀x∀y (p x ∧ p y) → (x < y → (∃z p z ∧ x < z ∧ z < y)), 20 ∀x p x → (∃y p y ∧ x < y), 21 ∀x p x → (∃y p y ∧ y < x ), 22 ∀x ∀y ∀z (p x ∧ p y ∧ p z ) → (x < y → (x + z < y + z )), 23 0 < 1,
where f and g are two distinct function symbols taken from F , h ∈ F -F M , x, y, z are variables, x is a vector of variables x i , ȳ is a vector of variables y i , z is vector of distinct variables z i and where t k (x, ȳ, z) is a term which begins by a function symbol f k element of F followed by variables taken from x or ȳ or z, moreover, if f k ∈ F M then t k (x, ȳ, z) contains at least a variable taken from ȳ or z. This theory has been used by A. Colmerauer to modelize the execution of Prolog III and IV [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF].

Completeness of T

We suppose that the variables of V are ordered by a strict linear dense order relation denoted by . We call leader of an M -equation α the greatest variable x of all variables in α, according to the order , such that M |= ∃!xα. -true, false, px, ¬px,

-x = y, x = f x 1 . . . x n , with f ∈ F , -t 1 = t 2 ∧ n i=1 px i ,
x 0 = t 0 (x 1 ) ∧ x 1 = t 1 (x 2 ) ∧ • • • ∧ x n-1 = t n-1 (x n ) ∧ n-1 i=0 ¬px i ,
where x i+1 has an occurrence in the term t i (x i+1 ), then the variable x n and the equation x n-1 = t n-1 (x n ) are called reachable from x 0 in α.

-p x ∧ ¬p x , -x = hȳ ∧ p x , with h ∈ F -F M , -x = f 0 ∧ ¬p x , with f 0 a constant of F M , -x 0 = f x 1 ...x n ∧ ¬p x 0 ∧ n i=1 p x i , with f ∈ F M , -x 0 = f x 1 ...x n ∧ p x 0 ∧ ¬p x i , with f ∈ F -x 0 = x 1 ∧ p x 0 ∧ ¬p x 1 , -x 0 = x 1 ∧ ¬p x 0 ∧ p x 1 , -rt 1 ...t n ∧¬p x i with r ∈ R M

Completeness of T Theorem 4.3.1 If T is a flexible theory then T is complete.

We show this theorem using Theorem 3.1.2. The sets Ψ (u), A, A and A are chosen as follows:

-Ψ (u) is the set of the formulae of the form ∃ȳ u = f ȳ ∧ ¬p u, with f ∈ F not a constant. -A is the set of blocks.

-A is the set of the formulae of the form ∃x α , where:

• all the variables of x are reachable in α from free variables of ∃x α ,

• α is a solved equation block, different from the formula false, and where the order is such that all the variables of x are greater than the free variables of ∃x α , • all the equations of α of the form

x 0 = f x 1 ...x n with f ∈ F -F M are reachable in α from free variables of ∃x α , • if the M -equation t 1 = t 2 is a sub-formula of α then, each variable x i
which occurs in it is either a free variable of ∃x α or reachable in α from free variables of ∃x α , -A is the set of solved relation blocks.

Conclusion

We have defined in this paper the structure of the M -extended trees for any model M . This structure can be considered as a combination of the structure of finite or infinite trees with the structure M . Having used an axiomatization T of M we have given a first-order axiomatization T of the M -extended trees structure and have shown that if T is flexible then T is complete. To prove the completeness in this case, we have used our general sufficient condition. From this condition we can extract a general algorithm for solving first-order constraints in T . Due to lack of space we cannot present this algorithm in this paper. Just note that this algorithm uses the block defined in our paper and transforms any formula ϕ in a particular formula ψ called solved formula equivalent to ϕ in T . In particular if ϕ has no free variables then ψ is either the formula true or the formula false. The correctness of our algorithm is another proof of the completeness of T of each flexible theory T .

There exists a lot real and practical problems which can be represented by full first-order formulae on M -extended trees. We can site for example the works of A. Colmerauer [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF] who has realized the execution of Prolog III and IV using the M -extended trees where M is the structure of the rational numbers together with the operations of addition and substraction and linear dense order relation.

On the other hand S. Vorobyov [START_REF] Vorobyov | An Improved Lower Bound for Elementary Theories of Trees, Proceeding of the 13th Conference on Automated Deduction[END_REF] have shown that the problem of deciding if a proposition without free variables is true or not in the tree theory is nonelementary, i.e. the complexity of all algorithm which solve it is not bounded by a tower of powers of 2 s (with a top down evaluation) with a fixed height. A.

Colmerauer and B. Dao [START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis[END_REF][START_REF] Colmerauer | Expressiveness of full first-order constraints in the algebra of finite or infinite trees[END_REF] have also given a proof of non-elementary complexity of solving constraints in the tree theory. Thus, it is normal that our sufficient condition is complex and the properties of our blocks uses some nonclassical quantifiers. Nevertheless we hope find some interesting class of complexities in the implementation of our algorithm as it has been done in [START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis[END_REF] in the theory of finite or infinite trees.

Actually we try to show the completeness of T where M is the structure of the real numbers together with addition, substraction, multiplication and a linear dense order relation. We also study the complexity and the expressiveness of the first-order constraints in T as it has done in [START_REF] Colmerauer | Expressiveness of full first-order constraints in the algebra of finite or infinite trees[END_REF][START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis[END_REF].

Let us show that every flat atomic formula ϕ is equivalent in T to a wnfv Boolean combination of basic formulas, i.e. a wnfv Boolean combination of formulas of the form ∃xα with α ∈ A. Let ϕ be a flat atomic formula. If ϕ is of the form true, false, px or ¬p x , then ϕ is a block which is quantified by the empty vector ε, thus, ϕ is equivalent in T to ∃εϕ with ϕ ∈ A, which is clearly a wnfv Boolean combination of basic formulas. Else, the following equivalences, after having distributed the ∧ on the ∨ and the ∃ on the ∨, give the adequate Boolean combinations:

T |= rx 0 ...x n ↔ ∃ε rx 0 ...x n ∧ n i=0 (p x i ∨ ¬p x i ) , T |= x 0 = x 1 ↔ ∃ε x 0 = x 1 ∧ 1 i=0 (p x i ∨ ¬p x i ) , T |= x 0 = f x 1 ...x n ↔ ∃ε x 0 = f x 1 ...x n ∧ n i=0 (p x i ∨ ¬p x i ) , with r ∈ R -{p}, f ∈ F .
Thus T satisfies the first condition of Theorem 3.1.2.

T satisfies the second condition

Let us show that every formula ϕ, without free variables, of the form ∃x α ∧ α with ∃x α ∈ A and α ∈ A , is equivalent to true or to false in T . Since the formula ϕ does not contain free variables, then there are no reachable variables and no reachable equations in α from the free variables of ∃x α and thus according to section 5.1 x = ε. From this and since ∃x α does not contains free variables we deduce then that var(α ) = ∅. But according to section 5.1 α is a solved block different from false, thus according to the definition of solved blocks (first point) the formula α is the formula true. Then ϕ is equivalent in T to the formula without free variables α . According to section 5.1, the formulas α is a solved conjunction of relation blocks and thus according to the definition of the solved blocks (first point) α is either the formula true or false then ϕ is either equivalent to false or to true in T . Thus the theory T satisfies the second condition of Theorem 3.1.2.

T satisfies the third condition

Let us first introduce the following convenient definition.

Definition 5.4.1 Let α be a solved block. We call non-trees formula each block of the form

t 1 = t 2 ∧ n i=1 px i (1)
with var(t

1 = t 2 ) = {x 1 , ..., x n } and t 1 , t 2 M -terms. If (1
) is a sub-formula of α then we call α-leader of the non-trees formula [START_REF] Benhamou | Le manuel de Prolog IV[END_REF], the α-leader of the M -equation

t 1 = t 2 .
Let us show that every formula of the form ∃x α ∧ ψ, with α ∈ A and ψ any formula, is equivalent in T to a wnfv formula of the form

∃x α ∧ (∃x α ∧ (∃x α ∧ ψ))), (2)
with ∃x α ∈ A , α ∈ A , α ∈ A and T |= ∀x α → ∃!x α .
Let us choose the order such that all the variables of x are greater than the free variables of ∃xα. Let β be the solved formula of α, ( β exists according to Property 4.2.8). Let X be the set of the variables of the vector x. Let Y rea be the set of the reachable variables in β from the free variables of ∃xβ and let Y nrea be the set of the no-reachable variables in β from the free variables of ∃xβ. Let us now rename the variables of Y nrea ∩ X which have at least an occurrence in a sub-non-trees-formula of β by variables greater than the other variables of β (according to the order ). Note that theses variables are quantified (they are elements Y nrea ∩ X ), thus we can rename them in ∃xβ. Let β * be the solved formula of β. Let Lead be the set of the β * -Leaders of all the equations of β * . If f aux is a sub-formula of β * then: x = x = x = ε, α = true, α = false and α = true. Else: -x contains the variables of X ∩ Y rea , -x contains the variables of (X -Y rea ) -Lead.

-x contains the variables of (X -Y rea ) ∩ Lead.

-α is of the form α 1 ∧ α 2 where α 1 is the conjunction of (1) all the reachable equations in β * from the free variables of ∃xβ * , (2) all the sub-non-trees-formulas of β * whose β * -leader is not element of Y nrea ∩X. α 2 is the conjunction of all the sub-formulas of β * of the form p x or ¬p x with x having at least an occurrence in α 1 .

-α is of the form α 1 ∧ α 2 where α 1 is the conjunction of all the sub-formulas of β * of the form p x or ¬p x with x / ∈ x , α 2 is the conjunction of all the sub-formulas of β * of the form rt 1 ...t n .

-α is of the form α 1 ∧α 2 where α 1 is the conjunction of (1) all the equations which are not reachable in β * from the free variables of ∃xβ * , (2) all the sub-nontrees-formulas of β * whose β * -leader belongs to Y nrea ∩ X. α 2 is the conjunction of all the sub-formulas of β * of the form p x or ¬p x with x having at least an occurrence in α 1 .

By construction of the sets A and A it is clear that ∃x α ∈ A , α ∈ A and α ∈ A. Moreover, Since x = (X -Y rea ) ∩ Lead and since the blocks are solved (thus well typed), then according to the axiom 3 of T (unique solution) and the definition of solved blocks (point 3 and 4) and the properties of the α-leaders we get T |= ∀x α → ∃!x α . Thus T satisfies the third condition of Theorem 3.1.2.

T satisfies the fourth condition

Let us show now that T satisfies the fourth condition of Theorem 3.1.2, i.e. if ∃x α ∈ A then T |= ∃?x α . Since ∃x α ∈ A and according to section 5.1, the variables of x are reachable in α from the free variables of ∃x α . Thus, using Property 4.2.3 we get T |= ∃?x α .

Let us show now that if y is a free variable of ∃x α then T |= ∃?yx α or there exists ψ(u) ∈ Ψ (u) such that T |= ∀y (∃x α ) → ψ(y). Let y be a free variable of ∃x α . Since α is a solved equation block different from false then three cases arise:

Either y occurs in a sub-formula of α of the form y = t(x , z , y)∧¬py, where z is the set of the free variables of ∃x α which are different from y, t(x , z , y) is a term which begins by an element of F followed by variables taken from x or z or {y}. In this case, the formula ∃x α implies in T the formula ∃x y = t(x , z , y) ∧ ¬p y, which implies in T the formula

∃x z w y = t(x , z , w) ∧ ¬p y, (3)
where y = t(x , z , w) is the formula y = t(x , z , y) in which we have replaced every free occurrence of y in the term t(x , z , y) by the variable w. According to section 5.1, the formula (3) belongs to Ψ (y).

Or y occurs in a sub-formula of α of the form y = z ∧ ¬py. In this case:

1. Recall that according to section 5.1, x contains the quantified reachable variables and the order is such that all the variables of x are greater than the free variables of ∃x α thus greater than y. 2. According to the definition of solved blocks and α -leader, we have y z and y is the α -leader of y = z.

From ( 1) and ( 2), we deduce that z is a free variable in ∃x α . Since α is a solved block, y is not α -leader in any other equation of α (because all the α -leaders are distinct), thus y can not appear in another left hand side of an equation of α (because ¬px and α is well typed), thus since the variables of x are reachable in α from the free variables of ∃x α (section 5.1), all the variables of x keep reachable in α from the free variables of ∃x y α (see Definition4.2.2 of reachable variable). More over, for each value of the free variable z there exists at most a value for y. Using this and Property 4.2.3 we get T |= ∃?x y α .

Or y occurs only in sub-formulas of the form

x 0 = t(y) ∧ ¬px 0 or t 1 = t 2 ∧ i∈I px i ( 4
)
with t(y) a term which begins by an element of F ∈ F and contains at least an occurrence of y. t 1 = t 2 ∧ i∈I px i is a non-trees-formula. Recall that according to section 5.1, x contains the quantified reachable variables. According to section 5.1, all the variables of x and all the equations of the form x 0 = t(y) ∧ ¬px 0 are reachable in α from the free variables of ∃x α . (1) if ¬py is a sub-formula of α then since α is well typed then y does not occur in any non-trees-formula. Since y does not occur in a left-hand side of an equation of α then the variables of x y keep reachable in α from the free variables of ∃x y α and thus using Property 4.2.3 we get T |= ∃?x y α . (2) If y occurs in a sub-formula of α of the form py then (i) if y occurs in a non-trees-formula of α then using the last point of the solved block definition we get T |= ∃?y α , using this and using the fact that α contains py and not ¬py then the variables of x keep reachable in α from the free variables of ∃x y α and thus using Property 4.2.3 we get T |= ∃?x y α (ii) else since y does not occur in a left-hand side of an equation of α of the form y = f x 1 ...x n or y = x 1 then the variables of x y keep reachable in α from the free variables of ∃x y α and thus using Property 4.2.3 we get T |= ∃?x y α . In all the other cases the blocks are not well typed thus not solved and thus can not be element of A . In all cases T satisfies the fourth condition of Theorem 3.1.2.

T satisfies the fifth condition

T satisfies the first point of the fifth condition Let us show that if α ∈ A then the formula ¬α is equivalent in T to a disjunction of elements of A, i.e. a disjunction of blocks. Let α a formula of A .

According to section 5.1, either α is the formula false and thus ¬α is the formula true which clearly belongs to A , or α is a formula of the form β ∧ ( T satisfies the second point of the fifth condition Let us show that if α ∈ A then for every variable x , the formula ∃x α is equivalent in T to an element of A . Let α be a formula of A , three cases arise:

If x has no occurrences in α then the formula ∃x α is equivalent in T to α which belongs to A .

If the formula ∃x α is of the form ∃x α 1 ∧ ¬p x with α 1 ∈ A and x has no occurrences in α 1 then the formula ∃x α is equivalent in T to α 1 ∧ (∃x ¬p x ), which, according to our axiomatization is equivalent in T to α 1 , which belongs to A .

If the formula ∃x α is of the form ∃x α 1 ∧ ϕ with ϕ a relation block containing at least a formula of the form rt 1 ...t n with r ∈ R M and x has no occurrences in α 1 , then the formula ∃x α is equivalent in T to α 2 ∧ (∃x ϕ), with α 2 a block of the form α 1 ∧ φ where φ is a conjunction of sub-formulas of α 1 of the form ¬px or px with x ∈ var((α 1 ∩ ϕ) -{x }). According to the last point of the definition of flexible theory, the preceding formula is wnfv equivalent in T to false or to to α 2 ∧ ϕ .

Since α 2 belongs to A and ϕ does not contains new variables (wnfv) then preceding formula belongs to A . In all cases T satisfies the second point of the fourth condition of Theorem 3.1.2.

T satisfies the third point of the fifth condition First, we present two properties which hold in any model of T . The first one results from the axiomatization of T and introduce the notion of zero-infinite in M. The second one is due to the fact that T is flexible thus all model M of T is also flexible (more exactly the last point of the definition of flexible model). Let M be a model of T . Recall that Ψ (u) is the set of formulae of the form ∃ȳ u = f ȳ ∧ ¬p u, with f ∈ F -F 0 . Let ϕ(x) be a formula which belongs to A , let us show that, for every variables x we have T |= ∃ Ψ (u) o ∞ x ϕ(x). Let M be a model of T and let ∃x ϕ (x) be an any instantiation of ∃x ϕ(x) by individuals of M such that M |= ∃x ϕ (x). Having an any condition of the form

M |= ϕ (i) ∧ ¬ψ 1 (i) ∧ • • • ∧ ¬ψ n (i),
with ψ j (u) ∈ Ψ (u), it is enough to show that there exists an infinity of individuals i of M which satisfy this condition. This condition can be replaced by the following stronger condition

M |= p i ∨ ψ n+1 (i) ∧ ϕ (i) ∧ ¬ψ 1 (i) ∧ • • ∧¬ψ n (i),
where ψ n+1 (u) is an element of Ψ (u) which has been chosen different from ψ 1 (u), . . . , ψ n (u), (always possible because the set F -F M is infinite). Since for every k between 1 and n, we have:

-T |= p x → ¬ψ k (x) -T |= ψ n+1 (x) → ¬ψ k (x) (axiom 2of T conflict of symbol).

The preceding condition is simplified to

M |= (p i ∧ ϕ (i )) ∨ (ψ n+1 (i ) ∧ ϕ (i ))
and thus, knowing that M |= ∃x ϕ (x), it is enough to show that there exists an infinity of individuals i of M such that

M |= p i ∧ ϕ (i ) or M |= ψ n+1 (i ) ∧ ϕ (i ). (6)
Two cases arise: Either the formula p x occurs in ϕ (x). Since ϕ (x) is an instantiation of a solved relation block and M |= ∃x ϕ (x), the formula p x ∧ ϕ (x ) is equivalent in M to a M -formula of the form [START_REF] Comon | Unification et disunification : Théorie et applications[END_REF]. According to Property 5.6.2 and since M |= ∃x p x ∧ ϕ (x ), there exists an infinity of individuals i of M such that M |= p i ∧ ϕ (i ) and thus, such that [START_REF] Courcelle | Equivalences and Transformations of Regular Systems applications to Program Schemes and Grammars[END_REF].

Or, the formula p x does not occur in ϕ (x). Since ϕ (x) is an instantiation of a solved relation block and M |= ∃x ϕ (x), the M -formula ψ n+1 (x) ∧ ϕ (x) is equivalent in M to ψ n+1 (x). According to Property 5.6.1 there exists an infinity of individuals i of M such that M |= ψ n+1 (i), thus, such that M |= ψ n+1 (i) ∧ ϕ (i) and thus such that (6).

This article was processed using the L A T E X macro package with LLNCS style

4. 1

 1 Flexible structure The model M is called flexible if for each conjunction α of M -equations and each conjunction β of M -relations: 1. α is equivalent in M either to false or to a wnfv conjunction α of Mequations whose each element has a distinct leader which has one and only occurrence in α , and for all variable x ∈ var(α ) we have M |= ∃!xα , 2. the formula ¬β is equivalent in M to a wnfv disjunction of M -equations and M -relations, 3. for all x ∈ V -the formula ∃x β is equivalent in M either to false or to a quantifier free conjunction of M -relations, -for all x ∈ V and for all instantiation ∃x β (x) of ∃x β(x) by individuals of D M , either M |= ¬∃xβ (x) or there exists an infinite set of individuals i of D M such that M |= β (i).A theory T is called flexible iff all its models are flexible. Property 4.1.1 If T is flexible then it is complete. 4.2 Blocks and solved blocks in T Definition 4.2.1 A block is a conjunction α of formulae of the following forms:

Property 4 . 2 . 3

 423 Let α be a block. If all the variables of x are reachable in α from free variables of ∃xα, then T |= ∃?xα. Definition 4.2.4 A block α is called well-typed iff α does not contain subformulae of one of the following forms:

  x∈X px) ∧ ( y∈Y ¬py), with β a conjunction of M -relations β k with var(β) ⊆ X ∪ Y . According to the second point of the definition of the flexible theory we have T |= ¬β ↔ β where β is a disjunction of M -relations and M -equations. Thus, the formula ¬α is equivalent in T to a wnfv formula of the form ( k∈K (β k ∧ p k )) ∨ ( x∈X ¬px) ∨ ( y∈Y py), where β k is an M -equation or an M -relation, p k is a conjunction of formula of the form px for all variable x ∈ var(beta k ). This formula is clearly a disjunction of blocks. In all cases T satisfies the first point the fifth condition of Theorem 3.1.2.

Property 5 . 6 . 1 5 )

 5615 Let F 0 the set of the 0-ary function symbols of F . Let M be a model of T and let f ∈ F -F 0 . The set of the individuals i of M, such that M |= ¬p i and the set of the individuals i of M, such that M |= ∃x i = f x∧¬pi, are infinite. Property 5.6.2 Let M be a model of T . Let j∈J r j (x) be a conjunction of relation blocks. Let ∃x j∈J r j (x) be an instantiation of ∃x j∈J r j (x) by individuals of M. Let ϕ(x) the formula p x ∧ j ∈J r j (x ). (The set of the individuals i of M such that M |= ϕ(i) is empty or infinite.

  and is the result of the construction operation f on (a 1 , .., a n ) otherwise, -to each n-ary relation symbols r of R-{p} is associated the set r Ext M = r M .To the unary relation symbols p is associated the setp Ext M = D M . V ,s, t and the t i 's are terms, r is an n-ary relation symbol in R and ϕ and ψ are shorter formulae. Formulae of the first form are called equations and of the second form relations. A M -equation is an equation of M -terms and a M -relation is a relation rt 1 ...t n with r ∈ R M and the t i 's M -terms.

	A M -term is either a variable or a term whose function symbols are elements of
	F M . A formula is an expression of the forms
	s = t, rt 1 ..t n , true, false, ¬(ϕ), (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ), ∃xϕ, ∀xϕ,
	where x ∈
	3 Theory of finite or infinite M -extended trees
	Let V an infinite countable set of variables. A term is an expression of the form x
	or f t 1 . . . t n where n ≥ 0, f an n-ary symbol in F and the t i 's are shorter terms.

  where {x 1 , . . . , x n } is the set of variables which occur in the M -equation t 1 = t 2 , -rt 1 . . . t n , where r ∈ R M and the t i 's are M -terms, and such that α contains px or ¬px for each variable x ∈ var(α). A relation block is a block without equations. An equation block is a block without M -relations and where each variable has an occurrence in at least one equation. Definition 4.2.2 If a block α has a sub-formula of the form

  ), 5. for all variable x which occurs in an equation of α we have T |= ∃?xα. Let α be a solved equation block different from the formula false and let x be the set of the α-leaders of the equations of α. We have T |= ∃!xα.

	Property 4.2.7 Property 4.2.8 If T is flexible then each block is equivalent in T to a solved
	block.

and x i a variable which occurs in the M -relation rt 1 ...t n . Definition 4.2.5 Let t 1 be a term. Let t 2 and t 3 be two M -terms. Let α be a well-typed equation block. Either x = t 1 ∧ ¬px is a sub-formula of α. In this case, x is called α-leader of the equation x = t 1 . Else t 2 = t 3 ∧ i∈var(t2=t3) pi is a sub-formula of α. In this case, the greatest variable in var(t 2 = t 3 ) according to the order such that T |= ∃!x t 2 = t 3 ∧ i∈var(t2=t3) pi is called α-leader of the equation t 2 = t 3 . Definition 4.2.6 A block α is called solved block, iff: 1. α is well-typed and does not contain formulae of the form t 1 = t 2 or rt 1 ...t n with r ∈ R M and the t i 's terms which does not contain variables, 2. for each equation x = y in α, x y, 3. each equation in α has a distinct α-leader which does not occur in Mrelations of α, 4. if px and py are sub-formulas of α with x and y two α-leaders of two equations α 1 , α 2 of α then x ∈ var(α 2

Acknowledgements We thank Alain Colmerauer for our many discussions and his help in the organization and the drafting of this paper. We thank him too, for the definitions and proof of his course of DEA. We dedicate to him this paper with our best wishes for a speedy recovery.

Appendix

Theorem 3.1.2 If T is a flexible theory then T is complete.

Proof. We show this theorem using Theorem 3.1.2. The sets Ψ (u), A, A and A are chosen as follows:

5.1 Choice of the sets Ψ (u), A, A and A -Ψ (u) is the set of the formulae of the form ∃ȳ u = f ȳ ∧¬p u, with f ∈ F -F 0 .

-A is the set of blocks.

-A is the set of the formulae of the form ∃x α , where:

• all the variables of x are reachable in α from free variables of ∃x α , • α is a solved equation block, different from the formula false, and where the order is such that all the variables of x are greater than the free variables of ∃x α , • all the equations of α of the form

which occurs in it is either a free variable of ∃x α or reachable in α from free variables of ∃x α , -A is the set of solved relation blocks.

Note 5.1.1 Note that, A is closed under conjunction and renaming and A is a sub-set of A.

Let T be a flexible theory. Let us show that T satisfies the five conditions of Theorem 3.1.2.