Maths Discrètes Licence 1 --- Introduction ---

Ce module regroupe 402 exercices à destination des étudiants de première année du portail Sciences Fondamentales de l'Université de Nice Sophia Antipolis


1 Evaluer (deux quantif. réels) le vrai

Calculer :


1 Evaluer (deux quantif. réels) vrai V29

Calculer :


1 Evaluer (table de vérité) backup

Ecrire la table de vérité de

B
V
F
A
V
F

1 Evaluer (table de vérité) V20? backup

Ecrire la table de vérité de

B
V
F
A
V
F

1 NewNier finit positive backup

Ici est une fonction. Nier :


1 NewNier finit positive vrai

Ici est une fonction. Nier :


1 Traduire (fonctions) V60? backup

(Choisissez -- si l'énoncé ne dit rien.)


2 Evaluer suites II

Dites si l'énoncé suivant est vrai ou faux

.


2 Evaluer suites II exam

Dites si l'énoncé suivant est vrai ou faux

.


2 Formaliser CNCS(nb) V30? backup


2 Formaliser CNCS(nb) V30?backup


2 Formaliser CNCS(nb) V30?exam

Au choix, on privilégiera l'ordre alphabétique.

444 Carré de majorée


444 Constante implique majorée


444 Double de surjective


444 Cinq gratuites

Donner une liste de cinq tactiques gratuites qui s'applique au but suivant [on fera le minimum au contexte pour pouvoir agir au but, on sautera les explicitations, et s'il reste du choix on privilégiera l'ordre alphabétique des tactiques]

Si une suite finit arithmétique ses multiples aussi


444 Cinq gratuites rapides

Donner une liste de cinq tactiques gratuites qui s'applique au but suivant [on fera le minimum au contexte pour pouvoir agir au but, on sautera les explicitations, et s'il reste du choix on privilégiera l'ordre alphabétique des tactiques]

La somme de deux suites qui finissent constantes finit constante


444 Constante implique bornée


444 Opposée de Cauchy


444 valabs majorée implique bornée


444 Double de constante backup


444 Double de constante vrai


444 Double de surjective backup


444 Maximum de constante


444 Maximum de constante backup


444 Nb de var

On essaie de prouver l'énoncé :

Toute fonction dont le carré est majoré est elle-même majorée

en appliquant autant que possible les tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables libres?


444 Nb de var 2

On essaie de prouver l'énoncé :

Si une fonction est majorée il en est de même pour tous ses multiples

en appliquant autant que possible les tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables libres?


444 Nb de var 3

On essaie de prouver l'énoncé :

Si une fonction est monotone il en est de même pour tous ses multiples

en appliquant autant que possible les tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables libres?


444 Nb de var 4

On essaie de prouver l'énoncé :

Toute combinaison linéaire de deux fonctions bornées est bornée

en appliquant autant que possible les six tactiques gratuites EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables?


444 Qui atteint ses bornes est majorée


4 Opposée de surjective


test2 Affine et surjective


test1 tacgrat6


444 Affine et injective


test2 Double de constante exam


test2 Associativité de la réunion

Donner les premières tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


test1 tacgrat5


644 constante et affine


644 finit affine et multiples


644 finit periodique et multiples


644 finit surjective et surjective


644 finit surjective pas injective


744 BBconstante implique majorée


744 Carré de majorée 1


744 Double de bconstante


744 Double de finit surjective


744 Maximum de bconstante


745 BBconstante implique CCconstante


745 constante implique BBconstante


AAAABmax_des partiest

Voici un énoncé suivi d'un début de preuve en étapes:
Toute partie non-vide et majorée de admet un plus grand élément.

Preuve. 1- On montre par récurrence sur n que toute partie P de non-vide et majorée par n admet un plus grand élément.

2- Si n est nul, alors le maximum de P est O.

3- Soit maintenant P une partie non-vide et majorée par n+1. Si n+1 est dans P, c'en est forcément le plus grand élément.

4- Si au contraire n+1 n'est pas dans P, l'hypothèse de récurrence s'applique: en effet, dans ce cas, P est en fait majoré par n.


Avec les blocs proposés ci-dessous, formez la liste de tactiques proposées par cette preuve (à l'exclusion de celles qui traitent les buts sur lesquels la preuve est muette).


AAAA Croissance du Max 5

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AAAAFVImageRecInter


AAAAImMonot3t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AAAA L'intersection est commutative


Donner les tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


AAAATac convergente plus stationnaire


AAAAYG Associativité de la réunion

Donner les premières tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


2 Evaluer (fonctions) V50?

Dites si l'énoncé suivant est vrai ou faux


Privilégier le contexte entrainement


AA Croissance de l'intersec Tac


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


AA Intersection idem


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


AA Monotonie complementaire Tac


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].

Aide: La 10. tactique est Contrapos.


AA Reunion idem


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


Témoigner (fonctions) V15

essaie de prouver l'énoncé
.
Il a appliqué la liste suivante de tactiques avec les variables et arguments indiqués.

Pourra-t-il s'en sortir ?


AA vide absorbant


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


AA vide neutre2


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


XC Définir croissance fonctions V 4


AE0


AE1

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AE2

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AE3

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AE4

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AE5

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


A Evaluer (deux quantif. réels) 1

Calculer :


Evaluer (deux quantif. réels) V30?

Calculer :


Evaluer (deux quantificateurs entiers) V

Calculer :


Evaluer (fonctions) V3

Dites si l'énoncé suivant est vrai ou faux


Evaluer réels ou complexes v5


Evaluer (sans quantificateur) V25?

Calculer :


Formaliser CNCS(nb) V30?


Formaliser fonctions I V2

Formalisez l'énoncé : .


Formaliser fonctions II V2

Formalisez l'énoncé : .


Formaliser (nb nonamb) V12?


XC Inférer le contexte (fonctions) V3


Témoigner meilleur temooin

Dans le contexte

,

Bob s'attaque au but

,

Il propose la tactique ExistB. Parmi ceux que Bob envisage, quel est le meilleur témoin?


Témoin choisir le bon

Bob essaie de prouver l'énoncé

Pour qu'une fonction soit majorée il suffit que son double le soit.

Il a appliqué la liste suivante de tactiques avec les variables et arguments indiqués.

ForallB [f] ImpB ReecC ExistC[M] ReecB

Il va maintenant appliquer ExistB et il hésite pour le témoin. Quel est le bon choix?


XC Variables libres (formules) V30

Dans la formule suivante, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


XC Variables libres (Enoncés) V30

Dans l'énoncé suivant, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


Formaliser CNCS(nb) V30?


Formaliser (nb nonamb) V12?


AH Cinq tactiques


AH Huit tactiques fonctions


AH ImRecDiff0


AH ImRecDiff1g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff1t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff2g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff2t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff3g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff3t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff4g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff4t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff5g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff5t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH ImRecDiff6t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


AH Infos

Les exercices suivants concerne la différence, qui est une opération sur les parties d'un ensemble, comme l'intersection et la réunion.

Si P et Q sont deux parties de l'ensemble X, la différence P-Q est constituée des éléments de X qui sont dans P mais pas dans Q.

Par exemple pour X :=R, P := [1,3] et Q := [2, 6], on a P-Q = [1, 2[ et Q-P = ]3, 6].

La règle de réécriture correspondante est donc

Par ailleurs, notez que les buts intermédiaires sont mieux payés (poids 3) que les tactiques. Traîtez-les donc avec le plus grand soin. Aussi, si vous vous trompez sur les buts intermédiaires, wims vous les donne: notez-les soigneusement pour la suite.

Pour sortir de cet "exo", tapez ok, si vous préférez le vert.


AH Preuves fonctions, 6,7,8


AH Privilégier le contexte memes tac


AH Six tactiques SuiteEtFin


2 Evaluer réels ou complexes v55


Typer (réels ou complexes) V20


Evaluer (table de vérité) secours

Ecrire la table de vérité de

B
V
F
A
V
F

Evaluer (deux quantificateurs entiers) V

Calculer :


Evaluer (deux quantif. réels) V30?

Calculer :


1 Evaluer (fonctions) V50

Dites si l'énoncé suivant est vrai ou faux

.


Evaluer réels ou complexes v50?


Evaluer (sans quantificateur) V25?

Calculer :


Evaluer (table de vérité) V20?

Ecrire la table de vérité de

B
V
F
A
V
F

Evaluer (table de vérité) secours

Ecrire la table de vérité de

B
V
F
A
V
F

Tac 5 Finit V25


2 Formaliser CNCS(nb) V30?


Formaliser fonctions I

Formalisez l'énoncé : .


2 Formaliser fonctions genre majorées V

Formalisez l'énoncé : .


Formaliser (nb nonamb) V12?


XC Inférer le contexte (fonctions) V7


Témoigner x ou 2y

Dans le contexte

Bob s'attaque au but

Il propose la tactique ExistB avec pour témoin

Pourra-t-il s'en sortir? (y/n)


Témoigner (fonctions) test

Bob essaie de prouver l'énoncé

.

Il a appliqué la liste suivante de tactiques avec les variables et arguments indiqués.

Peut-il encore s'en sortir? (y/n)


Variables libres (énoncés) V30

Dans l'énoncé suivant, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


Variables libres (formules) V30

Dans l'énoncé suivant, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


Archimède 1

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :

Preuve. ...


Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par ce début de preuve. On mettra Facile pour traîter chaque séquent pour lequel la preuve fournie ne donne aucune indication.


YH L'intersection est commutative bis


Donner les tactiques qu'il vous faut exécuter pour prouver

.


Archimède 3

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de sa preuve :

Preuve.

Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par cette dernière phrase de la preuve. On mettre Facile pour traîter chaque séquent pour lequel la preuve fournie ne donne aucune indication.


BL Croissance du Max 0


BL Croissance du Max 1

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


BL Croissance du Max 2

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


BL Croissance du Max 3

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


BL Croissance du Max 4

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


BL Croissance du Max 5

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


BMaxCroissantAlpha

Voici un énoncé:
Si P et Q sont deux parties non-vides et majorées de avec P contenue dans Q alors on a max P max Q.


Et le début de "preuve" de Bob:
Ress, Ress, ForallB, ForallB, ImpB, EtC, EtC, EtC, EtC, ReecC, ForallC, EtC, ForallC, EtC, ForallC, ImpC
Bob s'est presque sûrement trompé et en plus il a oublié de privilégier l'ordre alphabétique. Avec les blocs proposés ci-dessous, remettez dans l'ordre la partie correcte de sa preuve.


BMaxCroissantBob

Voici un énoncé:
Si P et Q sont deux parties non-vides et majorées de avec P contenue dans Q alors on a max P max Q.


Et le début de "preuve" de Bob:
Ress, Ress, ForallB, ForallB, ImpB, EtC, EtC, EtC, EtC, ReecC, ForallC, EtC, ForallC, EtC, ForallC, ImpC
Bob s'est presque sûrement trompé. Avec les blocs proposés ci-dessous, recopiez la partie correcte de sa preuve.


BMaxReu

Voici un énoncé:
Le maximum de la réunion de deux parties non-vides et majorées de est le plus grand des deux maxima.


Et le début de "preuve" de Bob:
Ress, Ress, ForallB, ForallB, ImpB, EtC, EtC, EtC, ReecC, ReecC, ReecC, ReecC, ForallC, ForallC, EtC, EtC, ReecB
Bob s'est peut-être trompé et en plus il a oublié de privilégier l'ordre alphabétique. Avec les blocs proposés ci-dessous, remettez dans l'ordre la partie correcte de sa preuve.


Bmax_des partiesg

Voici un énoncé suivi d'un début de preuve en étapes:
Toute partie non-vide et majorée de admet un plus grand élément.

Preuve. 1- On montre par récurrence sur n que toute partie P de non-vide et majorée par n admet un plus grand élément.

2- Si n est nul, alors 0 est le plus grand élément de P.

3- Soit maintenant P une partie non-vide et majorée par n+1. Si n+1 est dans P, c'en est forcément le plus grand élément.

4- Si au contraire n+1 n'est pas dans P, alors P est en fait majoré par n et l'hypothèse de récurrence s'applique.


Avec les blocs proposés ci-dessous, formez le but intermédiaire


Bmax_des partiest

Voici un énoncé suivi d'un début de preuve en étapes:
Toute partie non-vide et majorée de admet un plus grand élément.

Preuve. 1- On montre par récurrence sur n que toute partie P de non-vide et majorée par n admet un plus grand élément.

2- Si n est nul, alors le maximum de P est O.

3- Soit maintenant P une partie non-vide et majorée par n+1. Si n+1 est dans P, c'en est forcément le plus grand élément.

4- Si au contraire n+1 n'est pas dans P, l'hypothèse de récurrence s'applique: en effet, dans ce cas, P est en fait majoré par n.


Avec les blocs proposés ci-dessous, formez la liste de tactiques proposées par cette preuve (à l'exclusion de celles qui traitent les buts sur lesquels la preuve est muette).


Témoigner x2 et y

Dans le contexte
s'attaque au but
Il propose la tactique ExistB avec pour témoin

Pourra-t-il s'en sortir ?


XC Inférer le contexte (fonctions) V20


Croissante majorée 1

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.25), suivi de son début de preuve :

Preuve.


La deuxième phrase ci-dessus suggère une liste de tactiques dont vous devez donner seulement la première et la dernière.


Croissante majorée 1bis

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.25), suivi de son début de preuve :

Preuve.


La deuxième phrase ci-dessus suggère une liste de tactiques dont vous devez donner seulement les trois premières et les deux dernières (avec "..." après les trois premières)..


DQuestion 0


DQuestion 1


DQuestion 2


DQuestion 3


DQuestion 4


Début gratuit 1


1 Définition et négation (Xiao)

Soit une fonction réelle. Formalisez la propriété `` est ''. (Tirez les éléments pour composer votre formule)

La propriété `` est '' se formalise en

.

Quel est le contraire (négation) de cette propriété ?

Maintenant formalisez la négation `` n'est pas ''.

La négation `` n'est pas '' se formalise donc en

.

Donnez deux valeurs , pour montrer que la fonction ci-contre n'est pas , selon la formule. (Chaque case de la grille vaut 1 ; il faut donc choisir et entre -5 et 5.)


Densité 1

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
est dense dans

Preuve. Comme est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n...


Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par ce début de preuve. On privilégiera l'ordre alphabétique des tactiques.


Densité 1bis

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
est dense dans

Preuve. Comme est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n...


Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par ce début de preuve. On privilégiera l'ordre alphabétique des tactiques.


Densité2

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de son début de preuve :
est dense dans

Preuve. Comme est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n . Comme l’ensemble est minoré par 1 et contient n, il possède un minimum qu'on note p.


Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par la deuxième phrase de cette preuve. On privilégiera l'ordre alphabétique des tactiques.


Densité3

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.8), suivi de sa preuve :
est dense dans

Preuve. Comme est archimédien, il existe un entier q > 0 tel que 1/(y − x) < q ainsi qu’un entier n > 0 tel que qx < n . Comme l’ensemble est minoré par 1 et contient n, il possède un minimum qu'on note p. On a donc p − 1 ≤ qx < p de sorte que qx < p ≤ qx + 1 et x < p/q ≤ x + 1/q < y par la première inégalité.


La fin de la preuve est incorrecte. A partir de la liste des inégalités prétendues, formez la liste des inégalités prouvables . On les laissera dans l'ordre proposé ci-dessous.


1 Formaliser croissance fonctions V 4


EQuestion 0


EQuestion 1


EQuestion 2


EQuestion 3


EQuestion 4


EQuestion 5


1 Formaliser CNCScroissance fonctions V6


1 Evaluer (deux quantif. réels) V29

Calculer :


1 Evaluer (sans quantificateur) V28

Calculer :


1 Evaluer (deux quants entiers) V50

Calculer :


2 Evaluer suites II vieux

Dites si l'énoncé suivant est vrai ou faux

.


Tac 8 V22


Formaliser fonctions II

Formalisez l'énoncé : .


Formaliser fonctions I

Formalisez l'énoncé : .


Tac 8 fonctions V12


Tac 5 fini V17


Tac SuiteEtFin V12


XF Preuve guidée fonctions


2 Evaluer suites I

Dites si l'énoncé suivant est vrai ou faux

.


XC Formaliser suites V6

Formalisez l'énoncé : .


Former une CNouS mijo


Tac Composition graphes the old one


FT Applipart phrase 1


Tac convergente plus stationnaire


Tac stationnaire plus stationnaire


FT Tactiques finales


FT Objectifs finaux


FT Applipart la fin


FT Applipart phrase 2


FT Applipart phrase 3


FT Applipart phrase 1


FT Applipart phrase 1


FT Applipart phrase 1


FT Formaliser


FU Formaliser


FUReltot phrase 1


FUReltot phrase 2


FUReltot phrase 3


FVImageInter


FVImageInterGen


FVImageRecCompl


FVImageRecInter


FVImageRecReu


FVImageReu


FVRecip


FVRecip0


2 Définir nier majminbor fonctions V3x2

. Formalisez l'énoncé : .


1 Formaliser CNCS mijo fonctions V25


1 Traduire (fonctions) V60?

(Choisissez -- si l'énoncé ne dit rien.)


PreuveGen0


Définir inj V1

. Formalisez l'énoncé : .


2 Définir surj V4

. Formalisez l'énoncé : .


2 Définir pairimpperconst V4

. Formalisez l'énoncé : .


2 Former CS (suites mijo) V30


2 Former une CN mijo V50


ImInter2


ImInter3


ImInterDer

Voici maintenant l'énoncé suivi de sa preuve complète:

Preuve.


Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par le dernier alinéa de cette preuve.


ImMonot0


ImMonot1g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImMonot1t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImMonot2g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImMonot2t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImMonot3t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImRecCompl0


ImRecCompl1g

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecCompl2g

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecCompl2t

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecMonot2t

Voici le même énoncé suivi d'une preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecCompl3g

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecCompl3t

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecCompl4t

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecInter0


ImRecInter1


ImRecInter2


ImRecInter3


ImRecInterDer

Voici maintenant l'énoncé suivi de sa preuve complète:

Preuve.


Avec les blocs proposés ci-dessous, formez la liste de tactiques suggérée par le dernier alinéa de cette preuve.


ImRecMonot0


ImRecMonot1g

Voici le même énoncé suivi d'une preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


PreuveGen1t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImRecMonot1t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImRecMonot2g

Voici le même énoncé suivi d'une preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecMonot3t

Voici le même énoncé suivi d'une preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


ImRecMonotINV


ImReu0


ImReu1


ImReu2


ImReu3


ImReu4


ImReu5


ImInter0


ImInter1


La composée de deux fonctions dont l'une

Voici un énoncé :
La composée de deux fonctions dont l'une est constante est elle-même constante.
Vous devez concevoir un enchainement de tactiques prouvant cet énoncé, et donner le sous-enchaînement correspondant de tactiques Forall et Exist. Vous devez choisir une preuve conduisant à la réponse optimale du point de vue de l'ordre alphabétique inverse.


BMaxCroissantLibre

Voici un énoncé suivi d'un début de preuve:
Si P et Q sont deux parties non-vides et majorées de avec P contenue dans Q alors on a max P max Q.


Avec les blocs proposés ci-dessous, formez une preuve qui commence par invoquer deux fois la ressource.


Modele de preuve

Donner les tactiques de votre preuve du but suivant


PreuveGen2g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


PreuveGen2t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


PreuveGen4t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


PreuveGen3t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


PreuveGen5t

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


PreuveGen1g

Voici le même énoncé suivi en étapes:


Avec les blocs proposés ci-dessous, formez


ImRecCompl1t

Voici le même énoncé suivi d'un début de preuve en étapes:

Preuve.


Avec les blocs proposés ci-dessous, formez


PreuveParties AuB dans B

Donner les tactiques de votre preuve du but suivant


PreuveParties A dans AnB contexte vrai

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties AuB dans B au contexte

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties AuB dans B alpha

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties AuB dans B alphainv

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties AuB dans B grat

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties A dans AnB alpha

Donner les premières tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties A dans AnB alphainv

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties AuA dans BnB alpha

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties A dans AnB alpha vrai

Donner les tactiques de votre preuve du but suivant en sous-entendant les réécritures et


PreuveParties Bob1

Bob est un boulet. Il a cru trouver une preuve de

à savoir:

Recopier la partie de sa preuve qui est correcte.


PreuveParties Bob1

Bob est un boulet. Il a cru trouver une preuve de

à savoir:

Recopier la partie de sa preuve qui est correcte.


PreuveParties régularité

Donner les tactiques de votre preuve du but suivant


Privilégier le contexte tacdiff


Privilégier le contexte test


XC Traduire un énoncé formel (entiers) V


2 Traduire (intervalles) V30


Recip1


Recip2


Recip3


Recip4


Somme de Cauchy inverse vrai

Voici un énoncé qu'on aurait pu trouver sur le web, suivi de sa preuve :
La somme de deux suites de Cauchy est de Cauchy.

Preuve. Soient u et v deux suites de Cauchy. Nous savons qu'on a

et

.

On en déduit que, pour tout n et m , on a

,

ce qui prouve que u+v est de Cauchy.


Ce texte vous inspire diverses preuves qui diffèrent par l'ordre des tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement de 14 tactiques Forall et Exist dans l'une de ces variantes, en choisissant celle qui donne la réponse optimale pour l'ordre alphabétique INVERSE.


ZModele de mariages

Etablissez la correspondance entre les symboles et leurs sens ci-dess ous.


1 Evaluer (table de vérité) V20?

Ecrire la table de vérité de

B
V
F
A
V
F

XD Tac grat but 5 fini V17


Témoigner V20

Dans le contexte
s'attaque au but
Il propose la tactique ExistB avec pour témoin

Pourra-t-il s'en tirer?


ZModele paup QCM

Quelle est la traduction de l'énoncé suivant:

?


ZModele QCM

Quelle est la nature fonctionnelle de "" dans la phrase suivante?

.


Typer complexes pap V5


Typer fonctions pap V8


Typer parties V1


Typer réelscompl V8


Typer réels V5


Typer entiers pap V2


Variables libres (énoncés) V30

Dans l'énoncé suivant, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


Variables libres (formules) V30

Dans l'énoncé suivant, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


Variables libres texte V1

Dans le début de phrase suivant, identifier les variables libres.

(ATTENTION: Séparez vos variables par des virgules. Tapez VIDE si la liste de variables répondant à la question est vide. Le comparateur distingue les majuscules des minuscules.)


XC Définir finit constante

Ici est une fonction. En vous inspirant de

f finit nulle ssi         

définir:


XC Définir finit positive

Ici est une fonction. En vous inspirant de

f finit nulle ssi         

définir:


1 Nier finit positive

Ici est une fonction. Nier :


1 Nier finit constante

Ici est une fonction. Nier :


XD Début gratuit


XD Début gratuit but/contexte


XD Formaliser intervalles


XD Tac SuiteEtFin V12


XD Tac grat but courant

On commence la preuve de l'énoncé :

en appliquant autant que possible les sept tactiques gratuites ImpB EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, quel est le but courant?


XD tac grat nb var

On essaie de prouver l'énoncé :

en appliquant autant que possible les six tactiques gratuites EtC EtB OuB OuC ForallB ExistsC. Une fois que c'est fait, combien le contexte courant contient-il de variables?


XE 5tactiques Entrainement


XE 5tactiques test


XE Preuves Fonctions diverses Entrainem


XE Preuves Fonctions diverses Test


XE Tac 8 fonctions Entrainement


XE Tac 8 fonctions Test


XE Tac Entrainement


XE Tac Test


ZZ1 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


XG Newtactiques


XG NewDéfinir finit

Ici est une fonction. En vous inspirant de

f finit nulle ssi         

définir:


XG Newevaluer (table de vérité) V10

Ecrire la table de vérité de

B
V
F
A
V
F

XG NewFormaliser mijo


XG NewFormaliser croissances


1 NewNier finit positive

Ici est une fonction. Nier :


XG Tac 8 fonctions Entrainement


XG Tac A modifier 1


XG Tac A modifier 2


XG Tac A modifier 3


XG Tac Entrainement


XG Tac New8 fonctions Entrainement


XG Tac grat but 5 fini V17


XG NewTraduire f

(Choisissez -- si l'énoncé ne dit rien.)


XG NewTraduire


YEns Associativité de la réunion B

Donner une liste de tactiques qui commence la preuve de

[on agira d'abord et s'il reste du choix on privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].


YEns Associativité de la réunion C

Donner une liste de tactiques qui commence la preuve de

[on agira d'abord et s'il reste du choix on privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].


YEns Associativité de la réunion Alpha

Donner une liste de tactiques qui commence la preuve de

[On privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].


YEns Associativité de la réunion Antialp

Donner une liste de tactiques qui commence la preuve de

[On privilégiera l'ordre des tactiques; Attention, OuB désigne le Ou faible (non gratuit)].


YEns NbTacAlpha Associativité de la réun

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YEns NbTacAlpha Associativité de l'inter

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YEns NbTacAlpha Croissance de l'intersec

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YF NbTacAlphaIdempotence inter

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].


YF NbTacAlphaIdempotence reu

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].


YF NbTacAlpha Neutralité du vide

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].


YF NbTacAlpha vide absorbant

Vous avez commencé votre preuve de

par la liste de tactiques

.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve . Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp, VraiB, FauxC [Attention, OuB désigne le Ou faible (non gratuit)].


YG Associativité de la réunion

Donner les premières tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YG Commutativité de la réunion


Donner les 15 premières tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YG Commutativité de la réunion backup


Donner les 15 premières tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YH La réunion minore les majorants


Donner les tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YH L'intersection majore les minorants


Donner les tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YG Partie minimum


Donner les tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YG Reflexivité de l'inclusion


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


YG Transitivité de l'inclusion


Donner les tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YH L'intersection est commutative ter


Donner les tactiques qu'il vous faut exécuter pour prouver

.


YH L'intersection est commutative vrai


Donner les tactiques qu'il vous faut exécuter pour prouver

.
[Attention, OuB désigne le Ou faible (non gratuit)].


YH Monotonie complémentaire

Alice a commencé sa preuve de

par une liste de huit tactiques privilégiant l'action au but. Elle a ensuite fait une réécriture au contexte puis une contraposition.

Vous êtes donc confronté à un certain objectif courant et vous continuez cette preuve. Donner le nombre de tactiques qu'il vous faut exécuter pour venir à bout de cet objectif courant.

Les tactiques disponibles sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YH Une invocation


Vous commencez votre preuve de

par ForallB ImpB EtC EtC puis vous invoquez le théorème qui dit que l'image d'une fonction continue est un intervalle. Donnez la liste des trois tactiques que vous exécutez ensuite pour exploiter cette ressource..
[Attention, OuB désigne le Ou faible (non gratuit)].


YH Utilisation d'une limite


Vous commencez votre preuve de

par ForallB ImpB EtC EtC ForallB. Après ça, vous invoquez le théorème des valeurs intermédiaires d'où vous déduisez que l'image de votre fonction est un intervalle. Vous réécrivez alors l'hypothèse concernant la limite en . Donnez la liste des quatre tactiques que vous exécutez ensuite en vue d'exploiter cette hypothèse.
[Attention, OuB désigne le Ou faible (non gratuit)].


YH menage assoc inter

Alice propose à Bob une preuve de

conçue .

Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de tactiques proposées par Alice, Bob va-t-il accepter avant de faire du ménage?

Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YH menage commut inter nombre

Alice propose à Bob une preuve de

conçue .

Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de fois Bob va-t-il interrompre la preuve d'Alice pour faire du ménage?

Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YH menage commut inter rang

Alice propose à Bob une preuve de

conçue .

Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de tactiques d'Alice Bob va-t-il accepter avant de faire du ménage?

Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YH menage monot inter

Alice propose à Bob une preuve de

conçue .

Mais Bob ne supporte pas les hypothèses ou les variables inutiles. Combien de tactiques proposées par Alice Bob va-t-il accepter avant de faire du ménage?

Les tactiques utilisées par Alice sont: ForallB, ForallC, ReecB, ReecC, ExistB, ExistC, EtB, EtC, ImpB, ImpC, OuB, OuC, Hyp [Attention, OuB désigne le Ou faible (non gratuit)].


YK Composition d' injectives


Bob prouve

,

. Il exécute 16 tactiques et envisage de poursuivre avec ImpC. Mais Alice lui fait observer que, s'il veut s'en sortir, il doit d'abord faire autre chose. A quelle tactique pense-t-elle?


YK Composition de surjectives, nb de tac


Bob prouve

,

. Il exécute 11 tactiques et envisage de poursuivre avec ExistB. Mais Alice lui fait observer que, s'il veut s'en sortir, il doit d'abord faire autre chose. Combien de tactiques préconise-t-elle d'exécuter avant ExistB?


YK Composition de surjectives, coups de


Bob prouve

,

Il choisit la stratégie qui lui permet d'exécuter ExistB au plus vite. Sachant qu'il est pressé, combien de tactiques va-t-il exécuter après ExistB pour conclure?


YK Composition injective


Alice prouve

,

. Elle exécute 12 tactiques et envisage de poursuivre avec ImpC. Mais Bob lui fait observer que, si elle veut s'en sortir, elle doit d'abord faire autre chose. A quelle tactique pense-t-il?


YK Composition injective, but courant


Alice prouve

.

Elle exécute 12 tactiques et poursuit avec ImpB et ImpC. Ensuite elle effectue deux réécritures au but, et invoque Refl. Combien de tactiques lui faut-il pour venir à bout de son but courant?


YK Composition injective, coups de grâce


Alice prouve

.

Elle exécute 12 tactiques et poursuit avec ImpB et ImpC. Ensuite elle effectue deux réécritures au but, et invoque Refl. Combien de tactiques lui faut-il pour finir sa preuve?


YK Composition surjective, nb de tac


Bob prouve

.

. Il a exécuté 9 tactiques et envisage de poursuivre avec ExistB. Mais Alice lui fait observer que, s'il veut s'en sortir, il doit d'abord faire autre chose. Combien de tactiques préconise-t-elle d'exécuter maintenant avant ExistB?


YK Injections monos, but courant


Alice prouve

.

Elle exécute 15 tactiques et poursuit avec ImpC. Ensuite elle effectue deux réécritures au contexte. Combien de tactiques lui faut-il alors pour venir à bout de son but courant?


YK Injections monos, coups de grâce


Alice prouve

.

Elle exécute 16 tactiques . Ensuite elle effectue deux réécritures au contexte. Combien de tactiques lui faut-il alors pour venir à bout de sa preuve?


YK Surjections épis, nb de tac


Alice prouve

.

Combien de tactiques doit-elle exécuter avant de faire son deuxième ForallC?


YK Surjections épis, coups de grâce


Alice prouve

.

Elle a fait ses deux ForallC au plus vite. Elle fait ensuite les réécritures utiles. Combien de tactiques doit-elle exécuter après ces réécritures pour finir sa preuve?


ZX11 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZX13 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZX14 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZZ11 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZZ12 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZZ13 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZZ14 NewTraduire f

(Choisissez -- si l'énoncé est toujours vrai.)


ZZ1 Définition et négation (Xiao)

Soit une fonction réelle. Formalisez la propriété `` est ''. (Tirez les éléments pour composer votre formule)

La propriété `` est '' se formalise en

.

Quel est le contraire (négation) de cette propriété ?

Maintenant formalisez la négation `` n'est pas ''.

La négation `` n'est pas '' se formalise donc en

.

Donnez deux valeurs , pour montrer que la fonction ci-contre n'est pas , selon la formule. (Chaque case de la grille vaut 1 ; il faut donc choisir et entre -5 et 5.)


ZZ2' NewTraduire interv


ZZ2 Traduire (intervalles) V30


ZZ3 Définir finit positive

Ici est une fonction. En vous inspirant de

f finit nulle ssi         

définir:

f commence négative


1 Nier finit positive

Ici est une fonction. Nier :

f commence négative


ZZ5 Formaliser intervalles


ZZ6


Donner une liste de six tactiques gratuites qui s'applique au but suivant [on sautera les explicitations. Au choix, on agira d'abord au contexte; et s'il reste du choix on privilégiera l'ordre alphabétique des tactiques]

Si une fonction finit affine ses multiples aussi.


ZZ7 New5tactiques


ZZ8 Tac New8 fonctions Entrainement


ZZ91 vide absorbant


Donner les tactiques qu'il vous faut exécuter pour prouver

.

[Attention, OuB désigne le Ou faible (non gratuit)].


ZZ92 ImRecInter0


ZZ92 ImRecInter1


ZZ92 ImRecInter2


ZZ92 ImRecInter3


ZZ92 ImRecInterDer

Voici maintenant l'énoncé suivi de sa preuve complète:

Preuve.


Avec les blocs proposés ci-dessous, formez la liste de 12 tactiques suggérée par le dernier alinéa de cette preuve.


ZZ92 ImRecInter0 vrai


ZZ92 ImRecInter1 vrai


ZZ9

Donner les 23 tactiques de votre preuve du but suivant en retardant au maximum les réécritures et en privilégiant les autres actions au but


ZSteps générique


Somme de Cauchy chaos

Voici un énoncé qu'on aurait pu trouver sur le web, suivi de sa preuve :
La somme de deux suites de Cauchy est de Cauchy.

Preuve. Soient u et v deux suites de Cauchy. Nous savons qu'on a

et

.

On en déduit que, pour tout n et m , on a

,

ce qui prouve que u+v est de Cauchy.


Ce texte vous inspire diverses preuves qui diffèrent par l'ordre des tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement de 14 tactiques Forall et Exist dans l'une de ces variantes, en choisissant celle qui donne la réponse optimale pour l'ordre privilégiant ExistC devant ForallC, devant ForallB, devant ExistB.

ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!

ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!

ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!

ATTENTION: les tactiques ne sont pas proposées dans cet ordre!!!!!!


Somme de Cauchy direct

Voici un énoncé qu'on aurait pu trouver sur le web, suivi de sa preuve :
La somme de deux suites de Cauchy est de Cauchy.

Preuve. Soient u et v deux suites de Cauchy. Nous savons qu'on a

et

.

On en déduit que, pour tout n et m , on a

,

ce qui prouve que u+v est de Cauchy.


Cette preuve vous inspire un enchainement de tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement correspondant de 14 tactiques Forall et Exist. On respectera l'ordre suggéré par la preuve et, au choix, on privilégiera l'ordre alphabétique.


convergence vers Cauchy au but

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy.

Preuve. Soit u une suite convergente et soit sa limite. Nous savons que . On en déduit que, pour tout n et m ,

. ce qui prouve que u est de Cauchy.


Cette preuve vous inspire un enchainement de tactiques. Modifiez cet enchainement de façon a privilégier l'action au but. Puis, avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist.


convergence vers Cauchy antialpha

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy.

Preuve. Soit u une suite convergente et soit sa limite. Nous savons que . On en déduit que, pour tout n et m ,

. ce qui prouve que u est de Cauchy.


Vous devez concevoir un enchainement de tactiques prouvant cet énoncé, et donner le sous-enchaînement correspondant de tactiques Forall et Exist. Vous devez choisir une preuve conduisant à la réponse optimale du point de vue de l'ordre alphabétique inverse.


convergence vers Cauchy direct vrai

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy.

Preuve. Soit u une suite convergente et soit sa limite. Nous savons que . On en déduit que, pour tout n et m ,

. ce qui prouve que u est de Cauchy.


Cette preuve vous inspire un enchainement de tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist. On respectera l'ordre suggéré par la preuve et, dans le doute, on privilégiera l'ordre alphabétique.


convergence vers Cauchy inverse vrai

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy.

Preuve. Soit u une suite convergente et soit sa limite. Nous savons que . On en déduit que, pour tout n et m ,

. ce qui prouve que u est de Cauchy.


Cette preuve vous inspire un enchainement de tactiques. Avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist. On respectera l'ordre suggéré par la preuve et, dans le doute, on privilégiera l'ordre alphabétique inverse.


convergence vers Cauchy au but vrai

Voici un énoncé trouvé sur le web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45), suivi de sa preuve :
Toute suite convergente est de Cauchy.

Preuve. Soit u une suite convergente et soit sa limite. Nous savons que . On en déduit que, pour tout n et m ,

. ce qui prouve que u est de Cauchy.


Cette preuve vous inspire un enchainement de tactiques. Modifiez cet enchainement de façon a privilégier l'action au but. Puis, avec les blocs ci-dessous, formez le sous-enchaînement correspondant de tactiques Forall et Exist.


Cette page n'est pas dans son apparence habituelle parce que WIMS n'a pas pu reconnaître votre navigateur web.
Afin de tester le navigateur que vous utilisez, veuillez taper le mot wims ici : puis appuyez sur ``Entrer''.

Veuillez noter que les pages WIMS sont générées interactivement; elles ne sont pas des fichiers HTML ordinaires. Elles doivent être utilisées interactivement EN LIGNE. Il est inutile pour vous de les ramasser par un programme robot.