Re: [Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

Hi Mario, I just want to instantiate `l`, but now I know it is impossible. I will try another method. Thank you for your answers. Regards, Liu > -Original Messages- > From: "Mario Castelán Castro" > Sent Time: 2017-12-19 23:27:35 (Tuesday) > To:

Re: [Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

Hi Thomas, Thank you for your detailed answers, now I get it. I will try to ues another method to solve my problem. Regards, Liu -Original Messages- From:"Thomas Tuerk" Sent Time:2017-12-19 23:10:56 (Tuesday) To: hol-info@lists.sourceforge.net Cc:

Re: [Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

Hi Liu, you can't instantiate such a variable. The existential quantifier in your formula is morally a universal one. (?x. P x) ==> Q is equivalent to !x. (P x ==> Q) Let's make an example and instantiate P and Q as follows: P x := (x = 5) Q := F Then (?x. P x) ==> Q does not hold. "?x. P

Re: [Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

Hello. You can not choose the value of «l» because it is in the antecedent. You must prove it for any value of “l”, as seen in the following equivalence: > SIMP_CONV pure_ss [GSYM LEFT_FORALL_IMP_THM] “(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)”; <> val it = ⊢ (∃l. (l1

Re: [Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

Hello. You can not choose the value of «l» because it is in the antecedent. You must prove it for any value of “l”, as seen in the following equivalence: > SIMP_CONV pure_ss [GSYM LEFT_FORALL_IMP_THM] “(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)”; <> val it = ⊢

Re: [Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

On 19/12/17 05:21, Liu Gengyang wrote: > How can I instantiate the variable which constrained by the existential > quantifier in the parentheses(i.e. (?x. _) ==> _, replacing x with a specific > value.)? For example, > > > (?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2) > > >

[Hol-info] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

Hi， How can I instantiate the variable which constrained by the existential quantifier in the parentheses(i.e. (?x. _) ==> _, replacing x with a specific value.)? For example, (?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2) Now I want to instantiate `l` using `[]` ,which