liquid-fixpoint-0.9.6.3.2: tests/pos/polyset.fq

data PolySet.Lst 1 = [
       | PolySet.Cons {PolySet.hd : @(0), PolySet.tl : (PolySet.Lst @(0))}
       | PolySet.Emp {}
     ]

constant PolySet.hd : (func(1 , [(PolySet.Lst @(0)); @(0)]))
constant PolySet.tl : (func(1 , [(PolySet.Lst @(0)); (PolySet.Lst @(0))]))
constant is$PolySet.Cons : (func(1 , [(PolySet.Lst @(0)); bool]))
constant is$PolySet.Emp : (func(1 , [(PolySet.Lst @(0)); bool]))
constant PolySet.Cons : (func(1 , [@(0);
                                   (PolySet.Lst @(0));
                                   (PolySet.Lst @(0))]))
constant PolySet.lstHd : (func(1 , [(PolySet.Lst @(0));
                                    (Set_Set @(0))]))

bind 1 PolySet.Emp : {VV : func(1 , [(PolySet.Lst @(0))]) | []}
bind 2 PolySet.Cons : {VV : func(1 , [@(0);
                                       (PolySet.Lst @(0));
                                       (PolySet.Lst @(0))]) | []}
bind 3 p : {VV : (PolySet.Lst l) | []}

constraint:
  env [1; 2; 3]
  lhs {VV : (PolySet.Lst (PolySet.Lst l)) | [(is$PolySet.Cons VV);
                                             (~ ((is$PolySet.Emp VV)));
                                             (VV = (PolySet.Cons p PolySet.Emp));
                                             ((PolySet.hd VV) = p);
                                             ((PolySet.tl VV) = PolySet.Emp);
                                             ((PolySet.lstHd VV) = (Set_sng p))]}
  rhs {VV : (PolySet.Lst (PolySet.Lst l)) | [(VV = (PolySet.Cons p PolySet.Emp))]}
  id 4 tag [4]