Fitch proof exercise: showing $(lnot forall x ; P(x)) leftrightarrow (exists x lnot P(x))$
$begingroup$
I have got a Problem with the following fitch proof excercise:
$quad;; |$
$triangleright quad | quad ?. quad (lnot forall x ; P(x)) leftrightarrow (exists x lnot P(x))$
This is how far I got: (Notice: I started from the bottom to the top!)
My problem is, that I can't find a way how to contradict $P(c)$. My first idea was, to proof $forall x ; P(x)$ in the subproof in order to get a contradiction.
As you can see, this is only the first part of the proof. I know that I will have to use a Biconditional introduction in the end. I only need help for the first subproof.
Would be great if anyone could give me some hints.
logic first-order-logic predicate-logic
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
asked Jan 5 at 12:17
JenewJenew
112
$endgroup$
add a comment |
$begingroup$
I have got a Problem with the following fitch proof excercise:
$quad;; |$
$triangleright quad | quad ?. quad (lnot forall x ; P(x)) leftrightarrow (exists x lnot P(x))$
This is how far I got: (Notice: I started from the bottom to the top!)
My problem is, that I can't find a way how to contradict $P(c)$. My first idea was, to proof $forall x ; P(x)$ in the subproof in order to get a contradiction.
As you can see, this is only the first part of the proof. I know that I will have to use a Biconditional introduction in the end. I only need help for the first subproof.
Would be great if anyone could give me some hints.
logic first-order-logic predicate-logic
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
asked Jan 5 at 12:17
JenewJenew
112
$endgroup$
$begingroup$
Welcome to math stackexchange. I have tidied up your question -- we like it when titles are very specific! I hope you find the answers helpful.
$endgroup$
– 6005
Jan 5 at 13:02
$begingroup$
Thank you very much. I will do better next time ;).
$endgroup$
– Jenew
Jan 5 at 13:10
add a comment |
$begingroup$
I have got a Problem with the following fitch proof excercise:
$quad;; |$
$triangleright quad | quad ?. quad (lnot forall x ; P(x)) leftrightarrow (exists x lnot P(x))$
This is how far I got: (Notice: I started from the bottom to the top!)
My problem is, that I can't find a way how to contradict $P(c)$. My first idea was, to proof $forall x ; P(x)$ in the subproof in order to get a contradiction.
As you can see, this is only the first part of the proof. I know that I will have to use a Biconditional introduction in the end. I only need help for the first subproof.
Would be great if anyone could give me some hints.
logic first-order-logic predicate-logic
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
asked Jan 5 at 12:17
JenewJenew
112
$endgroup$
I have got a Problem with the following fitch proof excercise:
$quad;; |$
$triangleright quad | quad ?. quad (lnot forall x ; P(x)) leftrightarrow (exists x lnot P(x))$
This is how far I got: (Notice: I started from the bottom to the top!)
My problem is, that I can't find a way how to contradict $P(c)$. My first idea was, to proof $forall x ; P(x)$ in the subproof in order to get a contradiction.
As you can see, this is only the first part of the proof. I know that I will have to use a Biconditional introduction in the end. I only need help for the first subproof.
Would be great if anyone could give me some hints.
logic first-order-logic predicate-logic
logic first-order-logic predicate-logic
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
asked Jan 5 at 12:17
JenewJenew
112
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
asked Jan 5 at 12:17
JenewJenew
112
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
edited Feb 18 at 14:32
Mauro ALLEGRANZA
66.9k449115
66.9k449115
asked Jan 5 at 12:17
JenewJenew
112
asked Jan 5 at 12:17
JenewJenew
112
asked Jan 5 at 12:17
JenewJenew
112
112
$begingroup$
Welcome to math stackexchange. I have tidied up your question -- we like it when titles are very specific! I hope you find the answers helpful.
$endgroup$
– 6005
Jan 5 at 13:02
$begingroup$
Thank you very much. I will do better next time ;).
$endgroup$
– Jenew
Jan 5 at 13:10
add a comment |
$begingroup$
Welcome to math stackexchange. I have tidied up your question -- we like it when titles are very specific! I hope you find the answers helpful.
$endgroup$
– 6005
Jan 5 at 13:02
$begingroup$
Thank you very much. I will do better next time ;).
$endgroup$
– Jenew
Jan 5 at 13:10
$begingroup$
Welcome to math stackexchange. I have tidied up your question -- we like it when titles are very specific! I hope you find the answers helpful.
$endgroup$
– 6005
Jan 5 at 13:02
$begingroup$
Welcome to math stackexchange. I have tidied up your question -- we like it when titles are very specific! I hope you find the answers helpful.
$endgroup$
– 6005
Jan 5 at 13:02
$begingroup$
Thank you very much. I will do better next time ;).
$endgroup$
– Jenew
Jan 5 at 13:10
$begingroup$
Thank you very much. I will do better next time ;).
$endgroup$
– Jenew
Jan 5 at 13:10
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
It looks to me like you are trying to show that $lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $forall x ( lnot P(x))$. But that's too strong -- you only want to show that $exists x (lnot P(x))$. (Convince yourself that $forall x ( lnot P(x))$ is not necessarily implied by $lnot (forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)
So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $exists x (lnot P(x))$; but you only know that $lnot forall x. P(x)$, and there's no way to get a $c$ directly from that statement.
In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $exists x (lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving
$$
lnot lnot (exists x ( lnot P(x))),
$$
by assuming $lnot exists x ( lnot P(x)))$ and getting a contradiction.
The proof structure will look like this:
1. $lnot ( forall x ( P(x)))$
$lnot exists x ( lnot P(x))$
...[fill in here]...
$bot$
5. $lnot lnot exists x (lnot P(x))$
6. $exists x (lnot P(x))$ (double negation elimination from 5)
But you have to fill in the details for step 3. ... above.
To do this, show as another lemma there that $forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.
$^1$ To prove $forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $lnot P(a)$ and derive a contradiction, thus showing $lnot lnot P(a)$, then double negation to $P(a)$.
answered Jan 5 at 12:51
60056005
36.3k751125
$endgroup$
1
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
add a comment |
$begingroup$
Hint
You have to start assuming $lnot Pc$ and $lnot exists x lnot Px$ and find a first contradiction.
Then use Double Negation to derive $Pc$ and from it $forall x Px$ and a new contradiction.
Then, conclude by Double Negation again.
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3062661%2ffitch-proof-exercise-showing-lnot-forall-x-px-leftrightarrow-exist%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
It looks to me like you are trying to show that $lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $forall x ( lnot P(x))$. But that's too strong -- you only want to show that $exists x (lnot P(x))$. (Convince yourself that $forall x ( lnot P(x))$ is not necessarily implied by $lnot (forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)
So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $exists x (lnot P(x))$; but you only know that $lnot forall x. P(x)$, and there's no way to get a $c$ directly from that statement.
In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $exists x (lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving
$$
lnot lnot (exists x ( lnot P(x))),
$$
by assuming $lnot exists x ( lnot P(x)))$ and getting a contradiction.
The proof structure will look like this:
1. $lnot ( forall x ( P(x)))$
$lnot exists x ( lnot P(x))$
...[fill in here]...
$bot$
5. $lnot lnot exists x (lnot P(x))$
6. $exists x (lnot P(x))$ (double negation elimination from 5)
But you have to fill in the details for step 3. ... above.
To do this, show as another lemma there that $forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.
$^1$ To prove $forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $lnot P(a)$ and derive a contradiction, thus showing $lnot lnot P(a)$, then double negation to $P(a)$.
answered Jan 5 at 12:51
60056005
36.3k751125
$endgroup$
1
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
add a comment |
$begingroup$
It looks to me like you are trying to show that $lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $forall x ( lnot P(x))$. But that's too strong -- you only want to show that $exists x (lnot P(x))$. (Convince yourself that $forall x ( lnot P(x))$ is not necessarily implied by $lnot (forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)
So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $exists x (lnot P(x))$; but you only know that $lnot forall x. P(x)$, and there's no way to get a $c$ directly from that statement.
In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $exists x (lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving
$$
lnot lnot (exists x ( lnot P(x))),
$$
by assuming $lnot exists x ( lnot P(x)))$ and getting a contradiction.
The proof structure will look like this:
1. $lnot ( forall x ( P(x)))$
$lnot exists x ( lnot P(x))$
...[fill in here]...
$bot$
5. $lnot lnot exists x (lnot P(x))$
6. $exists x (lnot P(x))$ (double negation elimination from 5)
But you have to fill in the details for step 3. ... above.
To do this, show as another lemma there that $forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.
$^1$ To prove $forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $lnot P(a)$ and derive a contradiction, thus showing $lnot lnot P(a)$, then double negation to $P(a)$.
answered Jan 5 at 12:51
60056005
36.3k751125
$endgroup$
1
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
add a comment |
$begingroup$
It looks to me like you are trying to show that $lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $forall x ( lnot P(x))$. But that's too strong -- you only want to show that $exists x (lnot P(x))$. (Convince yourself that $forall x ( lnot P(x))$ is not necessarily implied by $lnot (forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)
So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $exists x (lnot P(x))$; but you only know that $lnot forall x. P(x)$, and there's no way to get a $c$ directly from that statement.
In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $exists x (lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving
$$
lnot lnot (exists x ( lnot P(x))),
$$
by assuming $lnot exists x ( lnot P(x)))$ and getting a contradiction.
The proof structure will look like this:
1. $lnot ( forall x ( P(x)))$
$lnot exists x ( lnot P(x))$
...[fill in here]...
$bot$
5. $lnot lnot exists x (lnot P(x))$
6. $exists x (lnot P(x))$ (double negation elimination from 5)
But you have to fill in the details for step 3. ... above.
To do this, show as another lemma there that $forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.
$^1$ To prove $forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $lnot P(a)$ and derive a contradiction, thus showing $lnot lnot P(a)$, then double negation to $P(a)$.
answered Jan 5 at 12:51
60056005
36.3k751125
$endgroup$
It looks to me like you are trying to show that $lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $forall x ( lnot P(x))$. But that's too strong -- you only want to show that $exists x (lnot P(x))$. (Convince yourself that $forall x ( lnot P(x))$ is not necessarily implied by $lnot (forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)
So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $exists x (lnot P(x))$; but you only know that $lnot forall x. P(x)$, and there's no way to get a $c$ directly from that statement.
In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $exists x (lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving
$$
lnot lnot (exists x ( lnot P(x))),
$$
by assuming $lnot exists x ( lnot P(x)))$ and getting a contradiction.
The proof structure will look like this:
1. $lnot ( forall x ( P(x)))$
$lnot exists x ( lnot P(x))$
...[fill in here]...
$bot$
5. $lnot lnot exists x (lnot P(x))$
6. $exists x (lnot P(x))$ (double negation elimination from 5)
But you have to fill in the details for step 3. ... above.
To do this, show as another lemma there that $forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.
$^1$ To prove $forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $lnot P(a)$ and derive a contradiction, thus showing $lnot lnot P(a)$, then double negation to $P(a)$.
answered Jan 5 at 12:51
60056005
36.3k751125
answered Jan 5 at 12:51
60056005
36.3k751125
answered Jan 5 at 12:51
60056005
36.3k751125
answered Jan 5 at 12:51
60056005
36.3k751125
36.3k751125
1
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
add a comment |
1
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
1
1
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
Thanks for this answer! I managed to find the solution. My fitch program tells me its correct. It was actually way more complex than I thougth.
$endgroup$
– Jenew
Jan 5 at 16:22
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
$begingroup$
@Jenew Yes, this was a messy one. Sometimes you just end up with tons of sub-proofs by contradiction followed by double-negation elimination.
$endgroup$
– 6005
Jan 5 at 16:40
add a comment |
$begingroup$
Hint
You have to start assuming $lnot Pc$ and $lnot exists x lnot Px$ and find a first contradiction.
Then use Double Negation to derive $Pc$ and from it $forall x Px$ and a new contradiction.
Then, conclude by Double Negation again.
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
add a comment |
$begingroup$
Hint
You have to start assuming $lnot Pc$ and $lnot exists x lnot Px$ and find a first contradiction.
Then use Double Negation to derive $Pc$ and from it $forall x Px$ and a new contradiction.
Then, conclude by Double Negation again.
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
add a comment |
$begingroup$
Hint
You have to start assuming $lnot Pc$ and $lnot exists x lnot Px$ and find a first contradiction.
Then use Double Negation to derive $Pc$ and from it $forall x Px$ and a new contradiction.
Then, conclude by Double Negation again.
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
Hint
You have to start assuming $lnot Pc$ and $lnot exists x lnot Px$ and find a first contradiction.
Then use Double Negation to derive $Pc$ and from it $forall x Px$ and a new contradiction.
Then, conclude by Double Negation again.
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
edited Jan 5 at 13:04
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
answered Jan 5 at 12:29
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
66.9k449115
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
add a comment |
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
$begingroup$
Right. Although it does not address possible issues with the poster's attempted solution.
$endgroup$
– 6005
Jan 5 at 12:56
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3062661%2ffitch-proof-exercise-showing-lnot-forall-x-px-leftrightarrow-exist%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
Welcome to math stackexchange. I have tidied up your question -- we like it when titles are very specific! I hope you find the answers helpful.
$endgroup$
– 6005
Jan 5 at 13:02
$begingroup$
Thank you very much. I will do better next time ;).
$endgroup$
– Jenew
Jan 5 at 13:10