Trinh Le Khanh (Oct 16 2020 at 10:15): Trinh Le Khanh (Oct 16 2020 at 10:15):Hello everyone,
I'm working in the field of software verification and try to use Isabelle to prove the equivalence between two formulas. I tried three lemmas and have some questions as follows:
lemma test1: "(P 0 ⟶ ~P 1) ∧ (P 1 ⟶ ~P 0) ⟹ ~P 0∨~P 1"
apply(auto)
done
It worked perfectly as I want.
lemma test2: "(P 0 --> (~P 1 & ~P 2)) & (P 1 --> (~P 0 & ~P 2)) & (P 2 --> (~P 1 & ~P 0))
==> ((~P 1 & ~P 2) | (~P 0 & ~P 2) | (~P 1 & ~P 0))"
apply(auto)
done
When I added one more predicate "P 2", it run until out of memory. I don't think that the lemma is big enough unprovable like this.
lemma test3: "⋀i∈I.(P i ⟶ (⋀j∈I-{i}. ¬P j)) ⟹ ⋁i∈I.(⋀j∈I-{i}. ¬P j)"
apply (auto)
done
I tested a generic case and the Isabelle showed that "Failed to apply proof method". I tried to add "apply (induction)" and the result is "Failed to finish proof". So I guess the problem is about applying the right proof method, right? Then, I tried some other like "simp" or "rules" but they didn't work.
P.s: the symbol "bigvee" and "bigwedge" are redefined as follows (@Mathias Fleury re-defined it)
Screenshot-2020-10-16-at-12.13.52.png
Could you explain those questions, please? Thank you very much.
Manuel Eberl (Oct 16 2020 at 10:29):As for 2, auto is not always the best way to go. In this particular case, it seems that the simplifier loops (no idea why). More specialised methods for logic/set theory like blast and metis and smt solve this almost instantly. There are also more obscure ones (argo, sat, satx) that do a good job here.
As for the bigvee thing, please post the actual source could and not just a screenshot. It's a lot of text to copy from a screenshot by hand. I don't really understand what the advantage of bigvee and bigwedge are over Bex and Ball, i.e. ∃x∈A. P x instead of ⋁x∈A. P x.
Lukas Stevens (Oct 16 2020 at 10:32):Zulip uses markdown as markup so you can use triple backticks for code like this:
f x = x
Also, I don't think 3 holds if I is the empty set. The following can easily be proven by blast:
∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ I ≠ {} ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j
This is the source code:
theory test1
imports Main
begin
context comm_monoid_add (*commutative monoid with addition*)
begin
sublocale bigvee: comm_monoid_set HOL.disj False
defines bigvee = bigvee.F and bigvee' = bigvee.G
by standard auto
abbreviation bigvee'' :: ‹bool set ⇒ bool› ("⋁")
where "⋁ ≡ bigvee (λx. x)"
sublocale bigwedge: comm_monoid_set HOL.conj True
defines bigwedge = bigwedge.F and bigwedge' = bigwedge.G
by standard auto
abbreviation bigwedge'' :: ‹bool set ⇒ bool› ("⋀")
where "⋀ ≡ bigwedge (λx. x)"
end
syntax (*Define pattern of bigwedge and bigvee*)
"_bigwedge" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add" ("(2⋀(_/∈_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
"⋀i∈A. b" ⇌ "CONST bigwedge (λi. b) A"
syntax
"_bigvee" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add" ("(2⋁(_/∈_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!› (*translation between parse rules or print rules*)
"⋁i∈A. b" ⇌ "CONST bigvee (λi. b) A"
(*CONST ensures that the given identifier is treated as constant term*)
instantiation bool :: comm_monoid_add
begin
definition zero_bool where
[simp]: ‹zero_bool = False›
definition plus_bool where
[simp]: ‹plus_bool = (∨)›
instance
by standard auto
end
thm bigvee_def
thm bigwedge_def
(*meaningful name*)
definition J :: "nat set" where
"J = {n . n > 0}"
definition U :: "nat set" where
"U = {n . n > 0}"
definition T :: "nat set" where
"T = {n . n > 0}"
definition I :: "nat set" where
"I = {n . n > 0}"
definition V :: "nat set" where
"V = {n . n > 0}"
definition K :: "nat set" where
"K = {n . n > 0}"
definition H :: "nat set" where
"H = {n . n > 0}"
definition L :: "nat set" where
"L = {n . n > 0}"
definition B :: "nat set" where
"B = {1, 2, 3, 4}"
lemma ‹finite A ⟹ (⋁i∈A. f i) ⟷ (∃i ∈ A. f i)›
apply (induction rule: finite_induct)
apply (auto simp: )
done
lemma ‹finite A ⟹ (⋀i∈A. f i) ⟷ A = {} ∨ (∀i ∈ A. f i)›
apply (induction rule: finite_induct)
apply (auto simp: )
done
lemma ‹infinite A ⟹ (⋀i∈A. f i) ⟷ True›
by auto
lemma test0:
‹(⋀j∈J. ⋀u∈U. ⋀t∈T. ⋀l∈L. ⋀l⇩1∈L-{l}. ¬P j u t l⇩1) ∨
(⋁i∈I. ⋁v∈V. ⋀k∈K. ⋁h∈H. Q i v k h) ⟹
(⋁i∈I. ⋁v∈V. ⋀k∈K. ⋁h∈H. Q i v k h) ∨ (⋀j∈J. ⋀u∈U. ⋀t∈T. ⋀l⇩1∈-{l}. ¬P j u t l⇩1)›
apply auto
done
lemma "∀ x. P x ⟶ P x"
apply (auto)
done
lemma test1: "(P 0 ⟶ ~P 1) ∧ (P 1 ⟶ ~P 0) ⟹ ~P 0∨~P 1"
apply(auto)
done
(*
lemma test2: "(P 0 --> (~P 1 & ~P 2)) & (P 1 --> (~P 0 & ~P 2)) & (P 2 --> (~P 1 & ~P 0))
==> ((~P 1 & ~P 2) | (~P 0 & ~P 2) | (~P 1 & ~P 0))"
apply(auto)
done *)
lemma test3: "⋀i∈I.(P i ⟶ (⋀j∈I-{i}. ¬P j)) ⟹ ⋁i∈I.(⋀j∈I-{i}. ¬P j)"
apply (induction)
apply (auto)
done
If you want to do induction, you should specify what you want to do induction over.
Trinh Le Khanh (Oct 16 2020 at 10:35):I defined the set B with 4 elements and used it but the 3rd lemma returned the same result.
Manuel Eberl (Oct 16 2020 at 10:38):Also note that bigwedge over an infinite set is always true and bigvee over an infinite set is always false. So 3 is trivially false because I is infinite.
Manuel Eberl (Oct 16 2020 at 10:38):I think you really want to use ∀x∈I etc.
Manuel Eberl (Oct 16 2020 at 10:39):then you don't need induction either, it's straightforward set theory and blast can do it (as long as you feed in the fact that I ≠ {}).
Trinh Le Khanh (Oct 16 2020 at 10:44):So if I have
I = {1, 2, 3, 4}
I can use this directly, right?
∀i∈I.⋀P i = P 1 ∧ P 2 ∧ P 3 ∧ P 4
∀i∈I.⋁P i = P 1 ∨ P 2 ∨ P 3 ∨ P 4
You probably mean
(∀i∈I. P i) = P 1 ∧ P 2 ∧ P 3 ∧ P 4
(∃i∈I. P i) = P 1 ∨ P 2 ∨ P 3 ∨ P 4
right?
In that case: Yes. You just have to unfold the definition of I and then it simplifies to that.
Trinh Le Khanh (Oct 16 2020 at 11:18):(deleted)
Trinh Le Khanh (Oct 16 2020 at 11:31):Manuel Eberl said:
Also, I don't think 3 holds if
Iis the empty set. The following can easily be proven by blast:∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ I ≠ {} ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j
Thank you. I tried this with blast and it worked.
I also tried that:
definition I :: "nat set" where
"I = {1, 2, 3, 4}"
I ≠ {} lemma test3: "∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j"
apply (blast)
done
It's failed to prove. So I ≠ {} seems mandatory despite we define set I or not, right?
Manuel Eberl (Oct 16 2020 at 11:47):blast doesn't know how you defined the set. You can e.g. unfold the definition like this:
lemma test3: "∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j"
unfolding I_def by blast
Or you can prove that I is nonempty first and then supply that fact to blast:
lemma I_not_empty: "I ≠ {}"
by (auto simp: I_def)
lemma test3: "∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j"
using I_not_empty by blast
Wow, that's awesome. Thank you very much.
Manuel Eberl (Oct 16 2020 at 12:17):If you want to learn Isabelle systematically, I suggest you work through the first half of the ‘Concrete Semantics’ books. It's online for free: http://www.concrete-semantics.org/
Trinh Le Khanh (Oct 16 2020 at 12:24):Thank you for your suggestion. After putting my lemma and choosing to prove them using metis, the metis is highlighted in purple (and my computer's fans are running so hard). Do you know the meaning of this color? (I just know that red for error). Screenshot-2020-10-16-at-14.19.08.png
Manuel Eberl (Oct 16 2020 at 12:32):It means that the command is still running. Metis might not be good enough to do something this big. Other methods might be. If you paste the full example in here, I can have a look at it.
Trinh Le Khanh (Oct 16 2020 at 12:36):Here you are. I tried blast first but it couldn't prove. Thus, I changed to metis.
theory MyMaths
imports Main
begin
definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A & ~B) | (~A & B)"
definition J :: "nat set" where
"J = {n . n > 0}"
definition U :: "nat set" where
"U = {n . n > 0}"
definition T :: "nat set" where
"T = {n . n > 0}"
definition I :: "nat set" where
"I = {n . n > 0}"
definition V :: "nat set" where
"V = {n . n > 0}"
definition K :: "nat set" where
"K = {n . n > 0}"
definition H :: "nat set" where
"H = {n . n > 0}"
definition L :: "nat set" where
"L = {n . n > 0}"
lemma "((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∨ (∃h∈H.∃i∈I.∃v∈V.∀k∈K. (Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))
∧ (∃l∈L.∃h∈H.((∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))
⟹ (∃h∈H.((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∧ (∀i∈I.∀v∈V.∀k∈K.∀h⇩1∈H-{h}.¬Q i v k h⇩1)))
∨ (∃l∈L.∃h∈H.(∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.(Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))"
unfolding I_def and V_def and K_def and H_def and J_def and U_def and T_def and L_def
using [[simp_trace]]
by metis
end
Okay, now you're back to infinite sets again. That means things like SAT solvers cannot be used. The definitions of your sets don't really make the problem any easier either, so I don't think unfolding helps.
Manuel Eberl (Oct 16 2020 at 14:16):Normally, I would say to tackle something like this with an SMT solver like Z3 or CVC4, but it seems this is too difficult for them.
Manuel Eberl (Oct 16 2020 at 14:16):(then again, I am not sure if this holds in the first place)
Manuel Eberl (Oct 16 2020 at 14:28):For two particular values of P and Q, I was able to prove the negation of your goal, so apparently it doesn't hold:
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
lemma "¬(((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∨ (∃h∈H.∃i∈I.∃v∈V.∀k∈K. (Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))
∧ (∃l∈L.∃h∈H.((∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))
⟶ (∃h∈H.((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∧ (∀i∈I.∀v∈V.∀k∈K.∀h⇩1∈H-{h}.¬Q i v k h⇩1)))
∨ (∃l∈L.∃h∈H.(∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.(Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))))"
unfolding I_def and V_def and K_def and H_def and J_def and U_def and T_def and L_def P_def Q_def
apply auto
apply (rule exI[of _ 2])
apply auto
subgoal for h
apply (rule bexI[of _ "h + 2"])
apply auto
done
The proof isn't pretty, but it gets the point across. I found that particular counterexample for P and Q using the nitpick command.
Trinh Le Khanh (Oct 16 2020 at 14:44):I might make something wrong when typing the formulas. I'll check it again.
To make sure that they're not infinite sets. I re-defined as follows (each set has 99 elements):
definition J :: "nat set" where
"J = {n . n < 100}"
definition U :: "nat set" where
"U = {n . n < 100}"
definition T :: "nat set" where
"T = {n . n < 100}"
definition I :: "nat set" where
"I = {n . n < 100}"
definition V :: "nat set" where
"V = {n . n < 100}"
definition K :: "nat set" where
"K = {n . n < 100}"
definition H :: "nat set" where
"H = {n . n < 100}"
definition L :: "nat set" where
"L = {n . n < 100}"
Nope.
definition J :: "nat set" where
"J = {n . n < 100}"
definition U :: "nat set" where
"U = {n . n < 100}"
definition T :: "nat set" where
"T = {n . n < 100}"
definition I :: "nat set" where
"I = {n . n < 100}"
definition V :: "nat set" where
"V = {n . n < 100}"
definition K :: "nat set" where
"K = {n . n < 100}"
definition H :: "nat set" where
"H = {n . n < 100}"
definition L :: "nat set" where
"L = {n . n < 100}"
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
lemma *: "(∃x∈A - B. R x) ⟷ (∃x. x ∈ A ∧ x ∉ B ∧ R x)"
"(∀x∈A - B. R x) ⟷ (∀x. x ∉ A ∨ x ∈ B ∨ R x)"
by auto
lemma "¬(((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∨ (∃h∈H.∃i∈I.∃v∈V.∀k∈K. (Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))
∧ (∃l∈L.∃h∈H.((∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))
⟶ (∃h∈H.((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∧ (∀i∈I.∀v∈V.∀k∈K.∀h⇩1∈H-{h}.¬Q i v k h⇩1)))
∨ (∃l∈L.∃h∈H.(∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.(Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))))"
unfolding I_def and V_def and K_def and H_def and J_def and U_def and T_def and L_def P_def Q_def
apply (auto simp: *)
apply presburger+
done
(presburger is a decision procedure for Presburger logic, i.e. linear arithmetic on integers plus quantifiers. It has pretty terrible performance, but in this case, it works pretty well.)
Trinh Le Khanh (Oct 16 2020 at 15:10):Can you explain why did you define P and Q like this?
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
Because it leads to a counterexample?
Manuel Eberl (Oct 16 2020 at 15:11):The way you stated your lemma, P and Q were free variables, i.e. you claimed that it holds for all values of P and Q. I showed that there are two particular values for which it does not hold.
Trinh Le Khanh (Oct 16 2020 at 15:12):But when you applied presburger+, it's solved, right?
Trinh Le Khanh (Oct 16 2020 at 15:14):Ah, when I remove your definition of P and Q, it's unsolvable.
Manuel Eberl (Oct 16 2020 at 15:14):I proved the negation of your lemma.
Manuel Eberl (Oct 16 2020 at 15:15):If we call the statement of your lemma foo(P,Q), you essentially claimed ∀P Q. foo(P,Q). I showed ∃P Q. ¬foo(P,Q).
Trinh Le Khanh (Oct 16 2020 at 15:16):Yes, I see. So the problem is the correctness of my lemma, not the definition.
Trinh Le Khanh (Oct 18 2020 at 23:37):The proof isn't pretty, but it gets the point across. I found that particular counterexample for P and Q using the
nitpickcommand.
Hi Manuel, how can you generate the definition of P and Q using the nitpick command? When I used this command, it showed hundreds of lines like this Screenshot-2020-10-19-at-01.36.04.png
Manuel Eberl (Oct 19 2020 at 07:23):I did it for the variant with {n. n > 0}. Or rather, I think I even did it for the variant where all the sets where UNIV (which I think should be equivalent).
Trinh Le Khanh (Oct 19 2020 at 11:45):I set up the variant with {n. n>0} and the result is shown as follows:
Screenshot-2020-10-19-at-13.43.18.png
Screenshot-2020-10-19-at-13.43.48.png
How did you generate the definition of P and Q from them?
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
This is perhaps a bit tricky to read. If you look at the first one, you see that it's a predicate P a b c d that is defined to be false for all a, b, c, d ≤ 2 and unspecified everywhere else. So I went ahead and just defined it to be false everywhere.
Manuel Eberl (Oct 19 2020 at 15:19):For Q you just have to see for which combinations of the values 0,1,2 for a,b,c,d it is true and then write down a definition that does exactly that
Trinh Le Khanh (Oct 19 2020 at 21:52):Thank you :D. I have another question is that I'm testing my formulas with a small case. My code to setup is:
theory prog_2
imports Main
begin
(*P*)
definition J :: "nat set" where
"J = {0}"
definition U :: "nat set" where
"U = {0}"
definition T :: "nat set" where
"T = {0}"
definition L :: "nat set" where
"L = {0, 1}"
(*Q*)
definition I :: "nat set" where
"I = {0, 1}"
definition V :: "nat set" where
"V = {0}"
definition K :: "nat set" where
"K = {0}"
definition H :: "nat set" where
"H = {0, 1}"
(*test*)
value "∃l∈L.∃h∈H.(∀j∈J.∀u∈U.(∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K. Q i v k h)))"
end
The result is:
(P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
But my expected output is:
(P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 1)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 0)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 1)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 0)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
I know that because I put ∃h∈H out of the first open bracket, so the result has the same value at the h position. I tried to move ∃h∈H inside or use another variable like h1 but the result is not what I expected. Do you have any suggestion?
Trinh Le Khanh (Oct 20 2020 at 08:46):My solution is that I added the formula for the different h like this
value "∃l∈L.∃h∈H.(∀j∈J.∀u∈U.(∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K.∃h1∈H-{h}. Q i v k h1))
∨ (∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K. Q i v k h)))"
It works. It seems not the smart way, though.
UPDATE: It DOESN'T works. It duplicated the result :D
Mathias Fleury (Oct 20 2020 at 08:56):I think that you are confusing and . You version is equivalent to putting the inside the implication symbol:
lemma "(∃l∈L. (∀j∈J. ∀u∈U. (∀t∈T. (P j u t l ⟶ (∃h∈H. ∃i∈I.∃v∈V.∀k∈K. Q i v k h))))) ⟷
(∃l∈L.∃h∈H.(∀j∈J.∀u∈U.(∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K.∃h1∈H-{h}. Q i v k h1))
∨ (∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K. Q i v k h))))"
unfolding L_def I_def J_def V_def H_def T_def K_def
apply auto
done
I think that you are confusing \forall \exists∀∃ and \exists\forall∃∀. You version is equivalent to putting the \exists∃ inside the implication symbol
Thank you. I know that but this is a small piece of my code. I need something like
((P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0) ∧ ¬(all the others))
∨ ((P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1) ∧ ¬(all the others))
∨ ((P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 1) ∧ ¬(all the others))
∨ ((P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 0) ∧ ¬(all the others))
So if I put the \exists inside, it looks like:
((P 0 0 0 0 ⟶ (Q 0 0 0 0 ∨ Q 1 0 0 0) ∨ Q 0 0 0 1 ∨ Q 1 0 0 1) ∧ ¬(all the others))
The two things are different.
Last updated: Dec 21 2024 at 16:20 UTC