[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Instantiation hints




c5: lemma 
    (exists (a,b,c:real): a>b and b<c) => (exists (b,c,a:real): a<c and a<c)


  |-------
{1}   (EXISTS (a, b, c: real): a > b AND b < c) =>
       (EXISTS (b, c, a: real): a < c AND a < c)

Rule? (skosimp*)
Repeatedly Skolemizing and flattening,
this simplifies to: 
c5:  

{-1}  a!1 > b!1
{-2}  b!1 < c!1
  |-------
{1}   (EXISTS (b, c, a: real): a < c AND a < c)

Rule? (inst 1 "b!1" "c!1" "a!1")
Instantiating the top quantifier in 1 with the terms: 
 b!1, c!1, a!1,
this simplifies to: 
c5:  

[-1]  a!1 > b!1
[-2]  b!1 < c!1
  |-------
{1}   a!1 < c!1 AND a!1 < c!1

If you want to instantiate some and not others:

{-1}  a!1 > b!1
{-2}  b!1 < c!1
  |-------
{1}   (EXISTS (b, c, a: real): a < c AND a < c)

Rule? (inst 1 "b!1" "_" "a!1")
Instantiating the top quantifier in 1 with the terms: 
 b!1, _, a!1,
this simplifies to: 
c5:  

[-1]  a!1 > b!1
[-2]  b!1 < c!1
  |-------
{1}   EXISTS (c): a!1 < c AND a!1 < c