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] Can not build documentation because building polyscripter fails

I found the place where “-lgmp” was missing (see attached diff). This is a workaround. A better solution would be to allow the user to override the linker flags with a declaration in “poly-includes.ML”. -- Do not eat animals; respect them as you respect people.

[Hol-info] Can not build documentation because building polyscripter fails

In a recent development version (commit 38d36b51a) doing “make” in the directory “Manual” fails. I traced the error to a failure to build polyscripter. Here is what appears in Manual/Tools/.hollogs/polyscripter: “““ -

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