La règle conjI divise une conjonction comme suit :
show "A ^ B ^ C ^ D"
proof(rule conjI)
show "A" sorry
next
show "C ^ D" sorry"Existe-t-il une règle qui divise tous les termes reliés par la conjonction ? Certains comme :
show "A ^ B ^ C ^ D"
proof(rule ?)
show "A" sorry
next
show "C" sorry"
next
show "D" sorry"Vous ne pouvez pas faire cela avec une seule application de règle, mais vous pouvez faire intro conjI pour l'appliquer de manière exhaustive.
Il y a aussi la méthode safe qui fait une variété de choses comme cela (diviser les produits, appliquer les règles d'introduction/élimination appropriées, etc.)
Prograide est une communauté de développeurs qui cherche à élargir la connaissance de la programmation au-delà de l'anglais.
Pour cela nous avons les plus grands doutes résolus en français et vous pouvez aussi poser vos propres questions ou résoudre celles des autres.
