" x,y,z· x<yÙ y<zÞ x<z | |
Ù | " x,y· x<yÞ$ z· P(x,z)Ù¬ P(y,z) |
Ù | " x·$ y· x<y |
" x1· ... " xn· " y1· ... " yn· |
x1= y1 Ù ... Ù xn= yn Þ f(x1,...,xn)= f(y1,...,yn) |
" x1· ... " xn· " y1· ... " yn· |
x1= y1 Ù ... Ù xn= yn Ù P(x1,...,xn)Þ P(y1,...,yn) |
" x· 0+x= xÙ x= x+0 | (0 est élément neutre) |
" x· " y· " z· x+(y+z)= (x+y)+z | (associativité) |
" x·$ y· x+y= 0Ù y+x= 0 | (inverse) |
" x· " y· x+y= y+x | (commutativité de +) |
" x· 1*x= xÙ x= x*1 | (1 est neutre pour *) |
" x· " y· " z· x*(y*z)= (x*y)*z | (associativité) |
" x·" y·" z· x*(y+z)= x*y+x*z | |
" x·" y·" z· (y+z)*x= y*x+z*x | (distributivité) |
" x,y· x= yÞ s(x)= s(y) |
" x,y,z,t· x= zÙ y= tÞ x+y= z+t |
" x,y,z,t· x= zÙ y= tÞ x*y= z*t |
" x,y,z,t· x= zÙ y= tÙ x£ yÞ z£ t |