doc_en.properties

axiom_Antonym1_diagnostic=antonymy
axiom_Antonym1_justification=by antonymy of 'youngest' and 'oldest'
axiom_Antonym2_diagnostic=antonymy
axiom_Antonym2_justification=by antonymy of 'youngest' and 'oldest'
axiom_Superlative1_diagnostic=uniqueness
axiom_Superlative1_justification=by uniqueness of the youngest
axiom_Superlative2_diagnostic=uniqueness
axiom_Superlative2_justification=by uniqueness of the oldest
axiom_adabsurdium_diagnostic=ad absurdum
axiom_adabsurdium_justification=by ad absurdum reasoning
axiom_addsub_diagnostic=addition and subtraction
axiom_addsub_justification=by adding and subtracting {1} to {0}
axiom_app_def_diagnostic=mapping
axiom_app_def_justification=by definition of {0} applied to {1}
axiom_app_sqrt_bounded_diagnostic=square root
axiom_app_sqrt_bounded_justification=by applying the square root function
axiom_app_sqrt_diagnostic=square root
axiom_app_sqrt_justification=by applying the square root function
axiom_app_square_bounded_diagnostic=square
axiom_app_square_bounded_justification=by squaring
axiom_app_square_diagnostic=square
axiom_app_square_justification=by squaring
axiom_apply_forall_diagnostic=mapping
axiom_apply_forall_justification=by applying to {0}
axiom_apply_fun_lr_diagnostic=functional mapping
axiom_apply_fun_lr_justification=by mapping left and right sides of {0}
axiom_apply_ineq_inverse_diagnostic=multiplicative inverse
axiom_apply_ineq_inverse_justification=by decrease of multplicative inverse on ℝ*
axiom_apply_ineq_sqrt_diagnostic=square root
axiom_apply_ineq_sqrt_justification=by applying the square root function
axiom_apply_ineq_square_diagnostic=square
axiom_apply_ineq_square_justification=by squaring
axiom_arith_def_diagnostic=definition
axiom_arith_def_justification=by definition of an arithmetic progression
axiom_arith_pro_diagnostic=functional expression
axiom_arith_pro_justification=by functional expression of an arithmetic progression
axiom_ax_bad_diagnostic=lies of swindlecants
axiom_ax_bad_justification=by lies telling of swindlecants
axiom_ax_good_diagnostic=truth of honestants
axiom_ax_good_justification=by truth telling of honestcants
axiom_back_elim_equiv_diagnostic=definition
axiom_back_elim_equiv_justification=by definition of equivalence
axiom_bound_conj_diagnostic=double inequality
axiom_bound_conj_justification=by definition of double inequality
axiom_bound_to_eq_diagnostic=double inequality
axiom_bound_to_eq_justification=by definition of double inequality
axiom_bounded_elim_diagnostic=double inequality
axiom_bounded_elim_justification=by definition
axiom_case_base_binary_diagnostic=excluded middle
axiom_case_base_binary_justification=by principle of excluded middle
axiom_case_base_diagnostic=by disjunction of case
axiom_case_base_justification=by case base reasoning
axiom_case_good_or_bad_diagnostic=honestants or swindlecants
axiom_case_good_or_bad_justification=by disjonction of honestants and swindlecants
axiom_comb_comp_lt_diagnostic=composition
axiom_comb_comp_lt_justification=by composition of inclusions
axiom_combadd_diagnostic=addition
axiom_combadd_justification=by addition
axiom_combine_cmp_minus_diagnostic=subtraction
axiom_combine_cmp_minus_justification=by subtraction of inequalities
axiom_combine_cmp_plus_diagnostic=addition
axiom_combine_cmp_plus_justification=by addition of inequalities
axiom_combsub_diagnostic=subtraction
axiom_combsub_justification=by subtraction
axiom_commutativity_diagnostic=commutativity
axiom_commutativity_justification=by commutativity
axiom_conj_diagnostic=conjunction
axiom_conj_justification=by conjunction
axiom_deduce_not_color_diagnostic=binary color
axiom_deduce_not_color_justification=by binarity of colors
axiom_def_fbij_diagnostic=bijection
axiom_def_fbij_justification=by definition of a bijection
axiom_def_fcomp_diagnostic=composition of functions
axiom_def_fcomp_justification=by definition of function composition
axiom_def_finj_diagnostic=injection
axiom_def_finj_justification=by definition of an injection
axiom_def_finvol_diagnostic=involution
axiom_def_finvol_justification=by definition of an involution
axiom_def_fsurj_diagnostic=surjection
axiom_def_fsurj_justification=by definition of a surjection
axiom_def_rantisym_diagnostic=antisymmetric relation
axiom_def_rantisym_justification=by definition of an anti-symmetric relation
axiom_def_rcomp_diagnostic=composition of relations
axiom_def_rcomp_justification=by definition of composition of relations
axiom_def_rfun_diagnostic=functional relation
axiom_def_rfun_justification=by definition of a functional relation
axiom_def_rident_diagnostic=identity relation
axiom_def_rident_justification=by definition of the identity relation
axiom_def_rinj_diagnostic=injective relation
axiom_def_rinj_justification=by definition of an injective relation
axiom_def_rinv_diagnostic=inverse relation
axiom_def_rinv_justification=by definition of an inverse relation
axiom_def_rrefl_diagnostic=reflexive relation
axiom_def_rrefl_justification=by definition of a reflexive relation
axiom_def_rsurj_diagnostic=surjective relation
axiom_def_rsurj_justification=by definition of a surjective relation
axiom_def_rsym_diagnostic=symmetric relation
axiom_def_rsym_justification=by definition of a symmetric relation
axiom_def_rtotleft_diagnostic=left-total relation
axiom_def_rtotleft_justification=by definition of a left-total relation
axiom_def_rtrans_diagnostic=transitive relation
axiom_def_rtrans_justification=by definition of a transitive relation
axiom_elim_comp_diagnostic=inequality
axiom_elim_comp_justification=by definition of inequality
axiom_elim_conj_left_diagnostic=left deduction
axiom_elim_conj_left_justification=by left deduction
axiom_elim_conj_right_diagnostic=right deduction
axiom_elim_conj_right_justification=by right deduction
axiom_elim_eqfun_diagnostic=functional equality
axiom_elim_eqfun_justification=by definition of function equality
axiom_elim_eqset_diagnostic=set equality
axiom_elim_eqset_justification=by definition of set equality
axiom_elim_even_def_diagnostic=parity
axiom_elim_even_def_justification=by definition of parity
axiom_elim_false_exset_diagnostic=empty set
axiom_elim_false_exset_justification=by definition of the empty set
axiom_elim_gen_app_rel_diagnostic=relational membership
axiom_elim_gen_app_rel_justification=by relational membership
axiom_elim_has_finite_limit_decr_diagnostic=decreasing convergence
axiom_elim_has_finite_limit_decr_justification=by decreasing and reducing
axiom_elim_has_finite_limit_incr_diagnostic=increasing convergence
axiom_elim_has_finite_limit_incr_justification=by increasing et growing
axiom_elim_is_elem_universe_diagnostic=universe
axiom_elim_is_elem_universe_justification=by definition of the universe
axiom_elim_multiple_diagnostic=definition
axiom_elim_multiple_justification=by definition of divisibility
axiom_elim_negation_diagnostic=by definition
axiom_elim_negation_justification=by definition of negation
axiom_elim_pprod_diagnostic=cartesian product
axiom_elim_pprod_justification=by definition of cartesian product
axiom_elim_requiv_diagnostic=equivalence relation
axiom_elim_requiv_justification=by definition of an equivalence relation
axiom_elim_scomp_diagnostic=complement
axiom_elim_scomp_justification=by definition of the complement of a set
axiom_elim_sdiff_diagnostic=difference
axiom_elim_sdiff_justification=by definition of set difference
axiom_elim_sequiv_diagnostic=equivalence class
axiom_elim_sequiv_justification=by definition of an equivalence class
axiom_elim_set_lteq_diagnostic=set inclusion
axiom_elim_set_lteq_justification=by definition of set inclusion
axiom_elim_shas_lower_bound_diagnostic=lower bound
axiom_elim_shas_lower_bound_justification=by definition
axiom_elim_shas_upper_bound_diagnostic=upper bound
axiom_elim_shas_upper_bound_justification=by definition
axiom_elim_sinter_diagnostic=intersection
axiom_elim_sinter_justification=by definition of set intersection
axiom_elim_sis_decreasing_diagnostic=decrease
axiom_elim_sis_decreasing_justification=by definition
axiom_elim_sis_gt_zero_diagnostic=positive series
axiom_elim_sis_gt_zero_justification=by definition
axiom_elim_sis_increasing_diagnostic=increase
axiom_elim_sis_increasing_justification=by definition
axiom_elim_sis_lt_zero_diagnostic=suites négative
axiom_elim_sis_lt_zero_justification=by definition
axiom_elim_subset_diagnostic=power set
axiom_elim_subset_justification=by definition of power set
axiom_elim_sunion_diagnostic=set union
axiom_elim_sunion_justification=by definition of set union
axiom_elim_true_at_rank_diagnostic=definition of P
axiom_elim_true_at_rank_justification=by definition of {0}
axiom_eq_inverse_diagnostic=reverse
axiom_eq_inverse_justification=by changing to the reverse
axiom_eq_reverse_diagnostic=opposite
axiom_eq_reverse_justification=by taking the opposite
axiom_eq_symmetry_diagnostic=symmetry
axiom_eq_symmetry_justification=by symmetry of the equality relation
axiom_eq_trans_diagnostic=transitivity
axiom_eq_trans_justification=by transitivity of the equality relation
axiom_equiv_rtrans_diagnostic=inclusion-based formulation
axiom_equiv_rtrans_justification=by inclusion-based formulation of a transitive relation
axiom_ex_elim_diagnostic=by extraction
axiom_ex_elim_justification=by extraction of witness
axiom_ex_intro_diagnostic=by construction
axiom_ex_intro_justification=by construction
axiom_expand_diagnostic=expansion
axiom_expand_justification=by expanding
axiom_factorize_diagnostic=remarkable factorisation
axiom_factorize_justification=by factorising by {1}
axiom_falseall_diagnostic=ex falso quodlibet
axiom_falseall_justification=by deducing a contradiction
axiom_gen_factorize_diagnostic=factorisation
axiom_gen_factorize_justification=by factorising {0} by {1}
axiom_geo_def_diagnostic=definition
axiom_geo_def_justification=by definition of a geometric progression
axiom_geo_pro_diagnostic=functional expression
axiom_geo_pro_justification=by functional expression of a geometric progression
axiom_inclusionsimpl_diagnostic=simplify
axiom_inclusionsimpl_justification=by rewriting {1} as {0}
axiom_ind_basic_forall_diagnostic=induction
axiom_ind_basic_forall_justification=by induction
axiom_ind_init_diagnostic=induction from
axiom_ind_init_justification=by induction
axiom_ineq_sym_rew_diagnostic=symmetry
axiom_ineq_sym_rew_justification=by symmetrical rewriting
axiom_intro_false_diagnostic=non-contradiction
axiom_intro_false_justification=by the principle of non-contradiction
axiom_intro_or_left_diagnostic=par justification à gauche
axiom_intro_or_left_justification=par justification à gauche
axiom_intro_or_right_diagnostic=par justification à droite
axiom_intro_or_right_justification=par justification à droite
axiom_intro_sqrt_square_diagnostic=square root
axiom_intro_sqrt_square_justification=by simplifying the square root
axiom_limit_finite_diagnostic=finite limit
axiom_limit_finite_justification=by calculating a finite limit
axiom_limit_inf_diagnostic=+∞ limit
axiom_limit_inf_justification=by calculating the limit at + ∞
axiom_limit_neg_inf_diagnostic=-∞ limit
axiom_limit_neg_inf_justification=by calculating the limit at -∞
axiom_linearsimpl_diagnostic=simplification
axiom_linearsimpl_justification=by simplifying {0}
axiom_local_theo_justification=by local theorem {0}
axiom_lradd_bounded_diagnostic=addition
axiom_lradd_bounded_justification=by adding to left and right sides of {0}
axiom_lradd_diagnostic=addition
axiom_lradd_ineq_diagnostic=addition
axiom_lradd_ineq_justification=by adding to left and right sides of {0}
axiom_lradd_justification=by adding {0} to both sides
axiom_lradd_neq_diagnostic=addition
axiom_lradd_neq_justification=by adding to left and right sides of {0}
axiom_lrdiv_bounded_diagnostic=division
axiom_lrdiv_bounded_justification=by dividing left and right sides by {0}
axiom_lrdiv_diagnostic=division
axiom_lrdiv_ineq_diagnostic=division
axiom_lrdiv_ineq_justification=by dividing left and right sides by {0}
axiom_lrdiv_justification=by dividing both sides by {0}
axiom_lrdiv_neq_diagnostic=division
axiom_lrdiv_neq_justification=by dividing left and right sides of {0}
axiom_lrmul_bounded_diagnostic=multiplication
axiom_lrmul_bounded_justification=by multiplying left and right sides by {0}
axiom_lrmul_diagnostic=multiplication
axiom_lrmul_ineq_diagnostic=multiplication
axiom_lrmul_ineq_justification=by multiplying left and right sides by {0}
axiom_lrmul_justification=by multiplying both sides by {0}
axiom_lrmul_neq_diagnostic=multiplication
axiom_lrmul_neq_justification=by multiplying left and right sides by {0}
axiom_lrsub_bounded_diagnostic=subtraction
axiom_lrsub_bounded_justification=by subtracting left and right sides of {0}
axiom_lrsub_diagnostic=subtraction
axiom_lrsub_ineq_diagnostic=subtraction
axiom_lrsub_ineq_justification=by subtracting left and right sides of {0}
axiom_lrsub_justification=by subtracting {0} from both sides
axiom_lrsub_neq_diagnostic=subtraction
axiom_lrsub_neq_justification=by subtracting left and right sides of {0}
axiom_lt_next_int_diagnostic=next integer
axiom_lt_next_int_justification=by transition to the next integer
axiom_modus_ponens_diagnostic=modus ponens
axiom_modus_ponens_justification=by applying modus ponens
axiom_muldiv_diagnostic=multiplication and division
axiom_muldiv_justification=by multiplying and dividing by {1}
axiom_neq_symmetry_diagnostic=symétrie
axiom_neq_symmetry_justification=par symétrie de la relation d'inégalité
axiom_non_zero_gt_diagnostic=strictly greater than
axiom_non_zero_gt_justification=par supériorité stricte
axiom_non_zero_lt_diagnostic=strictly less than
axiom_non_zero_lt_justification=par infériorité stricte
axiom_polysquare_diagnostic=remarkable formulas
axiom_polysquare_justification=by identifying the perfect square {0}
axiom_proddecompl_diagnostic=decomposition
axiom_proddecompl_justification=by product decomposition
axiom_proddef_diagnostic=assocication
axiom_proddef_justification=by associativity of the product operator applied to {0}
axiom_prodinverse_diagnostic=reverse indexing
axiom_prodinverse_justification=by reverse indexing
axiom_prodlinear_diagnostic=associativity
axiom_prodlinear_justification=by associativity of the product operator applied to {0}
axiom_prodresult1_diagnostic=prodresult1
axiom_prodresult1_justification=prodresuult1
axiom_prodsimpl_diagnostic=prodsimpl
axiom_prodsimpl_justification=prodsimpl
axiom_produpshift_diagnostic=index shifting
axiom_produpshift_justification=by index shifting
axiom_reason_capacity_diagnostic=ability to reason
axiom_reason_capacity_justification=by hat wearer's ability to reason
axiom_red_true_at_rank_diagnostic=by definition
axiom_red_true_at_rank_justification=by definition of {0}
axiom_reducedenom_diagnostic=common denominator
axiom_reducedenom_justification=by reduction to a common denominator
axiom_rewriting_diagnostic=rewriting
axiom_rewriting_justification=by rewriting {0} as {1}
axiom_sandwich_diagnostic=sandwich
axiom_sandwich_justification=by the sandwich theorem
axiom_section_diagnostic=in a range
axiom_section_justification=demonstration
axiom_set_absorb_diagnostic=absorbtion
axiom_set_absorb_justification=by absorption
axiom_set_adabsurdum_diagnostic=ad absurdum
axiom_set_adabsurdum_justification=by involution of set complement
axiom_set_demorgan_diagnostic=De Morgan's laws
axiom_set_demorgan_justification=according to the laws of De Morgan
axiom_set_eq_symmetry_diagnostic=symmetry
axiom_set_eq_symmetry_justification=by symmetry of the equality relation
axiom_set_eq_trans_diagnostic=transitivity
axiom_set_eq_trans_justification=by transitivity of the equality relation
axiom_set_excluded_diagnostic=excluded middle
axiom_set_excluded_justification=by applying the excluded middle principle
axiom_set_inter_comb_diagnostic=intersection
axiom_set_inter_comb_justification=by intersection left and right
axiom_set_lteq_transitivity_diagnostic=transitivity
axiom_set_lteq_transitivity_justification=by transitivity of inclusion
axiom_set_neutral_diagnostic=identity element
axiom_set_neutral_justification=by property of the identity element
axiom_set_rewriting_diagnostic=rewriting
axiom_set_rewriting_justification=by rewriting {0} in {1}
axiom_set_union_comb_diagnostic=union
axiom_set_union_comb_justification=by union left and right
axiom_setassociative_diagnostic=associativity
axiom_setassociative_justification=by associativity
axiom_setcommutative_diagnostic=commutativity
axiom_setcommutative_justification=by commutativity
axiom_setdevelopp_diagnostic=expansion
axiom_setdevelopp_justification=by developping
axiom_setfactorize_diagnostic=factorisation
axiom_setfactorize_justification=by factorising
axiom_sigmadecompl_diagnostic=decomposition
axiom_sigmadecompl_justification=by decomposing sigma
axiom_sigmadef_diagnostic=definition
axiom_sigmadef_justification=by definition of the sigma function applied to {0}
axiom_sigmainverse_diagnostic=reverse
axiom_sigmainverse_justification=by reverse indexing
axiom_sigmalinear_diagnostic=linearity
axiom_sigmalinear_justification=by linearity of the sigma function applied to {0}
axiom_sigmaresult1_diagnostic=first integers
axiom_sigmaresult1_justification=by sum of the first integers
axiom_sigmaresult2_diagnostic=first squares
axiom_sigmaresult2_justification=by the sum of the first square roots
axiom_sigmaresult3_diagnostic=first powers
axiom_sigmaresult3_justification=by sum of the first powers
axiom_sigmasimpl_diagnostic=count
axiom_sigmasimpl_justification=by definition of the sigma function
axiom_sigmaupshift_diagnostic=index shifting
axiom_sigmaupshift_justification=by the difference of the indices
axiom_slim_def_elim_diagnostic=limit
axiom_slim_def_elim_justification=by definition of limit
axiom_slim_inf_def_elim_diagnostic=infinite limit
axiom_slim_inf_def_elim_justification=by definition of an infinite limit
axiom_slimfinite_inf_elim_diagnostic=infinite limit
axiom_slimfinite_inf_elim_justification=
axiom_square_diff_diagnostic=remarkable formula
axiom_square_diff_justification=by factorising the difference of two squares
axiom_subadd_diagnostic=subtraction and addition
axiom_subadd_justification=by subtracting and adding {1} to {0}
axiom_trans_lt_gt_diagnostic=transitivity
axiom_trans_lt_gt_justification=by transitivity
axiom_updownsimpl_diagnostic=simplification up and down
axiom_updownsimpl_justification=by simplification up and down
axiom_varchange_diagnostic=change of variables
axiom_varchange_justification=by rewriting {0} in {1}
basic_A=A
basic_BeMarried=to be married
basic_BeMarried_neg=to not be married
basic_BeScottish=to be Scottish
basic_BeScottish_neg=to not be Scottish
basic_BlackHat=black
basic_ExprGT={0} > {1}
basic_ExprGTEQ={0} ≥ {1}
basic_ExprLT={0} < {1}
basic_ExprLTEQ={0} ≤ {1}
basic_FBij={0} is a bijection
basic_FComp={0} ∘ {1}
basic_FFInj={1} is an injection on [ 0 ... {0} ]
basic_FFMono={1} is strictly monotonic on [ 0 ... {0} ]
basic_FInj={0} is an injection
basic_FInj_neg={0} is not an injection
basic_FInvolution={0} is an involution
basic_FSurj={0} is a surjection
basic_FSurj_neg={0} is not a surjection
basic_False=contradiction
basic_False_sci=false
basic_FindX=Find the value of x.
basic_FindY=Find the value of y.
basic_GoOutSundays=to go out on Sundays
basic_GoOutSundays_neg=to not go out on Sundays
basic_GoToMatch=to go to a football match tomorrow
basic_GoToMatch_neg=to not go to the match tomorrow
basic_GoToTraining=to go to training today
basic_GoToTraining_neg=to not go to training today
basic_O1FInj={0} is an injection
basic_O1FInj_neg={0} is not an injection
basic_O1FSurj={0} is a surjection
basic_O1FSurj_neg={0} is not a surjection
basic_OldYoungUtterance=Who is the oldest and who is the youngest?
basic_Oldest={0} is the oldest
basic_Oldest_neg={0} is not the oldest
basic_PropDependentN=proposition depending on n
basic_RAntiSym={2} is an antisymmetric relation
basic_RComp={6} . {7}
basic_REquiv={2} is an equivalence relation
basic_RFun={4} is a functional relation
basic_RIRRefl={2} is an irreflexive relation
basic_RInj={4} is an injective relation
basic_RInv={4} ⁻¹
basic_RRefl={2} is a relflexive relation
basic_RSurj={4} is a surjective relation
basic_RSym={2} is a symmetric relation
basic_RTot={4} is a total relation
basic_RTotLeft={4} is a left-total relation
basic_RTrans={2} is a transitive relation
basic_ScottishUtterance=Rules are so strict that no one can be accepted in the club.
basic_Set=ensemble
basic_ToBeHuman=to be human
basic_ToBeHuman_neg=is not human
basic_ToBeMortal=to be mortal
basic_ToBeMortal_neg=is not mortal
basic_ToBeSocrate=to be Socrates
basic_ToBeSocrate_neg=is not Socrate
basic_WearAKilt=to wear a kilt
basic_WearAKilt_neg=does not wear a kilt
basic_WearRedSocks=to wear red socks
basic_WearRedSocks_neg=does not wear red socks
basic_WhiteHat=white
basic_Youngest={0} is the youngest
basic_Youngest_neg={0} is not the youngest
basic_addition=by adding {0}
basic_and=and
basic_and_sci=∧
basic_app_fun_exset={2} ( {3} )
basic_app_prop={1} ( {2} )
basic_app_prop2={1} ( {2} , {3} )
basic_app_prop2_sci={1} ( {2} , {3} )
basic_app_prop_sci={1} ( {2} )
basic_app_rel={1} {0} {2}
basic_app_rel_sci={1} {0} {2}
basic_are_collinear={0} are collinear
basic_are_collinear_neg={0} are not collinear
basic_are_parallel={0} and {1} are parallel
basic_are_parallel_neg={0} and {1} are not parallel
basic_arith_elim=by definition of an arithmetic sequence
basic_case=case {0} : {1}
basic_demonstrate_lim=Prove that {0} has a limit of {1}
basic_determine=Determine {0}
basic_determine_lim=Determine the limit of {0}
basic_determine_reason=Determine the common difference of the series {0}
basic_determine_value=Determine the value of {0}
basic_development=by expansion
basic_division=dividing by {0}
basic_division_and_multiplication=dividing and multiplying by {0}
basic_elim_is_solution_equiv=by definition
basic_elim_limit_expr_b=by definition of a left or right limit
basic_elim_rewrite_equiv=by rewriting
basic_eq_symmetry_equiv=by symmetry of the equality relation
basic_equation=the equation {1}
basic_equation_systeq=the equation system {1}
basic_equiv={0} {math:⇔} {1}
basic_equiv1={0} {math:⇔} {1}
basic_equiv1_sci={0} {math: ⇔} {1}
basic_equiv_sci={0} {math:⇔} {1}
basic_expansion=by expanding
basic_expansion_of_power=by definition of powers
basic_expr_is_defined_on={1} is defined on {2}
basic_expr_is_defined_on_neg={0} is not defined on {1}
basic_factorization=by factorising
basic_findLimitExpr=determine the limit value {1} such that {2}
basic_find_asymptot={find} the asymptotic behavior of {2} at {3}
basic_find_expr={find} the value of {0} {justTags}
basic_find_limit={find} the limit of {2} as x approaches {3} {justTags}
basic_find_limit_type={find} the behavior of {4} at infinity
basic_find_series_type={find} the type of series {0}
basic_floor_id=Floor
basic_fun_has_finite_limit={4} is convergent
basic_fun_has_lower_bound={4} is bounded below
basic_fun_has_upper_bound={4} is bounded above
basic_fun_is_bounded={4} is limited
basic_fun_is_constant={4} is constant
basic_fun_is_decreasing={4} is decreasing
basic_fun_is_decreasing_neg={4} is not decreasing
basic_fun_is_defined_on={4} is defined on {5}
basic_fun_is_gt_zero={4} is strictly positive
basic_fun_is_increasing={4} is increasing
basic_fun_is_increasing_neg={4} is not increasing
basic_fun_is_lt_zero={4} is negative
basic_gen_app_rel={5} {4} {6}
basic_gen_app_rel_sci={5} {4} {6}
basic_geoconstr=by construction of {0}
basic_id={0}
basic_imply=implies
basic_imply_sci={math:⇒}
basic_ind_basic_evar_0=Rank of initialisation
basic_is_a_neighborhood={1} is a neighborhood of {2}
basic_is_add_increasing=Addition is increasing for relation '{0}'
basic_is_aware={0} knows that {1}
basic_is_aware_neg={0} does not know that {1}
basic_is_bad={0} is a swindlecant
basic_is_big_enough={0} is big
basic_is_crossed=the quadrilateral {0} is intersected
basic_is_crossed_neg=quadrilateral {0} is not crossed
basic_is_defined_on={0} is defined on {1}
basic_is_definition_set={0} is the set of definitions of {1}
basic_is_element={1} {math:∊} {2}
basic_is_element_dom={0} {math:∊} {1}
basic_is_element_neg={1} does not belong to {2}
basic_is_element_sci={1} {math:∊} {2}
basic_is_element_sci_neg={1} {math:∉} {2}
basic_is_even={0} is even
basic_is_good={0} is an honestant
basic_is_in_neighbourhood_of={0} is in the neighborhood of {1}
basic_is_integer={0} is an integer
basic_is_lci={0} is a binary operation on {1}
basic_is_lci_neg={0} is not a binary operation on {1}
basic_is_middle_segment={0} is the midpoint of the segment {1}
basic_is_middle_segment_neg={0} is not the midpoint of the segment {1}
basic_is_monotonic_on={1} is decreasing on {2}
basic_is_multiple_of={0} is divisible by {1}
basic_is_multiple_of_neg={0} is not divisible by {1}
basic_is_odd={0} is odd
basic_is_parallelogram={0} is a parallelogram
basic_is_parallelogram_neg={0} is not a parallelogram
basic_is_partition={1} is a partition of {0}
basic_is_polynom={1} is a polynomial
basic_is_projected_on={0} is the orthogonal projection of {1} on {2}
basic_is_reflexive=Relation '{0}' is reflexive
basic_is_restriction={5} is the restriction of {6} to {2}
basic_is_solution={0} is the set of solutions of {1}
basic_is_solution_neg={0} is not the solution of {1}
basic_is_symmetric={0} is the symmetric of {2} with respect to {1}
basic_is_transitive=Relation '{0}' is transitive
basic_isolate=Isolate {0}
basic_knows_hatcolor={0} knows the colour of their hat
basic_knows_hatcolor_neg={0} does not know the colour of their hat
basic_le=≤
basic_lor_elim=sufficient hypothesis
basic_multiplication_and_division=by multiplying and dividing by {0}
basic_nats={0} with {1}
basic_neighborset={1}
basic_not=not
basic_not_sci=¬
basic_oldyoung=oldest and youngest
basic_or=or
basic_or_sci=∨
basic_pis_element={2} belongs to {3}
basic_pis_element_neg={1} does not belong to {2}
basic_pis_element_sci={2} {math:∊} {3}
basic_pis_element_sci_neg={1} {math:∉} {2}
basic_proddecompr=by decomposition
basic_proddownshift=by index shifting
basic_pset3={0} {1} and {2}
basic_rel_is_defined_on={0} is defined on {1}
basic_rel_is_defined_on_neg={0} is not defined on {1}
basic_rel_le=≤
basic_resolve=Resolve {0}
basic_rewrite_in={1} is rewritten {2} in {0}
basic_ror_elim=Sufficient hypothesis
basic_say={0} says that {1}
basic_set_lt={0} ⊂ {1}
basic_set_lteq={1} ⊆ {2}
basic_shas_finite_limit={0} is convergent
basic_shas_limit={0} has a limit of {1}
basic_shas_limit_neg={0} does not have a limit of {1}
basic_sigmadecompr=by decomposing sigma
basic_sigmadownshift=by the difference of the indices
basic_sis_arith={0} is arithmetic
basic_sis_arith_neg={0} is not arithmetic
basic_sis_arith_reason={2} is arithmetic for reason {3}
basic_sis_arith_reason_neg={2} is not arithmetic because of {3}
basic_sis_caracterized=Is the series {0} arithmetic or geometric?
basic_sis_element={0} {math:∊} {1}
basic_sis_element_neg={0} {math:∉} {1}
basic_sis_element_sci={0} {math:∊} {1}
basic_sis_element_sci_neg={0} {math:∉} {0}
basic_sis_geo={0} is a geometric series
basic_sis_geo_neg={0} is not a geometric series
basic_sis_geo_reason={2} is geometric with common ratio {3}
basic_sis_geo_reason_neg={2} is not a geometric series because with common ratio {3}
basic_subtraction=by subtracting {0}
basic_subtraction_and_addition=by subtracting or adding {0}
basic_triv_div_lr=by dividing the two members by {0}
basic_true_at_rank={0} is true at rank {1}
basic_true_at_rank_neg={0} is false on rank {1}
basic_true_at_rank_sci={0} ( {1} )
basic_true_at_rank_sci_neg=¬ {0} ( {1} )
basic_uprod={0}×{1}
basic_wears_hat={0} wears a hat {1}
basic_wears_hat_neg={0} does not wear a {1} hat
help_part_content=Content
help_part_paper=Digital paper
help_section_browsing=Navigation
help_section_commutativity=Commutativity
help_section_evar=Reasoning variable
help_section_exercises=Exercises
help_section_proof=Proof
help_section_selection=Selection
help_section_trophy=Cockades
help_section_unification=Unifications
key_Product=Product
key_access_content=Content
key_access_date=Date
key_access_role=Role
key_access_role_ref=Admin
key_access_role_user=Student
key_account=My account
key_add=Add
key_add_exercise_message=Type exercise utterance ...
key_add_exercise_title=Request new exercise
key_and=and
key_apply=Apply
key_ask_hint_button=Hint
key_assume=Assume
key_back_connection_panel=To get back to previous screen,
key_browsing_train=Exercises
key_by=according to {0}
key_cancel=Cancel
key_catchme=Catch me
key_change_password=Change password
key_chapters=Chapters
key_character_not_available=character not available
key_check_box=Check box
key_check_cgu=GTU
key_check_text_cgu=Accept
key_class=Class
key_class_default_message=No class found.
key_click_here=click here
key_clickme=Click here
key_clickme_fix=Fix it and click here to validate
key_clickme_valid=Click here to validate
key_commuteme=Obtain below the following value:
key_conclusion=Conclusion
key_confirm_delete_tab_message=Delete scope ?
key_confirm_delete_tab_message_yes=Yes
key_confirm_password=Confirm password
key_confirm_quit_exercise=Give up exercise?
key_congrats=Well done, the exercise is proved!
key_connection=Connection
key_construct=Construct
key_context=Context
key_create_account=Create account
key_create_account_connect=Create account / login
key_credits=tokens
key_credits_content_message=Buy application content directly.
key_credits_content_title=Content
key_credits_pack_message=Unlock content in the application with tokens.
key_credits_pack_pack1_title=Discovery
key_credits_pack_pack2_title=Training
key_credits_pack_pack3_title=Ultimate
key_credits_pack_title=Credits
key_deduce=Deduce
key_deduce_in=Deduce in
key_deduce_of=Deduction from
key_deduce_scope=Deduce in this scope
key_delete=Delete
key_delete_account=Delete account
key_delete_account_message=A deletion link has been sent to your email address
key_delete_message=To delete the account, type 'DELETE' in the text field below and click the OK button.
key_delete_word=DELETE
key_deleted_account={0} account has been deleted.
key_demonstrate=Prove:
key_description_back=<div>Justify statement <!--{type="tag" input="{statementId}"}--> with the rule : <!--{type="axiom_api" input="{axiomId}"}--></div>
key_description_backsel=<div>Justify statement <!--{type="tag" input="{statementId}"}--> with the rule : <!--{type="axiom_api" input="{axiomId}"}--></div>
key_description_delete=<div>Delete statement <!--{type="tag" input="{statementId}"}--></div>
key_description_deleteby=<div>Delete justification of statement <!--{type="tag" input="{statementId}"}--></div>
key_description_for=<div>Deduce from <!--{type="tag" input="{statementId}"}--> with <!--{type="axiom_api" input="{axiomId}"}--></div>
key_description_forsel=<div>Deduce from <!--{type="tag" input="{statementId}"}--> with <!--{type="axiom_api" input="{axiomId}"}--></div>
key_description_inst=Assign value <!--{type="expr" input="{actTypArg2}"}--> to <!--{type="paper_evar" input="{actTypArg}"}--></div>
key_description_section=Open scope for statement <!--{type="tag" input="{statementId}"}-->
key_description_success=<div>Congrats, exercise solved!</div>
key_description_unif=Unify statements <!--{type="tag" input="{actTypArg}"}--> and <!--{type="tag" input="{statementId}"}-->
key_diagnostic_no_diag=The entries in this chapter are not yet available.
key_disconnect=Disconnect
key_draggable_title=Move titles
key_dragme=Drag here
key_email=Email
key_email_not_authorized=email not authorized
key_email_not_found=email not found
key_email_not_valid=email not valid
key_email_not_verif=email not verified
key_email_unknown=email unknown
key_email_used=email used
key_email_valid=email valid
key_empty_field=empty field
key_empty_suggest=Nothing available for this action
key_error_paper_subtitle=Not found
key_error_paper_title=cannot retrieve this paper
key_exercise=Exercise
key_exercises=Exercises
key_fill_evar=Value of
key_find=Find
key_firstname=Firstname
key_focus_text=Context
key_follow_us=News
key_forbid_mobile=The application is not available on mobile
key_forgot_password=Forgot password ?
key_geo_figure=Geometrical figure
key_get_credits=Get credits
key_goal=Goal
key_got_it=Got it.
key_graph=Graph
key_group_popup_button=Add
key_group_popup_input_default=access code
key_group_popup_title=Enter access code
key_help=Help
key_help_tooltip_chapter_icon_all=Indique la résolution ou non de tous les exercices du chapitre.
key_help_tooltip_chapter_icon_diag=Indique la résolution ou non de tous les exercices de type incontournable sur le chapitre.
key_help_tooltip_chapter_icon_tuto=Indique la résolution ou non de tous les exercices du didacticiel.
key_help_tooltip_chapter_icon_unavoidable=Indique la résolution ou non de tous les exercices de type incontournable sur le chapitre.
key_help_tooltip_clearall=clear all
key_help_tooltip_deduce=deduction diagnosis
key_help_tooltip_exercise_icon_diag=Exercice débloquant le mode diagnostic
key_help_tooltip_exercise_icon_difficulty_easy=Exercice de difficulté facile
key_help_tooltip_exercise_icon_difficulty_hard=Exercice de difficulté moyenne
key_help_tooltip_exercise_icon_difficulty_medium=Exercice de difficulté difficile
key_help_tooltip_exercise_icon_hint=Exercice prenant en charge des indications ou non.
key_help_tooltip_exercise_icon_unavoidable=Exercice de type incontournable ou non
key_help_tooltip_hint=hint
key_help_tooltip_justify=justification diagnosis
key_help_tooltip_lock_access_no=Not available
key_help_tooltip_lock_access_without_deadline=accessible
key_help_tooltip_print=print
key_help_tooltip_redo=redo
key_help_tooltip_section=Creation of scope
key_help_tooltip_undo=undo
key_help_tooltip_unify=unification
key_highlight_icon_backward=backward
key_highlight_icon_definition=definition
key_highlight_icon_forward=forward
key_highlight_icon_reduce=reduce
key_hint_message=Click the button below to display a hint
key_hintpopup_action=Action
key_hintpopup_actions=Actions
key_hintpopup_description=Description
key_hintpopup_preview=Preview
key_hintpopup_tab_desc=Description
key_hintpopup_tab_hint=Hint
key_home_credits_text=Number of tokens
key_home_dashboard_badges=Cockades
key_home_dashboard_exercises=Solved exercises
key_home_profile_text=Welcome, {firstname}
key_ice=An internal error occurred. Please reload.
key_id_connection=Connection
key_if=if
key_img_text_1=Mettre à jour
key_img_text_2=ma photo de profil
key_inputme=Enter the following value:
key_justify=Justify
key_justify_of=Justification of
key_language=Language
key_lastname=Lastname
key_legend=Legend:
key_levels=Levels
key_loading_message=Loading, please wait ...
key_local_theorem=Local theorem
key_login_with=Log in with:
key_main_scope=main scope
key_membership_alreadyadd=already added
key_membership_error=Error
key_membership_notfound=unknown code
key_membership_overused=quota reached
key_modify=Modify
key_nats={0} with {1}
key_need_help=Need help ?
key_new_exercise=New exercise
key_next=Next
key_no_email_message=email hidden, cannot log in.
key_not_yet_register=If you're not registered yet,
key_ok=OK
key_or=or
key_password=Password
key_password_confirmed=password confirmed
key_password_current=Current password
key_password_incorrect=password incorrect
key_password_new=New password
key_password_not_confirmed=password not confirmed
key_password_too_short=password is too short (at least 6 characters)
key_password_valid=password valid
key_password_with_digit=password must contained at least 1 digit
key_premises=Premises
key_preview=Preview
key_preview_deduce=Preview of deduction of
key_preview_justify=Preview of justification of
key_profile_informations=Profile information
key_proof_of=Proof of
key_propdeftag_def=the definition
key_propdeftag_prop=proposition
key_prove_text=Proof
key_prove_text_close=Proof ...
key_prove_text_open=Proof:
key_register=Register
key_registration=Registration
key_reinit=Reset
key_reinit_password=Enter your email address to reset your password.
key_reinit_password_message=A reset link has been sent to your email address.
key_report_input_default=Give feedback or ask for help
key_report_label=Send us a message
key_report_label_email=Your email address:
key_report_message_sent=Message sent !
key_report_modify_message=Edit message
key_report_next=Next
key_report_placeholder_email=Email address
key_report_recontact=We will get back to you.
key_report_send=Send
key_require_message=To access this chapter, get the cockade 'tutorial' of chapters below:
key_require_message_exercise=To access this exercise, get the cockade 'tutorial' of chapters below:
key_require_message_part=Get 'tutorial' cockades for access to chapters below
key_required=Prerequisites
key_save=Save
key_scroll_down=Scroll down
key_scroll_up=Scroll up
key_segments=Segments
key_selectme=Select the value above
key_send=Send
key_social_login=<div class="{0}"> <a target="_blank" href="http://en.wikipedia.org/wiki/Social_login" class="{1}">social login</a> is the easiest and safest way to sign-in and login. Nothing will be published on your "wall". </div> <div class="{2}">By clicking on one of the buttons, you are accepting <a target="_blank" href="{3}" class="{4}">our conditions of use and our confidentiality policy</a>. </div>
key_sorry_whitelist=The application is not available. If you with to sign up, please send an email to: contact@edukera.com
key_start=Start
key_status_report=Report a problem
key_step_choice_axiom=<div class="instruction-item"><!--{type="hint_itemize"}--> In part <span class="hint-text"> <!--{type="label_toolbox" input="{TPartId}"}--></span> <!--{type="toolbox_button" input="{TPartId}"}--> access toolbox chapter by clicking on <!--{type="label_toolbox" input="{TChapterId}"}--> <!--{type="toolbox_button" input="{TChapterId}"}--> <!--{type="hint_check"}--></div>
key_step_choice_axiom_in_diag=<div class="instruction-item"> <!--{type="hint_itemize"}--> Select rule <!--{type="diag_axiom" input="{axiomId}"}--> in section <!--{type="diag_axiom_part" input="{TSectionId}"}--> <!--{type="hint_check"}--></div>
key_step_choice_question_tab=<div class="instruction-item"> <!--{type="hint_itemize"}--> Select tab <!--{type="question_tab" input="{tabQuestionValue}"}--> <!--{type="hint_check"}--></div>
key_step_choice_tab_index_in_diag=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on tab <!--{type="diag_tab" input="{actIdx}"}--> <!--{type="hint_check"}--></div>
key_step_click_apply=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on <!--{type="button_apply"}--> in 'preview section'. <!--{type="hint_check"}--></div>
key_step_click_deduce=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on <!--{type="button_deduce"}--> of <!--{type="propdeftag" input="{statementId}"}--> <!--{type="tag" input="{statementId}"}--> to display diagnostic window. <!--{type="hint_check"}--></div>
key_step_click_justify=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on <!--{type="button_justify"}--> of statement <!--{type="tag" input="{statementId}"}--> to diaply diagnostic window. <!--{type="hint_check"}--></div>
key_step_delete=<div class="instruction-item"> <!--{type="hint_itemize"}--> Delete statement <!--{type="tag" input="{statementId}"}--> <!--{type="hint_check"}--></div>
key_step_deleteby=<div class="instruction-item"> <!--{type="hint_itemize"}--> Delete justification of statement <!--{type="tag" input="{statementId}"}--> <!--{type="hint_check"}--></div>
key_step_drag=<div class="instruction-item"> <!--{type="hint_itemize"}--> Drag rule <!--{type="toolbox_item" readonly="true" input="{axiomId}"}--> from section <!--{type="label_toolbox" class="toolbox-section-title-content" input="{TSectionId}"}-->. <!--{type="hint_check"}--></div>
key_step_drop=<div class="instruction-item"> <!--{type="hint_itemize"}--> Drop it on statement <!--{type="propdeftag" input="{statementId}"}--> <!--{type="tag" input="{statementId}"}--> <!--{type="hint_check"}--></div>
key_step_enter_expr_in_diag=<div class="instruction-item"> <!--{type="hint_itemize"}--> Enter value <!--{type="expr" statement="{statementId}" input="{actArgItemSecond}"}--> with virutal keyboard for proof variable <!--{type="evar" input="{evarId}"}--> <!--{type="hint_check"}--></div>
key_step_inst=<div class="instruction-item"> <!--{type="hint_itemize"}--> Enter value <!--{type="expr" input="{actTypArg2}"}--> for <!--{type="paper_evar" input="{actTypArg}"}--> <!--{type="hint_check"}--></div>
key_step_open_toolbox=<div class="instruction-item"> <!--{type="hint_itemize"}--> Open toolbox by clicking on <!--{type="toolbox_header_button"}--> <!--{type="hint_check"}--></div>
key_step_section=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on <!--{type="button_section"}--> of statement <!--{type="tag" input="{statementId}"}--> <!--{type="hint_check"}--></div>
key_step_selection=<div class="instruction-item"> <!--{type="hint_itemize"}--> Select, in statement <!--{type="tag" input="{statementId}"}-->, the term hilighted in blue below : <br> <div>  <!--{type="prop" statement="{statementId}" input="{selectionProp}"}-->  <!--{type="hint_check"}--> </div></div>
key_step_unification=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on <!--{type="button_unify" input="{actTypArg}"}--> of statement <!--{type="tag" input="{statementId}"}--> <!--{type="hint_check"}--></div>
key_step_unify_in_diag=<div class="instruction-item"> <!--{type="hint_itemize"}--> Click on <!--{type="button_unify" input="{actUnifItem}"}--> <!--{type="hint_check"}--></div>
key_sub_subscription_sentence=Thank you ! A confirmation link has been sent to your email address.
key_success_trophy_message=Congratulations, you just get the cockade {trophyId}, for chapter {chapterId}
key_success_trophy_title=Cockade {trophyId}
key_task_justify_label=Justify
key_then=then
key_to_justify=to justify
key_toolbox_error_message=This rule does not apply to this statement.
key_tooltip_axiom_close=hide formula
key_tooltip_axiom_open=display formula
key_tooltip_context_close=display context
key_tooltip_context_open=hide context
key_tooltip_section_close=hide scope
key_tooltip_section_open=display scope
key_trophy_diagnostic=diagnosis
key_trophy_exercises=Fiscal Year 2010
key_trophy_tutorial=tutorial
key_trophy_unavoidable=unavoidable
key_tutorial=Tutorial
key_uid=ID
key_unlock=Unlock
key_update_browser=You are currently using {browser} in version {current_version}. This version is not compatible with edukera application. Please, update or change your browser.
key_usage=Usage
key_utterance=Utterance
key_validate=Validate
key_with=with
key_without_hint=No hint for this exercise.
key_yes=Yes
pager_account=My account
pager_adabusrdum=Ad absurdum
pager_algebra=Algebra
pager_algebra_structures=Structures algébriques
pager_algebra_structures_01=
pager_analysis=Analysis
pager_analysis_induction=Induction
pager_analysis_limits=Limits
pager_analysis_series=Series
pager_analysis_series_05=
pager_badges=Cockades
pager_classical=Classical
pager_comb=Systems of equations
pager_commutativity=Commutativity
pager_credits=Credits
pager_dashboard=Dashboard
pager_demo_bernoulli_1=Bernoulli inequality 1
pager_demo_bernoulli_2=Bernoulli inequality 2
pager_demo_medium_ex_02=Divisibility
pager_demo_seg=Calculus
pager_demo_tuto_app=Applications
pager_demo_tuto_comb=Combinations
pager_demo_tuto_first=Left and right operations
pager_demo_tuto_fun=Definitions
pager_demo_tuto_neq=Inequality
pager_demo_tuto_rel=Transitivity
pager_demo_tuto_serie=Limit of 1/n
pager_demo_tuto_sigma=The sum of the first n integers
pager_demorgan=De Morgan
pager_easy=Easy
pager_enigma=Enigmas
pager_eq_seg=Equality
pager_eqothers=Mixtures
pager_existence=Existence
pager_expansion=Distributivity
pager_finj=Injectivity
pager_funpigeon=Pigeonhole principle
pager_funsurj=Surjectivity
pager_good_bad=Truths and lies
pager_hard=Hard
pager_ind_bernouilli=Inequalities
pager_ind_divis=Divisibility
pager_ind_sum=Calculations of sum
pager_ineq_ex_15=Operations
pager_ineq_ex_20=Combinations
pager_ineq_ex_22=Double inequality
pager_ineq_ex_24=Applications
pager_ineq_ex_25=Relation
pager_ineq_seg=Inequality
pager_ineq_system=Systems of inequalities
pager_ineqs=Inequalities
pager_limits_finite=Limits of functions at a finite point
pager_limits_inf=Functions limit at infinity
pager_limits_prop=Properties by definition
pager_limits_series=eries limits
pager_logic=Logic
pager_logic_connector=Connectors
pager_logic_connector_abs_peirce=Peirce's law by reduction ad absurdium
pager_logic_connector_associativity=Associativities
pager_logic_connector_classical=Classical logic
pager_logic_connector_constructivism=Constructivist logic
pager_logic_connector_deMorgan_laws=De Morgan's laws
pager_logic_connector_distributivity=Distributive properties
pager_logic_connector_ex_easy_01=Distributivity of disjunction
pager_logic_connector_ex_easy_02=Distributivity of the conjunction
pager_logic_connector_ex_easy_06=The universe of integers 1/2
pager_logic_connector_ex_easy_08=The syllogism
pager_logic_connector_ex_easy_12=De Morgan's laws 3/3
pager_logic_connector_ex_easy_13=De Morgan's laws 1/3
pager_logic_connector_ex_easy_14=Associativity of conjunction
pager_logic_connector_ex_easy_16=Contraposition 1/2
pager_logic_connector_ex_easy_17=Contraposition 2/2
pager_logic_connector_ex_easy_27=Associativity of disjunction
pager_logic_connector_ex_easy_31=Ad absurdium reasoning
pager_logic_connector_ex_easy_32=De Morgan’s laws 2/3
pager_logic_connector_ex_easy_33=Distributivity of disjunction
pager_logic_connector_ex_easy_34=Distributivity of conjunction
pager_logic_connector_negation=Negations
pager_logic_connector_peirce_abs_te=reduction ad absurdium by Peirce's law
pager_logic_connector_peirce_law=Peirce's law
pager_logic_connector_reasoning=Reasonings
pager_logic_connector_training=Basics
pager_logic_connector_tuto_01=To deduce from a conjunction
pager_logic_connector_tuto_02=To prove a conjunction
pager_logic_connector_tuto_03=To Prove a disjunction
pager_logic_connector_tuto_04=Case base reasoning
pager_logic_connector_tuto_06=To prove an implication
pager_logic_connector_tuto_07=To deduce from an implication
pager_logic_connector_tuto_08=To prove a negation
pager_logic_connector_tuto_085=To deduce from a negation
pager_logic_connector_tuto_09=Ex False quodlibet
pager_logic_connector_tuto_10=Excluded middle
pager_logic_function=Functions
pager_logic_quantifer_tuto_2=The universe of integers 2/2
pager_logic_quantifier=Quantifiers
pager_logic_quantifier_21=The Scottish Club
pager_logic_quantifier_ex_01=Distributivity of union
pager_logic_quantifier_ex_02=Distributivity of intersection
pager_logic_quantifier_ex_03=De Morgan Law 1/2
pager_logic_quantifier_ex_04=De Morgan law 2/2
pager_logic_quantifier_ex_05=Power set
pager_logic_quantifier_ex_06=Distributivity of the cartesian product
pager_logic_quantifier_ex_07=Existential distributivity
pager_logic_quantifier_ex_easy_08=De Morgan law 2/2
pager_logic_quantifier_ex_easy_09=De Morgan law 1/2
pager_logic_quantifier_ex_le_01=Is less than
pager_logic_quantifier_ex_le_02=Is less than (2)
pager_logic_quantifier_ex_le_03=Is less than (3)
pager_logic_quantifier_ex_le_04=Honestants and Swindlecants 1/4
pager_logic_quantifier_ex_le_05=Honestants and Swindlecants 2/4
pager_logic_quantifier_ex_le_06=Honestants and Swindlecants 3/4
pager_logic_quantifier_ex_le_07=Honestants and Swindlecants 4/4
pager_logic_quantifier_ex_le_08=Inverse, Injection
pager_logic_quantifier_ex_le_10=Total relations
pager_logic_quantifier_ex_le_13=The Pigeonhole Principle 1/2
pager_logic_quantifier_ex_le_14=The Pigeonhole Principle 2/2
pager_logic_quantifier_ex_le_15=Binary relations
pager_logic_quantifier_ex_le_37=Distributivity of the cartesian product
pager_logic_quantifier_ex_le_40=Function, injection
pager_logic_quantifier_ex_le_41=Surjection function
pager_logic_quantifier_ex_le_42=Involution, bijection
pager_logic_quantifier_ex_le_43=Composition
pager_logic_quantifier_ex_le_48=Law of excluded middle by ad absurdium reasoning
pager_logic_quantifier_ex_le_52=Symmetry of equality
pager_logic_quantifier_ex_le_53=Transitivity of equality
pager_logic_quantifier_ex_le_54=Transitivity of inclusion
pager_logic_quantifier_ex_le_67=Intersection of equalities
pager_logic_quantifier_ex_le_68=Union of equalities
pager_logic_quantifier_ex_le_69=Intersection of inclusions
pager_logic_quantifier_ex_le_70=Union of inclusions
pager_logic_quantifier_ex_le_71=Ms. Confuse
pager_logic_quantifier_ex_le_72=Three hats enigma
pager_logic_quantifier_tuto_01=To prove an existence
pager_logic_quantifier_tuto_02=To deduce an existence
pager_logic_quantifier_tuto_03=To prove a theorem
pager_logic_quantifier_tuto_04=To deduce from a theorem
pager_logic_relation=Relations
pager_logic_relation_tuto_01=Graph of a relation
pager_logic_relation_tuto_04=Equivalence
pager_logic_relation_tuto_05=Composition
pager_logic_set_rewrite_01=Rewriting
pager_logic_set_rewrite_03=Associativity
pager_logic_set_rewrite_04=Commutativity
pager_logic_set_rewrite_05=Simplification
pager_logic_set_rewrite_06=Development / Factoring
pager_logic_set_rewrite_08=Symmetry of equality
pager_logic_set_rewrite_09=Transitivity of equality
pager_logic_set_rewrite_10=Transitivity of inclusion
pager_logic_set_rewrite_11=Combinations
pager_logic_settheory_tuto_01=Intersection
pager_logic_settheory_tuto_02=Union
pager_logic_settheory_tuto_03=Difference
pager_logic_settheory_tuto_04=Complement
pager_logic_settheory_tuto_05=Inclusion
pager_logic_settheory_tuto_06=Equality
pager_logic_settheory_tuto_07=Empty set
pager_logic_settheory_tuto_08=Power set
pager_logic_settheory_tuto_09=Cartesian product
pager_lrops=Left and right Operations
pager_medium=Medium
pager_relcar=Set formulation
pager_relcomp=Composition
pager_relequiv=Equivalence
pager_relinv=Reverse
pager_relle=Relation '≤'
pager_reltrans=Transitivity
pager_rew_almostsquare=Almost perfect squares
pager_rew_conjugate=Conjugate values
pager_rew_equation=Equations
pager_rew_factorize=Factorisations
pager_rew_gold=Gold number
pager_rew_system=Systems of equations
pager_rew_tuto_develop=Development
pager_rew_tuto_fact1=Factorisation
pager_rew_tuto_fact2=Remarkable factorization
pager_rew_tuto_group=Grouping
pager_rew_tuto_idrem1=Différence de carrés
pager_rew_tuto_idrem2=Difference of squares
pager_rew_tuto_misc1=Commutativity
pager_rew_tuto_misc2=Rewriting
pager_rew_tuto_op=Operations
pager_rew_tuto_simpl=Simplifications
pager_rew_tuto_simpl2=Common denominator
pager_rew_tuto_varchange=Change of variables
pager_rewrite_seg=Rewritings
pager_root=Home
pager_series_arith=Arithmetic progressions
pager_series_arithgeo=Arithmetico-geometric sequences
pager_series_bounded=Bounded sequences
pager_series_ex_01=
pager_series_geo=Geometric sequences
pager_series_variation=Monotonicity
pager_set_operators=Operators
pager_set_rewoperators=Set calculus
pager_setcomb=Combinations
pager_setdemorgan=De Morgan
pager_setdistrib=Distributive properties
pager_setinclusion=Inclusions
pager_setprop=Properties
pager_settheory=Sets
pager_sigma_ex_15=Sum of the first integers
pager_sigma_ex_16=Sum of the first square
pager_sigma_ex_18=Decomposition
pager_sigma_ex_19=Association
pager_sigma_ex_20=Index shifting
pager_sigma_ex_21=Sum of the first powers
pager_sigma_ex_22=linearity
pager_sigma_ex_23=Remarkable sums
pager_sigma_ref=Standard sums
pager_sigma_seg=Sigma
pager_sigma_telescop=Telescoping series
pager_sigma_withref=Using the standard sums
pager_syllogism=Syllogisms
toolbox_analysis=Analysis
toolbox_appdef=Function definition
toolbox_arith_series=Arithmetic progression
toolbox_binrel=Binary relation
toolbox_calculus=Calculus
toolbox_combinaison=Combinaisons
toolbox_conjunction=Conjunction
toolbox_connector=Connector
toolbox_converge=Convergence
toolbox_disjonction=Disjunction
toolbox_distrib=Distributivity
toolbox_eq=Equality
toolbox_eqfun=Equality
toolbox_eqrel=Equal relation
toolbox_eqset=Equality
toolbox_equiv=Equivalence
toolbox_exists=Existential quantifier
toolbox_fact=Factorial
toolbox_forall=Universal quantifier
toolbox_function=Function
toolbox_funop=Functional operators
toolbox_geo_series=Geometric sequence
toolbox_implication=Implication
toolbox_induction=Récurrence
toolbox_ineq=Inequality
toolbox_ineqapp=Applications
toolbox_ineqbound=Double inequality
toolbox_ineqcomb=Combinations
toolbox_ineqconv=Conversions
toolbox_ineqrel=Relation
toolbox_leftright=Left and right operations
toolbox_leftright_ineq=Left and right operations
toolbox_leftright_neq=Inequality
toolbox_limfinite=Limit at a point
toolbox_limitinf=Limit at infinity
toolbox_limitops=Operations
toolbox_limits=Limit
toolbox_logic=Logic
toolbox_logicothers=Classical logic
toolbox_lrapply=Applications
toolbox_multiple=Divisibility
toolbox_negation=Negation
toolbox_oldest=Etre le plus agé
toolbox_operation=Operation
toolbox_operation_rewrite=Rewriting
toolbox_prod=
toolbox_prodidx=
toolbox_prodrem=
toolbox_quantifier=Quantifiers
toolbox_quantifier_confuse=Mrs. Confuse
toolbox_quantifier_truthlie=Truths and lies
toolbox_relation=Relation
toolbox_relops=Relational operators
toolbox_relothers=Remarkable Relations
toolbox_relprop=Relation
toolbox_relset=Set relations
toolbox_remid=Remarkable rewritings
toolbox_rewops=Operations
toolbox_rewprops=Rewritings
toolbox_rewrite=Rewriting
toolbox_series=Series
toolbox_series_limitation=Bounding
toolbox_series_sign=Sign
toolbox_series_variation=Monotonicity
toolbox_set=Set
toolbox_set_comb=Combinations
toolbox_set_rewriting=Rewritings
toolbox_setexpr=Set formulation
toolbox_setfun=Function
toolbox_setgraph=Graphe de relation
toolbox_setops=Operations
toolbox_sigma=Sigma rewriting
toolbox_sigmaidx=Index shiftings
toolbox_sigmarem=Remarkable formulas
toolbox_simpl=Simplifications
toolbox_slteq=Inclusion
toolbox_somesets=Remarkable sets
toolbox_sophiehat=Three hats enigma
toolbox_sophiehattheory=Hat theory
toolbox_true_at_rank=True to the rank n
toolbox_truthlie=Vérités et mensonges
toolbox_youngest=Etre le plus jeune
type_BinRel_arg=binary relation on {1}
type_BinRel_dec=Let {id} be a binary relation on {1}
type_BinRel_dec_body=Let {id} be a binary relation on {1} defined by {body}
type_BinRel_exists_several=there exist {id} binary relations on {1} such that
type_BinRel_exists_simple=there exists {id} a binary relation on {1} such that
type_BinRel_forall_several=for every {id} binary relations on {1},
type_BinRel_forall_simple=for every {id} a binary relation on {1},
type_BinRel_letin_several=
type_BinRel_letin_simple=
type_BinRel_sci_arg=({1}×{1})
type_BinRel_sci_dec=Let {id} ⊆ {1}×{1}
type_BinRel_sci_dec_body=Let {id} be a binary relation on {1} defined by {body}
type_BinRel_sci_exists_several=∃ {cartesian_id} ⊆ {cartesian_type},
type_BinRel_sci_exists_simple=∃ {id} ⊆ {1}×{1},
type_BinRel_sci_forall_several=∀ {cartesian_id} ⊆ {cartesian_type},
type_BinRel_sci_forall_simple=∀ {id} ⊆ {1}×{1},
type_BinRel_sci_letin_several=
type_BinRel_sci_letin_simple=
type_Child_arg=child
type_Child_dec=Let {id} be a child
type_Child_dec_body=
type_Child_exists_several=there exist children {id} such that
type_Child_exists_simple=there exists a child {id} such that
type_Child_forall_several=for every children {id},
type_Child_forall_simple=for every child {id},
type_Child_letin_several=
type_Child_letin_simple=
type_Child_sci_arg=child
type_Child_sci_dec=Let {id} be a child
type_Child_sci_dec_body=
type_Child_sci_exists_several=there exist children {id} such that
type_Child_sci_exists_simple=there exists a child {id} such that
type_Child_sci_forall_several=for every children {id},
type_Child_sci_forall_simple=for every child {id},
type_Child_sci_letin_several=
type_Child_sci_letin_simple=
type_Domain_arg=interval
type_Domain_dec=Let {id} be an interval
type_Domain_dec_body=Let the interval {id} defined by {body}
type_Domain_exists_several=there exist intervals {id} such as,
type_Domain_exists_simple=there exists an interval {id} such that,
type_Domain_forall_several=for every intervals {id};
type_Domain_forall_simple=for every interval {id}
type_Domain_letin_several=
type_Domain_letin_simple=
type_Domain_sci_arg=interval
type_Domain_sci_dec=Let {id} be an interval
type_Domain_sci_dec_body=Let {id} = {body}
type_Domain_sci_exists_several=∃ {id},
type_Domain_sci_exists_simple=∃ {id},
type_Domain_sci_forall_several=∀ {id},
type_Domain_sci_forall_simple=∀ {id},
type_Domain_sci_letin_several=
type_Domain_sci_letin_simple=
type_ExSet_arg={id}
type_ExSet_dec=Let {id} be a set
type_ExSet_dec_body=Let {id} be a set defined by {body}
type_ExSet_exists_several=there exist sets {id} such that
type_ExSet_exists_simple=there exists a set  {id} such that
type_ExSet_forall_several=for every sets {id},
type_ExSet_forall_simple=for every set {id}
type_ExSet_letin_several=
type_ExSet_letin_simple=
type_ExSet_sci_arg={id}
type_ExSet_sci_dec=Let {id} be a set
type_ExSet_sci_dec_body=Let {id} be a set defined by {body}
type_ExSet_sci_exists_several=there exist sets {id} such that
type_ExSet_sci_exists_simple=there exists a set  {id} such that
type_ExSet_sci_forall_several=for every sets {id},
type_ExSet_sci_forall_simple=for every set {id},
type_ExSet_sci_letin_several=
type_ExSet_sci_letin_simple=
type_ExprFun_arg=function from ℝ to ℝ
type_ExprFun_dec=Let {id} be a function from ℝ to ℝ
type_ExprFun_dec_body=Let {id} be a function from ℝ to ℝ defined by {body}
type_ExprFun_exists_several=
type_ExprFun_exists_simple=
type_ExprFun_forall_several=for every functions {id} from ℝ to ℝ,
type_ExprFun_forall_simple=for every function {id} from ℝ to ℝ,
type_ExprFun_letin_several=
type_ExprFun_letin_simple=
type_ExprFun_sci_arg=
type_ExprFun_sci_dec=Let f : ℝ→ℝ
type_ExprFun_sci_dec_body=Let f : ℝ→ℝ defined by {body}
type_ExprFun_sci_exists_several=
type_ExprFun_sci_exists_simple=
type_ExprFun_sci_forall_several=
type_ExprFun_sci_forall_simple=
type_ExprFun_sci_letin_several=
type_ExprFun_sci_letin_simple=
type_Expr_arg=real number
type_Expr_dec=Let {id} be a real number
type_Expr_dec_body=Let {id} be a real number defined by {body}
type_Expr_exists_several=there exist real numbers {id} such that
type_Expr_exists_simple=there  exists a real number {id} such that
type_Expr_forall_several=for every real numbers {id},
type_Expr_forall_simple=for every real number {id},
type_Expr_letin_several=
type_Expr_letin_simple={id} the real {id} defined by {body}
type_Expr_sci_arg=ℝ
type_Expr_sci_dec=Let {id} {math:∊} ℝ
type_Expr_sci_dec_body=Let {id}={body}
type_Expr_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_Expr_sci_exists_simple=∃ {id} {math:∊} ℝ,
type_Expr_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_Expr_sci_forall_simple=∀ {id} {math:∊} ℝ,
type_Expr_sci_letin_several=
type_Expr_sci_letin_simple={id} {math:∊} ℝ, {id} = {body}
type_FRel_arg=
type_FRel_dec=
type_FRel_dec_body=
type_FRel_exists_several=
type_FRel_exists_simple=
type_FRel_forall_several=
type_FRel_forall_simple=
type_FRel_letin_several=
type_FRel_letin_simple=
type_FRel_sci_arg={2}×{3}
type_FRel_sci_dec=Soit {id} ⊆ {2}×{3}
type_FRel_sci_dec_body=
type_FRel_sci_exists_several=
type_FRel_sci_exists_simple=
type_FRel_sci_forall_several=∀ {cartesian_id} ⊆ {cartesian_type},
type_FRel_sci_forall_simple=∀ {id} ⊆ {2}×{3},
type_FRel_sci_letin_several=
type_FRel_sci_letin_simple=
type_FunDef_arg=the function defined on {2}
type_FunDef_dec=Let {id} be a function defined on {2}
type_FunDef_dec_body=Let {id} be a function defined on {2} by {body}
type_FunDef_exists_several=there exist {id} functions on {2} such that,
type_FunDef_exists_simple=there exists {id} a function defined on {2} such that,
type_FunDef_forall_several=for  every function defined on {2} {id},
type_FunDef_forall_simple=for every function defined on {2} {id},
type_FunDef_letin_several=
type_FunDef_letin_simple={id} is the function on {2} by {body}
type_FunDef_sci_arg={2}→{2}
type_FunDef_sci_dec=Let {id}: {2}→{2}
type_FunDef_sci_dec_body=Let {id}: {2}→{2} defined by {body}
type_FunDef_sci_exists_several=∃ {pair_id} : {2}→{2},
type_FunDef_sci_exists_simple=∃ {id} : {2}→{2},
type_FunDef_sci_forall_several=∀ {pair_id} : {2}→{2},
type_FunDef_sci_forall_simple=∀ {id} : {2}→{2},
type_FunDef_sci_letin_several=
type_FunDef_sci_letin_simple={id} is the function on {2} by {body}
type_FunUnknown_arg=the function
type_FunUnknown_dec=Let {id} be a function
type_FunUnknown_dec_body=Let {id} be a function defined on {0}{2}{/0} by {body}
type_FunUnknown_exists_several=there exist functions {id} such as,
type_FunUnknown_exists_simple=there exist a function {id} such that,
type_FunUnknown_forall_several=for every functions {id},
type_FunUnknown_forall_simple=for every function {id},
type_FunUnknown_letin_several=
type_FunUnknown_letin_simple={id} is the function defined by {body}
type_FunUnknown_sci_arg={0}→{1}
type_FunUnknown_sci_dec=Let {id}: {0}→{1}
type_FunUnknown_sci_dec_body=Let {id}:{0}→{1} defined by {body}
type_FunUnknown_sci_exists_several=∃ {pair_id} : {0}→{1},
type_FunUnknown_sci_exists_simple=∃ {id} : {0}→{1},
type_FunUnknown_sci_forall_several=∀ {pair_id} : {0}→{1},
type_FunUnknown_sci_forall_simple=∀ {id} : {0}→{1},
type_FunUnknown_sci_letin_several=
type_FunUnknown_sci_letin_simple=
type_Fun_arg=function from {2} to {3}
type_Fun_dec=Let {id} be a function from {2} to {3}
type_Fun_dec_body=Let {id} be a function from {2} to {3} defined by {body}
type_Fun_exists_several=there exist {id} functions from {2} to {3},
type_Fun_exists_simple=there exists {id} a function form {2} to {3},
type_Fun_forall_several=for every functions {id} from {2} to {3},
type_Fun_forall_simple=for every function {id} from {2} to {3},
type_Fun_letin_several=
type_Fun_letin_simple={id} is the application from {2} to {3} defined by {body}
type_Fun_sci_arg={2}→{3}
type_Fun_sci_dec=Let {id} : {2}→{3}
type_Fun_sci_dec_body=Let {id} : {2}→{3} defined by {body}
type_Fun_sci_exists_several=∃ {pair_id} : {2}→{3},
type_Fun_sci_exists_simple=∃ {id} : {2}→{3},
type_Fun_sci_forall_several=∀ {pair_id} : {2}→{3},
type_Fun_sci_forall_simple=∀ {id} : {2}→{3},
type_Fun_sci_letin_several=
type_Fun_sci_letin_simple={id} is the application from {2} to {3} defined by {body}
type_HatColor_arg=color
type_HatColor_dec=Let {id} be a color
type_HatColor_dec_body=
type_HatColor_exists_several=there exist colors {id} such that,
type_HatColor_exists_simple=there exists a color {id} such that,
type_HatColor_forall_several=for every colors {id},
type_HatColor_forall_simple=for every color {id},
type_HatColor_letin_several=
type_HatColor_letin_simple=
type_LimitExpr_arg=limit value
type_LimitExpr_dec=Let {id} be a limit value
type_LimitExpr_dec_body=Let the limit value {id} = {body}
type_LimitExpr_exists_several=there exist limit values such that,
type_LimitExpr_exists_simple=there exist a limit value {id} such that,
type_LimitExpr_forall_several=for every limit values {id},
type_LimitExpr_forall_simple=for every limit value {id},
type_LimitExpr_letin_several=
type_LimitExpr_letin_simple=
type_LimitExpr_sci_arg=
type_LimitExpr_sci_dec=
type_LimitExpr_sci_dec_body=
type_LimitExpr_sci_exists_several=
type_LimitExpr_sci_exists_simple=
type_LimitExpr_sci_forall_several=
type_LimitExpr_sci_forall_simple=
type_LimitExpr_sci_letin_several=
type_LimitExpr_sci_letin_simple=
type_Neighborhood_arg=the neighborhood of {0}
type_Neighborhood_dec=Let {id} be a neighborhood of {0}
type_Neighborhood_dec_body=Let {id} be a neighborhood of {0} defined by {body}
type_Neighborhood_exists_several=there exist neighborhoods of {0} {id} such that,
type_Neighborhood_exists_simple=there exists a neighborhood of {0} {id} such that,
type_Neighborhood_forall_several=for  every neighborhoods of {0} {id},
type_Neighborhood_forall_simple=for every neighborhood of {0} {id},
type_Neighborhood_letin_several=
type_Neighborhood_letin_simple={id} the neighborhood of {0} defined by {body}
type_Neighborhood_sci_arg=𝓥({0})
type_Neighborhood_sci_dec=Let {id} {math:∊} 𝓥({0})
type_Neighborhood_sci_dec_body=Let {id}={body}
type_Neighborhood_sci_exists_several=∃ {pair_id} {math:∊} 𝓥({0}),
type_Neighborhood_sci_exists_simple=∃ {id} {math: 𝓥 ε} ( {0} )
type_Neighborhood_sci_forall_several={} {∀ pair_id math: 𝓥 ε} ( {0} )
type_Neighborhood_sci_forall_simple=∀ {id} {math: 𝓥 ε} ( {0} )
type_Neighborhood_sci_letin_several=
type_Neighborhood_sci_letin_simple=
type_NvarFun_arg=function form ℕ to ℕ
type_NvarFun_dec=Let {id} be a function from ℕ to ℕ
type_NvarFun_dec_body=Let {id} be a function from ℕ to ℕ defined by {body}
type_NvarFun_exists_several=
type_NvarFun_exists_simple=
type_NvarFun_forall_several=for every functions {id} from ℕ to ℕ,
type_NvarFun_forall_simple=for every function {id} from ℕ to ℕ,
type_NvarFun_letin_several=
type_NvarFun_letin_simple={id} is the application of ℕ to ℕ defined by {body}
type_NvarFun_sci_arg=
type_NvarFun_sci_dec=Let f : ℕ→ℕ
type_NvarFun_sci_dec_body=Let f : ℕ→ℕ defined by {body}
type_NvarFun_sci_exists_several=
type_NvarFun_sci_exists_simple=
type_NvarFun_sci_forall_several=
type_NvarFun_sci_forall_simple=
type_NvarFun_sci_letin_several=
type_NvarFun_sci_letin_simple={id} is the application of ℕ to ℕ defined by {body}
type_NvarProp_arg=
type_NvarProp_dec=Let {id} be a proposition defined on ℕ
type_NvarProp_dec_body=Let {id} be a proposition defined at rank {var} by {body}
type_NvarProp_exists_several=
type_NvarProp_exists_simple=
type_NvarProp_forall_several=
type_NvarProp_forall_simple=for every proposition {id} defined on ℕ
type_NvarProp_letin_several=
type_NvarProp_letin_simple=
type_NvarProp_sci_arg=
type_NvarProp_sci_dec=Let {id} be a proposition defined on ℕ
type_NvarProp_sci_dec_body=Let {id} be a proposition defined at rank {var} by {body}
type_NvarProp_sci_exists_several=
type_NvarProp_sci_exists_simple=
type_NvarProp_sci_forall_several=
type_NvarProp_sci_forall_simple=for every proposition {id} defined on ℕ,
type_NvarProp_sci_letin_several=
type_NvarProp_sci_letin_simple=
type_NvarRel_arg=
type_NvarRel_dec=Let {id} be a proposition defined on ℕ×ℕ
type_NvarRel_dec_body=
type_NvarRel_exists_several=
type_NvarRel_exists_simple=
type_NvarRel_forall_several=
type_NvarRel_forall_simple=for every proposition {id} defined on ℕ×ℕ,
type_NvarRel_letin_several=
type_NvarRel_letin_simple=
type_Nvar_arg=integer
type_Nvar_dec=Let {id} be an integer
type_Nvar_dec_body=Let {id} be an integer defined by {body}
type_Nvar_exists_several=there exist integers {id} such that
type_Nvar_exists_simple=there exists an integer {id} such that
type_Nvar_forall_several=for every integers {id},
type_Nvar_forall_simple=for every integer {id},
type_Nvar_letin_several=
type_Nvar_letin_simple=
type_Nvar_sci_arg=ℕ
type_Nvar_sci_dec=Let {id} {math:∊} ℕ
type_Nvar_sci_dec_body=Let {id}={body}
type_Nvar_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_Nvar_sci_exists_simple=∃ {id} {math:∊} ℕ,
type_Nvar_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_Nvar_sci_forall_simple=∀ {id} {math:∊} ℕ,
type_Nvar_sci_letin_several=
type_Nvar_sci_letin_simple=
type_O1BinRel_arg=binary relation on {0}
type_O1BinRel_dec=Let {id} be a binary relation on {0}
type_O1BinRel_dec_body=Let {id} be a binary relation on {0} defined by {body}
type_O1BinRel_exists_several=there exist binary relations {id} on {0} such that
type_O1BinRel_exists_simple=there exists a binary relation {id} on {0} such that
type_O1BinRel_forall_several=for every binary relations {id} on {0},
type_O1BinRel_forall_simple=for every binary relation {id} on {0},
type_O1BinRel_letin_several=
type_O1BinRel_letin_simple=
type_O1BinRel_sci_arg=({0}×{0})
type_O1BinRel_sci_dec=Let {id} ⊆ {0}×{0}
type_O1BinRel_sci_dec_body=Let {id} be a binary relation on {0} defined {body}
type_O1BinRel_sci_exists_several=∃ {cartesian_id} ⊆ {cartesian_type},
type_O1BinRel_sci_exists_simple=∃ {id} ⊆ {0}×{0},
type_O1BinRel_sci_forall_several=∀ {cartesian_id} ⊆ {cartesian_type},
type_O1BinRel_sci_forall_simple=∀ {id} ⊆ {0}×{0},
type_O1BinRel_sci_letin_several=
type_O1BinRel_sci_letin_simple=
type_O1ExSet_arg=set
type_O1ExSet_dec=Let {id} be a set
type_O1ExSet_dec_body=Let {id}={body}
type_O1ExSet_exists_several=there exist sets {id} such that
type_O1ExSet_exists_simple=there exists a set {id} such that
type_O1ExSet_forall_several=for every sets {id},
type_O1ExSet_forall_simple=for every set {id},
type_O1ExSet_letin_several=
type_O1ExSet_letin_simple=
type_O1ExSet_sci_arg=set
type_O1ExSet_sci_dec=Let {id} be a set
type_O1ExSet_sci_dec_body=Let {id}={body}
type_O1ExSet_sci_exists_several=∃ {id},
type_O1ExSet_sci_exists_simple=∃ {id},
type_O1ExSet_sci_forall_several=for every sets {id},
type_O1ExSet_sci_forall_simple=for every set {id},
type_O1ExSet_sci_letin_several=
type_O1ExSet_sci_letin_simple=
type_O1Fun_arg=function from {0} to {1}
type_O1Fun_dec=Let {id} be a function from {0} to {1}
type_O1Fun_dec_body=Let {id} be a function from {0} to {1} defined by {body}
type_O1Fun_exists_several=there exist functions {id} from {0} to {1} such that
type_O1Fun_exists_simple=there exists a function {id} from {0} to {1} such that
type_O1Fun_forall_several=for every functions {id} from {0} to {1},
type_O1Fun_forall_simple=for every function {id} from {0} to {1},
type_O1Fun_letin_several=
type_O1Fun_letin_simple=
type_O1Fun_sci_arg={0}→{1}
type_O1Fun_sci_dec=Let {id} : {0}→{1}
type_O1Fun_sci_dec_body=Let {id} : {0}→{1} defined by {body}
type_O1Fun_sci_exists_several=∃ {pair_id} : {0}→{1},
type_O1Fun_sci_exists_simple=∃ {id} : {0}→{1},
type_O1Fun_sci_forall_several=∀ {pair_id} : {0}→{1},
type_O1Fun_sci_forall_simple=∀ {id} : {0}→{1},
type_O1Fun_sci_letin_several=
type_O1Fun_sci_letin_simple=
type_O1Rel_arg=relation de {0}×{1}
type_O1Rel_dec=Let {id} be a relation on {0}×{1}
type_O1Rel_dec_body=Let {id} be a relation on {0}×{1} defined by {body}
type_O1Rel_exists_several=there exist relations {id} on {0}×{1} such that
type_O1Rel_exists_simple=there exists a relation {id} on {0}×{1} such that
type_O1Rel_forall_several=for every relations {id} on {0}×{1},
type_O1Rel_forall_simple=for every relation {id} on {0}×{1},
type_O1Rel_letin_several=
type_O1Rel_letin_simple=
type_O1Rel_sci_arg=({0}×{1})
type_O1Rel_sci_dec=Let {id} ⊆ {0}×{1}
type_O1Rel_sci_dec_body=Let {id} ⊆ {0}×{1} defined by {body}
type_O1Rel_sci_exists_several=∃ {cartesian_id} ⊆ {cartesian_type},
type_O1Rel_sci_exists_simple=∃ {id} ⊆ {0}×{1},
type_O1Rel_sci_forall_several=∀ {cartesian_id} ⊆ {cartesian_type},
type_O1Rel_sci_forall_simple=∀ {id} ⊆ {0}×{1},
type_O1Rel_sci_letin_several=
type_O1Rel_sci_letin_simple=
type_O1SetProp2_arg=formula
type_O1SetProp2_dec=Let {id} be a formula
type_O1SetProp2_dec_body=Let {id} be a formula defined by {body}
type_O1SetProp2_exists_several=there exist formulas {id} such that
type_O1SetProp2_exists_simple=there exists a formula {id} such that
type_O1SetProp2_forall_several=for every formulas {id},
type_O1SetProp2_forall_simple=for every formula {id},
type_O1SetProp2_letin_several=
type_O1SetProp2_letin_simple=
type_O1SetProp2_sci_arg=formula
type_O1SetProp2_sci_dec=Let {id} be a formula
type_O1SetProp2_sci_dec_body=Let {id} be a formula defined by {body}
type_O1SetProp2_sci_exists_several=there exist formulas {id} such that
type_O1SetProp2_sci_exists_simple=there exists a formula {id} such that
type_O1SetProp2_sci_forall_several=for every formulas {id},
type_O1SetProp2_sci_forall_simple=for every formula {id},
type_O1SetProp2_sci_letin_several=
type_O1SetProp2_sci_letin_simple=
type_O1SetProp_arg=formula
type_O1SetProp_dec=Let {id} be a formula
type_O1SetProp_dec_body=Let {id} be a formula defined by {body}
type_O1SetProp_exists_several=there exist formulas {id} such that
type_O1SetProp_exists_simple=there exists a formula {id} such that
type_O1SetProp_forall_several=for every formulas {id},
type_O1SetProp_forall_simple=for every formula {id},
type_O1SetProp_letin_several=
type_O1SetProp_letin_simple=
type_O1U_arg=universe
type_O1U_dec=Let {id} be an element
type_O1U_dec_body=Let {id} be the element {body}
type_O1U_exists_several=there exist element {id} such that
type_O1U_exists_simple=there exists an element {id} such that
type_O1U_forall_several=for every elements {id},
type_O1U_forall_simple=for every element {id},
type_O1U_letin_several=
type_O1U_letin_simple=
type_O1U_sci_arg=universe
type_O1U_sci_dec=Let {id} be an element
type_O1U_sci_dec_body=Let {id}={body}
type_O1U_sci_exists_several=∃ {id},
type_O1U_sci_exists_simple=∃ {id},
type_O1U_sci_forall_several=∀ {id},
type_O1U_sci_forall_simple=∀ {id},
type_O1U_sci_letin_several=
type_O1U_sci_letin_simple=
type_PHITYPE_arg=
type_PHITYPE_dec=
type_PHITYPE_dec_body=
type_PHITYPE_exists_several=
type_PHITYPE_exists_simple=
type_PHITYPE_forall_several=
type_PHITYPE_forall_simple=
type_PHITYPE_letin_several=
type_PHITYPE_letin_simple={id} is the function from ℘({2}) to ℘({0})×℘({1}) defined by {body}
type_PHITYPE_sci_arg=
type_PHITYPE_sci_dec=
type_PHITYPE_sci_dec_body=Let {id} : ℘({2})→℘({0})×℘({1}) defined by {body}
type_PHITYPE_sci_exists_several=
type_PHITYPE_sci_exists_simple=
type_PHITYPE_sci_forall_several=
type_PHITYPE_sci_forall_simple=
type_PHITYPE_sci_letin_several=
type_PHITYPE_sci_letin_simple={id} : ℘({2})→℘({0})×℘({1}) defined by {body}
type_Point_arg=point
type_Point_dec=Let {id} be a point
type_Point_dec_body=Let {id} be a point defined by {body}
type_Point_exists_several=there exist points {id} such that
type_Point_exists_simple=there exists a point {id} such that
type_Point_forall_several=for every points {id},
type_Point_forall_simple=for every point {id},
type_Point_letin_several=
type_Point_letin_simple=
type_Prop_arg=proposition
type_Prop_dec=Let {id} be a proposition
type_Prop_dec_body=Let {id} be a proposition defined by {body}
type_Prop_exists_several=there exist propositions {id} such that
type_Prop_exists_simple=there exist a proposition {id} such that
type_Prop_forall_several=for every propositions {id},
type_Prop_forall_simple=for every proposition {id},
type_Prop_letin_several=
type_Prop_letin_simple=
type_Rel_arg=({2}×{3})
type_Rel_dec=Let {id} be a relation on {2}×{3}
type_Rel_dec_body=Let {id} be a relation on {2}×{3} defined by {body}
type_Rel_exists_several=there exist relations {id} on {2}×{3} such that
type_Rel_exists_simple=there exists a relation {id} on {2}×{3} such that
type_Rel_forall_several=for every relations {id} on {2}×{3},
type_Rel_forall_simple=for every relation {id} on {2}×{3},
type_Rel_letin_several=
type_Rel_letin_simple=
type_Rel_sci_arg=({2}×{3})
type_Rel_sci_dec=Let {id} ⊆ {2}×{3}
type_Rel_sci_dec_body=Let {id} be a relation on {2}×{3} defined by {body}
type_Rel_sci_exists_several=∃ {cartesian_id} ⊆ {cartesian_type},
type_Rel_sci_exists_simple=∃ {id} ⊆ {2}×{3},
type_Rel_sci_forall_several=∀ {cartesian_id} ⊆ {cartesian_type},
type_Rel_sci_forall_simple=∀ {id} ⊆ {2}×{3},
type_Rel_sci_letin_several=
type_Rel_sci_letin_simple=
type_Series_arg=series
type_Series_dec=Let {id} be a series
type_Series_dec_body=Let {id} be a series defined on {0} by {body} {dom_serie}
type_Series_exists_several=there exist series {id} such that
type_Series_exists_simple=there exists a series {id} such that
type_Series_forall_several=for very series {id},
type_Series_forall_simple=for every series {id},
type_Series_letin_several=
type_Series_letin_simple={id} be a series defined on {0} by {body}
type_SetProp2_arg=
type_SetProp2_dec=Let {id} be a proposition on {0}
type_SetProp2_dec_body=
type_SetProp2_exists_several=
type_SetProp2_exists_simple=
type_SetProp2_forall_several=for every propositions {id} on {0},
type_SetProp2_forall_simple=for every proposition {id} on {0},
type_SetProp2_letin_several=
type_SetProp2_letin_simple=
type_SetProp2_sci_arg=
type_SetProp2_sci_dec=Let {id} be a proposition on {0}
type_SetProp2_sci_dec_body=
type_SetProp2_sci_exists_several=
type_SetProp2_sci_exists_simple=
type_SetProp2_sci_forall_several=for every propositions {id} on {0},
type_SetProp2_sci_forall_simple=for every proposition {id} on {0},
type_SetProp2_sci_letin_several=
type_SetProp2_sci_letin_simple=
type_SetProp_arg=
type_SetProp_dec=Let {id} be a proposition on {0}
type_SetProp_dec_body=
type_SetProp_exists_several=
type_SetProp_exists_simple=
type_SetProp_forall_several=for every propositions {id} on {0},
type_SetProp_forall_simple=for every proposition {id} on {0},
type_SetProp_letin_several=
type_SetProp_letin_simple=
type_UA_arg=A
type_UA_dec=Let {type} {id}
type_UA_dec_body=Let {type} {id} = {body}
type_UA_exists_several=∃ {id} {math:∊} {cartesian_type},
type_UA_exists_simple=∃ {id} {math:∊} {type},
type_UA_forall_several=∀ {id} {math:∊} {cartesian_type},
type_UA_forall_simple=∀ {id} {math:∊} {type},
type_UA_letin_several=
type_UA_letin_simple=
type_UA_sci_arg=A
type_UA_sci_dec=Let {id} {math:∊} A
type_UA_sci_dec_body=Let {id} = {body}
type_UA_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_UA_sci_exists_simple=∃ {id} {math:∊} {type},
type_UA_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_UA_sci_forall_simple=∀ {id} {math:∊} {type},
type_UA_sci_letin_several=
type_UA_sci_letin_simple=
type_UB_arg=B
type_UB_dec=Let {type} {id}
type_UB_dec_body=Let {type} {id} = {body}
type_UB_exists_several=∃ {id} {math:∊} {cartesian_type},
type_UB_exists_simple=∃ {id} {math:∊} {type},
type_UB_forall_several=∀ {id} {math:∊} {cartesian_type},
type_UB_forall_simple=∀ {id} {math:∊} {type},
type_UB_letin_several=
type_UB_letin_simple=
type_UB_sci_arg=B
type_UB_sci_dec=Let {id} {math:∊} B
type_UB_sci_dec_body=Let {id} = {body}
type_UB_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_UB_sci_exists_simple=∃ {id} {math:∊} {type},
type_UB_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_UB_sci_forall_simple=∀ {id} {math:∊} {type},
type_UB_sci_letin_several=
type_UB_sci_letin_simple=
type_UC_arg=C
type_UC_dec=Let {type} {id}
type_UC_dec_body=Let {type} {id} = {body}
type_UC_exists_several=∃ {id} {math:∊} {cartesian_type},
type_UC_exists_simple=∃ {id} {math:∊} {type},
type_UC_forall_several=∀ {id} {math:∊} {cartesian_type},
type_UC_forall_simple=∀ {id} {math:∊} {type},
type_UC_letin_several=
type_UC_letin_simple=
type_UC_sci_arg=C
type_UC_sci_dec=Let {id} {math:∊} C
type_UC_sci_dec_body=Let {id} = {body}
type_UC_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_UC_sci_exists_simple=∃ {id} {math:∊} {type},
type_UC_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_UC_sci_forall_simple=∀ {id} {math:∊} {type},
type_UC_sci_letin_several=
type_UC_sci_letin_simple=
type_UE_arg=E
type_UE_dec=Let {type} {id}
type_UE_dec_body=Let {type} {id} = {body}
type_UE_exists_several=∃ {id} {math:∊} {cartesian_type},
type_UE_exists_simple=∃ {id} {math:∊} {type},
type_UE_forall_several=∀ {id} {math:∊} {cartesian_type},
type_UE_forall_simple=∀ {id} {math:∊} {type},
type_UE_letin_several=
type_UE_letin_simple=
type_UE_sci_arg=E
type_UE_sci_dec=Let {id} {math:∊} E
type_UE_sci_dec_body=Let {id} = {body}
type_UE_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_UE_sci_exists_simple=∃ {id} {math:∊} {type},
type_UE_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_UE_sci_forall_simple=∀ {id} {math:∊} {type},
type_UE_sci_letin_several=
type_UE_sci_letin_simple=
type_U_arg={id}
type_U_dec=Let {type} {id}
type_U_dec_body=Let {type} {id} = {body}
type_U_exists_several=∃ {id} {math:∊} {cartesian_type},
type_U_exists_simple=∃ {id} {math:∊} {type},
type_U_forall_several=∀ {id} {math:∊} {cartesian_type},
type_U_forall_simple=∀ {id} {math:∊} {type},
type_U_letin_several=
type_U_letin_simple=
type_U_sci_arg={id}
type_U_sci_dec=Let {id} {math:∊} {type}
type_U_sci_dec_body=Let {id} = {body}
type_U_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_U_sci_exists_simple=∃ {id} {math:∊} {type},
type_U_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_U_sci_forall_simple=∀ {id} {math:∊} {type},
type_U_sci_letin_several=
type_U_sci_letin_simple=
type_Universe_arg=universe
type_Universe_dec=Let {id} be a universe
type_Universe_dec_body=Let {id} be a universe defined by {body}
type_Universe_exists_several=there exists universes {id} such that
type_Universe_exists_simple=there exists a universe {id} such that
type_Universe_forall_several=for every universes {id},
type_Universe_forall_simple=for every universe {id},
type_Universe_letin_several=
type_Universe_letin_simple=
type_WearingHat_arg=hat wearer
type_WearingHat_dec=Let {id} be a hat wearer
type_WearingHat_dec_body=
type_WearingHat_exists_several=there exist hat wearers {id} such that,
type_WearingHat_exists_simple=there exists a hat carrier {id} such that,
type_WearingHat_forall_several=for  every hat wearers {id},
type_WearingHat_forall_simple=for every hat wearer {id},
type_WearingHat_letin_several=
type_WearingHat_letin_simple=
type_gbmember_arg=islander
type_gbmember_dec=Let {id} be an islander
type_gbmember_dec_body=
type_gbmember_exists_several=there exists islanders {id} such that
type_gbmember_exists_simple=there exists an islander {id} such that
type_gbmember_forall_several=for every islanders {id},
type_gbmember_forall_simple=for every islander {id},
type_gbmember_letin_several=
type_gbmember_letin_simple=
type_gbmember_sci_arg=islander
type_gbmember_sci_dec=Let {id} be an islander
type_gbmember_sci_dec_body=
type_gbmember_sci_exists_several=there exists islanders {id} such that
type_gbmember_sci_exists_simple=there exists an islander {id} such that
type_gbmember_sci_forall_several=for every islanders {id},
type_gbmember_sci_forall_simple=for every islander {id},
type_gbmember_sci_letin_several=
type_gbmember_sci_letin_simple=
type_type_default_arg={id}
type_type_default_dec=Let {type} {id}
type_type_default_dec_body=Let {type} {id} = {body}
type_type_default_exists_several=∃ {id} {math:∊} {cartesian_type},
type_type_default_exists_simple=∃ {id} {math:∊} {type},
type_type_default_forall_several=∀ {id} {math:∊} {cartesian_type},
type_type_default_forall_simple=∀ {id} {math:∊} {type},
type_type_default_letin_several=
type_type_default_letin_simple=
type_type_default_sci_arg={id}
type_type_default_sci_dec=Let {id} {math:∊} {type}
type_type_default_sci_dec_body=Let {id} = {body}
type_type_default_sci_exists_several=∃ {pair_id} {math:∊} {cartesian_type},
type_type_default_sci_exists_simple=∃ {id} {math:∊} {type},
type_type_default_sci_forall_several=∀ {pair_id} {math:∊} {cartesian_type},
type_type_default_sci_forall_simple=∀ {id} {math:∊} {type},
type_type_default_sci_letin_several=
type_type_default_sci_letin_simple=