test00a-tx.fq

// This qualifier saves the day; solve constraints WITHOUT IT
// qualif Zog(v:a) : (10 <= v)

constraint:
  env [z : {v : int | true}]
  lhs {v : int | (z=10) \/ (z=20)}
  rhs {v : int | 10 <= z}
  id 3 

/*

Rewriting constraints as:

    id 1
    x:int, v:int |- x=10 /\ v=x => k0
    
    id 2
    y:int, v:int |- y=20 /\ v=y => k0

Projecting out all variables NOT in the WF of k0

    id 1
    v:int |- (exists x:int. x=10 /\ v=x) => k0
           
    id 2
    v:int |- (exists y:int. y=20 /\ v=y) => k0

Take the \/ of all constraints on k0

     k0 = (exists x:int. x=10 /\ v=x) \/ (exists y:int. y=20 /\ v=y)
     
     k0[z/v]
       = (\x. x=10 /\ v=x) \/ (\y. y=20 /\ v=y)[z/v]
         = (\x. x=10 /\ z=x) \/ (\y. y=20 /\ z=y)

So you get:

     env [2]
        lhs {v : int | (\x. x=10 /\ z=x) \/ (\y. y=20 /\ z=y)}
     rhs {v : int | 10 <= z}
     id 3 

*/