packages feed

liquid-fixpoint-0.7.0.3: tests/pos/test000.hs.fq

qualif Fst(v : @(1), y : @(0)): (v = fst([y])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.spec" (line 29, column 8)
qualif Snd(v : @(1), y : @(0)): (v = snd([y])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.spec" (line 30, column 8)
qualif IsEmp(v : GHC.Types.Bool, xs : [@(0)]): ((? Prop([v])) <=> (len([xs]) > 0)) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 13, column 8)
qualif IsEmp(v : GHC.Types.Bool, xs : [@(0)]): ((? Prop([v])) <=> (len([xs]) = 0)) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 14, column 8)
qualif ListZ(v : [@(0)]): (len([v]) = 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 16, column 8)
qualif ListZ(v : [@(0)]): (len([v]) >= 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 17, column 8)
qualif ListZ(v : [@(0)]): (len([v]) > 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 18, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]): (len([v]) = len([xs])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 20, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]): (len([v]) >= len([xs])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 21, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]): (len([v]) > len([xs])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 22, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]): (len([v]) <= len([xs])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 23, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]): (len([v]) < len([xs])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 24, column 8)
qualif EqLen(v : int, xs : [@(0)]): (v = len([xs])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 26, column 8)
qualif LenEq(v : [@(0)], x : int): (x = len([v])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 27, column 8)
qualif LenDiff(v : [@(0)], x : int): (len([v]) = (x + 1)) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 28, column 8)
qualif LenDiff(v : [@(0)], x : int): (len([v]) = (x - 1)) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 29, column 8)
qualif LenAcc(v : int, xs : [@(0)], n : int): (v = (len([xs]) + n)) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/GHC/Base.hquals" (line 30, column 8)
qualif Bot(v : @(0)): (0 = 1) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 3, column 8)
qualif Bot(v : @(0)): (0 = 1) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 4, column 8)
qualif Bot(v : @(0)): (0 = 1) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 5, column 8)
qualif Bot(v : bool): (0 = 1) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 6, column 8)
qualif Bot(v : int): (0 = 1) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 7, column 8)
qualif CmpZ(v : @(0)): (v < 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 9, column 8)
qualif CmpZ(v : @(0)): (v <= 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 10, column 8)
qualif CmpZ(v : @(0)): (v > 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 11, column 8)
qualif CmpZ(v : @(0)): (v >= 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 12, column 8)
qualif CmpZ(v : @(0)): (v = 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 13, column 8)
qualif CmpZ(v : @(0)): (v != 0) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 14, column 8)
qualif Cmp(v : @(0), x : @(0)): (v < x) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 16, column 8)
qualif Cmp(v : @(0), x : @(0)): (v <= x) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 17, column 8)
qualif Cmp(v : @(0), x : @(0)): (v > x) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 18, column 8)
qualif Cmp(v : @(0), x : @(0)): (v >= x) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 19, column 8)
qualif Cmp(v : @(0), x : @(0)): (v = x) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 20, column 8)
qualif Cmp(v : @(0), x : @(0)): (v != x) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 21, column 8)
qualif One(v : int): (v = 1) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 28, column 8)
qualif True(v : bool): (? v) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 29, column 8)
qualif False(v : bool): (~ ((? v))) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 30, column 8)
qualif True1(v : GHC.Types.Bool): (? Prop([v])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 31, column 8)
qualif False1(v : GHC.Types.Bool): (~ ((? Prop([v])))) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 32, column 8)
qualif Papp(v : @(0), p : (Pred  @(0))): (? papp1([p;
                                                   v])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 35, column 8)
qualif Papp2(v : @(1), x : @(0), p : (Pred  @(1)  @(0))): (? papp2([p;
                                                                    v;
                                                                    x])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 38, column 8)
qualif Papp3(v : @(2), x : @(0), y : @(1), p : (Pred  @(2)  @(0)  @(1))): (? papp3([p;
                                                                                    v;
                                                                                    x;
                                                                                    y])) // "/Users/benjamin/UCSDrepos/liquidhaskell/include/Prelude.hquals" (line 41, column 8)




constant runFun : (func(2, [(Arrow  @(0)  @(1)); @(0); @(1)]))
constant addrLen : (func(0, [int; int]))
constant xsListSelector : (func(1, [[@(0)]; [@(0)]]))
constant x_Tuple21 : (func(2, [(Tuple  @(0)  @(1)); @(0)]))
constant x_Tuple65 : (func(6, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5));
                               @(4)]))
constant GHC.Types.False$35$68 : (GHC.Types.Bool)
constant x_Tuple55 : (func(5, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4));
                               @(4)]))
constant x_Tuple33 : (func(3, [(Tuple  @(0)  @(1)  @(2)); @(2)]))
constant x_Tuple77 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(6)]))
constant papp3 : (func(6, [(Pred  @(0)  @(1)  @(2));
                           @(3);
                           @(4);
                           @(5);
                           bool]))
constant x_Tuple63 : (func(6, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5));
                               @(2)]))
constant x_Tuple41 : (func(4, [(Tuple  @(0)  @(1)  @(2)  @(3));
                               @(0)]))
constant papp4 : (func(8, [(Pred  @(0)  @(1)  @(2)  @(6));
                           @(3);
                           @(4);
                           @(5);
                           @(7);
                           bool]))
constant x_Tuple64 : (func(6, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5));
                               @(3)]))
constant autolen : (func(1, [@(0); int]))
constant x_Tuple52 : (func(5, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4));
                               @(1)]))
constant null : (func(1, [[@(0)]; bool]))
constant papp2 : (func(4, [(Pred  @(0)  @(1)); @(2); @(3); bool]))
constant x_Tuple62 : (func(6, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5));
                               @(1)]))
constant fromJust : (func(1, [(GHC.Base.Maybe  @(0)); @(0)]))
constant x_Tuple53 : (func(5, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4));
                               @(2)]))
constant x_Tuple71 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(0)]))
constant x_Tuple74 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(3)]))
constant len : (func(2, [(@(0)  @(1)); int]))
constant x_Tuple22 : (func(2, [(Tuple  @(0)  @(1)); @(1)]))
constant x_Tuple66 : (func(6, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5));
                               @(5)]))
constant x_Tuple44 : (func(4, [(Tuple  @(0)  @(1)  @(2)  @(3));
                               @(3)]))
constant xListSelector : (func(1, [[@(0)]; @(0)]))
constant strLen : (func(0, [int; int]))
constant x_Tuple72 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(1)]))
constant isJust : (func(1, [(GHC.Base.Maybe  @(0)); bool]))
constant Prop : (func(0, [GHC.Types.Bool; bool]))
constant x_Tuple31 : (func(3, [(Tuple  @(0)  @(1)  @(2)); @(0)]))
constant x_Tuple75 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(4)]))
constant papp1 : (func(1, [(Pred  @(0)); @(0); bool]))
constant x_Tuple61 : (func(6, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5));
                               @(0)]))
constant x_Tuple43 : (func(4, [(Tuple  @(0)  @(1)  @(2)  @(3));
                               @(2)]))
constant x_Tuple51 : (func(5, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4));
                               @(0)]))
constant GHC.Types.I$35$$35$6c : (func(0, [int; int]))
constant x_Tuple73 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(2)]))
constant x_Tuple54 : (func(5, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4));
                               @(3)]))
constant cmp : (func(0, [GHC.Types.Ordering; GHC.Types.Ordering]))
constant x_Tuple32 : (func(3, [(Tuple  @(0)  @(1)  @(2)); @(1)]))
constant x_Tuple76 : (func(7, [(Tuple  @(0)  @(1)  @(2)  @(3)  @(4)  @(5)  @(6));
                               @(5)]))
constant fst : (func(2, [(Tuple  @(0)  @(1)); @(0)]))
constant snd : (func(2, [(Tuple  @(0)  @(1)); @(1)]))
constant x_Tuple42 : (func(4, [(Tuple  @(0)  @(1)  @(2)  @(3));
                               @(1)]))
constant GHC.Types.True$35$6u : (GHC.Types.Bool)


bind 0 GHC.Types.False$35$68 : {VV$35$170 : GHC.Types.Bool | []}
bind 1 GHC.Types.True$35$6u : {VV$35$172 : GHC.Types.Bool | []}
bind 2 GHC.Num.$36$fNumInt$35$rma : {VV$35$178 : (GHC.Num.Num  int) | []}
bind 3 GHC.Classes.$36$fOrdInt$35$rni : {VV$35$179 : (GHC.Classes.Ord  int) | []}
bind 4 GHC.Types.EQ$35$6U : {VV$35$180 : GHC.Types.Ordering | [(VV$35$180 = GHC.Types.EQ$35$6U)]}
bind 5 GHC.Types.LT$35$6S : {VV$35$181 : GHC.Types.Ordering | [(VV$35$181 = GHC.Types.LT$35$6S)]}
bind 6 GHC.Types.GT$35$6W : {VV$35$182 : GHC.Types.Ordering | [(VV$35$182 = GHC.Types.GT$35$6W)]}
bind 7 GHC.Types.True$35$6u : {v_4 : GHC.Types.Bool | [(? Prop([v_4]))]}
bind 8 GHC.Types.False$35$68 : {v_5 : GHC.Types.Bool | [(~ ((? Prop([v_5]))))]}
bind 9 GHC.Types.False$35$68 : {v_5 : GHC.Types.Bool | [(~ ((? Prop([v_5]))))]}
bind 10 GHC.Types.$91$$93$$35$6m : {VV : func(1, [[@(0)]]) | []}
bind 11 GHC.Types.True$35$6u : {v_4 : GHC.Types.Bool | [(? Prop([v_4]))]}
bind 12 GHC.Types.GT$35$6W : {VV$35$227 : GHC.Types.Ordering | [(cmp([VV$35$227]) = GHC.Types.GT$35$6W)]}
bind 13 GHC.Types.LT$35$6S : {VV$35$228 : GHC.Types.Ordering | [(cmp([VV$35$228]) = GHC.Types.LT$35$6S)]}
bind 14 GHC.Types.EQ$35$6U : {VV$35$229 : GHC.Types.Ordering | [(cmp([VV$35$229]) = GHC.Types.EQ$35$6U)]}
bind 15 GHC.Base.Nothing$35$r1d : {VV : func(1, [(GHC.Base.Maybe  @(0))]) | []}
bind 16 lq_anf__d12p : {lq_tmp_x_238 : int | [(lq_tmp_x_238 = (0  :  int))]}
bind 17 lq_anf__d12q : {lq_tmp_x_244 : int | []}
bind 18 lq_anf__d12r : {lq_tmp_x_250 : int | [(lq_tmp_x_250 = (10  :  int))]}
bind 19 Test0.toss$35$rYP : {VV$35$234 : GHC.Types.Bool | [$k__235]}
bind 20 lq_anf__d12s : {lq_tmp_x_275 : GHC.Types.Bool | [(lq_tmp_x_275 = Test0.toss$35$rYP)]}
bind 21 lq_anf__d12s : {lq_tmp_x_277 : GHC.Types.Bool | [(lq_tmp_x_277 = Test0.toss$35$rYP)]}
bind 22 lq_anf__d12s : {lq_tmp_x_277 : GHC.Types.Bool | [(lq_tmp_x_277 = Test0.toss$35$rYP);
                                                         (~ ((? Prop([lq_tmp_x_277]))));
                                                         (~ ((? Prop([lq_tmp_x_277]))));
                                                         (~ ((? Prop([lq_tmp_x_277]))))]}
bind 23 lq_anf__d12s : {lq_tmp_x_283 : GHC.Types.Bool | [(lq_tmp_x_283 = Test0.toss$35$rYP)]}
bind 24 lq_anf__d12s : {lq_tmp_x_283 : GHC.Types.Bool | [(lq_tmp_x_283 = Test0.toss$35$rYP);
                                                         (? Prop([lq_tmp_x_283]));
                                                         (? Prop([lq_tmp_x_283]));
                                                         (? Prop([lq_tmp_x_283]))]}
bind 25 lq_anf__d12t : {lq_tmp_x_288 : GHC.Types.Bool | [(lq_tmp_x_288 = lq_anf__d12s)]}
bind 26 lq_anf__d12t : {lq_tmp_x_290 : GHC.Types.Bool | [(lq_tmp_x_290 = lq_anf__d12s)]}
bind 27 lq_anf__d12t : {lq_tmp_x_290 : GHC.Types.Bool | [(lq_tmp_x_290 = lq_anf__d12s);
                                                         (~ ((? Prop([lq_tmp_x_290]))));
                                                         (~ ((? Prop([lq_tmp_x_290]))));
                                                         (~ ((? Prop([lq_tmp_x_290]))))]}
bind 28 lq_anf__d12t : {lq_tmp_x_296 : GHC.Types.Bool | [(lq_tmp_x_296 = lq_anf__d12s)]}
bind 29 lq_anf__d12t : {lq_tmp_x_296 : GHC.Types.Bool | [(lq_tmp_x_296 = lq_anf__d12s);
                                                         (? Prop([lq_tmp_x_296]));
                                                         (? Prop([lq_tmp_x_296]));
                                                         (? Prop([lq_tmp_x_296]))]}
bind 30 Test0.prop_abs$35$r10h : {VV$35$272 : GHC.Types.Bool | [$k__273]}
bind 31 x$35$a11A : {VV$35$307 : int | [$k__308]}
bind 32 lq_anf__d12u : {lq_tmp_x_315 : int | [(lq_tmp_x_315 = (0  :  int))]}
bind 33 lq_anf__d12v : {lq_tmp_x_321 : GHC.Types.Bool | [((? Prop([lq_tmp_x_321])) <=> (x$35$a11A > lq_anf__d12u))]}
bind 34 lq_anf__d12w : {lq_tmp_x_345 : int | [$k__343[lq_tmp_x_340:=lq_anf__d12v][VV$35$342:=lq_tmp_x_345][lq_tmp_x_341:=x$35$a11A]]}
bind 35 lq_anf__d12x : {lq_tmp_x_350 : int | [(lq_tmp_x_350 = (1  :  int))]}
bind 36 lq_anf__d12y : {lq_tmp_x_373 : int | [(lq_tmp_x_373 = (12  :  int))]}
bind 37 Test0.goo$35$r10j : {VV$35$369 : int | [$k__370]}
bind 38 zzz$35$a11B : {VV$35$384 : int | [$k__385]}
bind 39 lq_anf__d12z : {lq_tmp_x_392 : int | [(lq_tmp_x_392 = (1  :  int))]}
bind 40 lq_anf__d12A : {lq_tmp_x_415 : int | [(lq_tmp_x_415 = (29  :  int))]}
bind 41 Test0.zoo$35$r10l : {VV$35$411 : int | [$k__412]}
bind 42 VV$35$426 : {VV$35$426 : int | [$k__389[lq_tmp_x_423:=lq_anf__d12A][lq_tmp_x_421:=VV$35$426][zzz$35$a11B:=lq_anf__d12A][VV$35$388:=VV$35$426]]}
bind 43 VV$35$426 : {VV$35$426 : int | [$k__389[lq_tmp_x_423:=lq_anf__d12A][lq_tmp_x_421:=VV$35$426][zzz$35$a11B:=lq_anf__d12A][VV$35$388:=VV$35$426]]}
bind 44 VV$35$429 : {VV$35$429 : int | [(VV$35$429 = lq_anf__d12A)]}
bind 45 VV$35$429 : {VV$35$429 : int | [(VV$35$429 = lq_anf__d12A)]}
bind 46 VV$35$432 : {VV$35$432 : int | [(VV$35$432 = 29)]}
bind 47 VV$35$432 : {VV$35$432 : int | [(VV$35$432 = 29)]}
bind 48 VV$35$435 : {VV$35$435 : int | [(VV$35$435 = (zzz$35$a11B + lq_anf__d12z))]}
bind 49 VV$35$435 : {VV$35$435 : int | [(VV$35$435 = (zzz$35$a11B + lq_anf__d12z))]}
bind 50 VV$35$438 : {VV$35$438 : int | [(VV$35$438 = lq_anf__d12z)]}
bind 51 VV$35$438 : {VV$35$438 : int | [(VV$35$438 = lq_anf__d12z)]}
bind 52 VV$35$441 : {VV$35$441 : int | [(VV$35$441 = zzz$35$a11B)]}
bind 53 VV$35$441 : {VV$35$441 : int | [(VV$35$441 = zzz$35$a11B)]}
bind 54 VV$35$444 : {VV$35$444 : int | [(VV$35$444 = 1)]}
bind 55 VV$35$444 : {VV$35$444 : int | [(VV$35$444 = 1)]}
bind 56 VV$35$447 : {VV$35$447 : int | [$k__312[VV$35$311:=VV$35$447][lq_tmp_x_381:=lq_anf__d12y][x$35$a11A:=lq_anf__d12y][lq_tmp_x_379:=VV$35$447]]}
bind 57 VV$35$447 : {VV$35$447 : int | [$k__312[VV$35$311:=VV$35$447][lq_tmp_x_381:=lq_anf__d12y][x$35$a11A:=lq_anf__d12y][lq_tmp_x_379:=VV$35$447]]}
bind 58 VV$35$450 : {VV$35$450 : int | [(VV$35$450 = lq_anf__d12y)]}
bind 59 VV$35$450 : {VV$35$450 : int | [(VV$35$450 = lq_anf__d12y)]}
bind 60 VV$35$453 : {VV$35$453 : int | [(VV$35$453 = 12)]}
bind 61 VV$35$453 : {VV$35$453 : int | [(VV$35$453 = 12)]}
bind 62 VV$35$456 : {VV$35$456 : int | [(VV$35$456 = (lq_anf__d12w + lq_anf__d12x))]}
bind 63 VV$35$456 : {VV$35$456 : int | [(VV$35$456 = (lq_anf__d12w + lq_anf__d12x))]}
bind 64 VV$35$459 : {VV$35$459 : int | [(VV$35$459 = lq_anf__d12x)]}
bind 65 VV$35$459 : {VV$35$459 : int | [(VV$35$459 = lq_anf__d12x)]}
bind 66 VV$35$462 : {VV$35$462 : int | [(VV$35$462 = lq_anf__d12w)]}
bind 67 VV$35$462 : {VV$35$462 : int | [(VV$35$462 = lq_anf__d12w)]}
bind 68 VV$35$465 : {VV$35$465 : int | [(VV$35$465 = 1)]}
bind 69 VV$35$465 : {VV$35$465 : int | [(VV$35$465 = 1)]}
bind 70 VV$35$468 : {VV$35$468 : int | [(VV$35$468 = x$35$a11A)]}
bind 71 VV$35$468 : {VV$35$468 : int | [(VV$35$468 = x$35$a11A)]}
bind 72 VV$35$471 : {VV$35$471 : GHC.Types.Bool | [(VV$35$471 = lq_anf__d12v)]}
bind 73 VV$35$471 : {VV$35$471 : GHC.Types.Bool | [(VV$35$471 = lq_anf__d12v)]}
bind 74 VV$35$474 : {VV$35$474 : int | [(VV$35$474 = lq_anf__d12u)]}
bind 75 VV$35$474 : {VV$35$474 : int | [(VV$35$474 = lq_anf__d12u)]}
bind 76 VV$35$477 : {VV$35$477 : int | [(VV$35$477 = x$35$a11A)]}
bind 77 VV$35$477 : {VV$35$477 : int | [(VV$35$477 = x$35$a11A)]}
bind 78 VV$35$480 : {VV$35$480 : int | [(VV$35$480 = 0)]}
bind 79 VV$35$480 : {VV$35$480 : int | [(VV$35$480 = 0)]}
bind 80 VV$35$483 : {VV$35$483 : GHC.Types.Bool | [(? Prop([VV$35$483]))]}
bind 81 VV$35$483 : {VV$35$483 : GHC.Types.Bool | [(? Prop([VV$35$483]))]}
bind 82 VV$35$486 : {VV$35$486 : GHC.Types.Bool | [(VV$35$486 = lq_anf__d12t)]}
bind 83 VV$35$486 : {VV$35$486 : GHC.Types.Bool | [(VV$35$486 = lq_anf__d12t)]}
bind 84 VV$35$489 : {VV$35$489 : GHC.Types.Bool | [(VV$35$489 = GHC.Types.False$35$68)]}
bind 85 VV$35$489 : {VV$35$489 : GHC.Types.Bool | [(VV$35$489 = GHC.Types.False$35$68)]}
bind 86 VV$35$492 : {VV$35$492 : GHC.Types.Bool | [(VV$35$492 = GHC.Types.False$35$68)]}
bind 87 VV$35$492 : {VV$35$492 : GHC.Types.Bool | [(VV$35$492 = GHC.Types.False$35$68)]}
bind 88 VV$35$495 : {VV$35$495 : GHC.Types.Bool | [((? Prop([VV$35$495])) <=> (lq_anf__d12q > lq_anf__d12r))]}
bind 89 VV$35$495 : {VV$35$495 : GHC.Types.Bool | [((? Prop([VV$35$495])) <=> (lq_anf__d12q > lq_anf__d12r))]}
bind 90 VV$35$498 : {VV$35$498 : int | [(VV$35$498 = lq_anf__d12r)]}
bind 91 VV$35$498 : {VV$35$498 : int | [(VV$35$498 = lq_anf__d12r)]}
bind 92 VV$35$501 : {VV$35$501 : int | [(VV$35$501 = lq_anf__d12q)]}
bind 93 VV$35$501 : {VV$35$501 : int | [(VV$35$501 = lq_anf__d12q)]}
bind 94 VV$35$504 : {VV$35$504 : int | [(VV$35$504 = 10)]}
bind 95 VV$35$504 : {VV$35$504 : int | [(VV$35$504 = 10)]}
bind 96 VV$35$507 : {VV$35$507 : int | [(VV$35$507 = lq_anf__d12p)]}
bind 97 VV$35$507 : {VV$35$507 : int | [(VV$35$507 = lq_anf__d12p)]}
bind 98 VV$35$510 : {VV$35$510 : int | [(VV$35$510 = 0)]}
bind 99 VV$35$510 : {VV$35$510 : int | [(VV$35$510 = 0)]}
bind 100 VV$35$411 : {VV$35$411 : int | [$k__412]}
bind 101 VV$35$384 : {VV$35$384 : int | [$k__385]}
bind 102 VV$35$388 : {VV$35$388 : int | [$k__389]}
bind 103 VV$35$369 : {VV$35$369 : int | [$k__370]}
bind 104 VV$35$307 : {VV$35$307 : int | [$k__308]}
bind 105 VV$35$342 : {VV$35$342 : int | [$k__343]}
bind 106 VV$35$328 : {VV$35$328 : int | [$k__329]}
bind 107 VV$35$311 : {VV$35$311 : int | [$k__312]}
bind 108 VV$35$272 : {VV$35$272 : GHC.Types.Bool | [$k__273]}
bind 109 VV$35$263 : {VV$35$263 : int | [$k__264]}
bind 110 VV$35$234 : {VV$35$234 : GHC.Types.Bool | [$k__235]}




constraint:
  env [0;
       1;
       2;
       3;
       19;
       4;
       36;
       5;
       6;
       7;
       8;
       9;
       10;
       58;
       11;
       12;
       13;
       14;
       30;
       15]
  lhs {VV$35$F5 : int | [(VV$35$F5 = lq_anf__d12y)]}
  rhs {VV$35$F5 : int | [$k__308[VV$35$307:=VV$35$F5][VV$35$F:=VV$35$F5][VV$35$450:=VV$35$F5][lq_tmp_x_378:=VV$35$F5]]}
  id 5 tag [4]
  // META constraint id 5 : tests/pos/test000.hs:16:11-12


constraint:
  env [0;
       32;
       1;
       33;
       2;
       3;
       19;
       4;
       5;
       6;
       7;
       8;
       72;
       9;
       10;
       11;
       12;
       13;
       14;
       30;
       15;
       31]
  lhs {VV$35$F8 : GHC.Types.Bool | [(VV$35$F8 = lq_anf__d12v)]}
  rhs {VV$35$F8 : GHC.Types.Bool | [(? Prop([VV$35$F8]))]}
  id 8 tag [3]
  // META constraint id 8 : tests/pos/test000.hs:14:23-29


constraint:
  env [0;
       80;
       1;
       2;
       3;
       19;
       4;
       20;
       5;
       6;
       7;
       23;
       8;
       24;
       9;
       25;
       10;
       11;
       12;
       28;
       13;
       29;
       14;
       15]
  lhs {VV$35$F11 : GHC.Types.Bool | [(? Prop([VV$35$F11]))]}
  rhs {VV$35$F11 : GHC.Types.Bool | [$k__273[VV$35$272:=VV$35$F11][VV$35$F:=VV$35$F11][VV$35$483:=VV$35$F11]]}
  id 11 tag [6]
  // META constraint id 11 : tests/pos/test000.hs:10:33-50


constraint:
  env [0;
       1;
       2;
       82;
       3;
       19;
       4;
       20;
       5;
       6;
       7;
       23;
       8;
       24;
       9;
       25;
       10;
       11;
       12;
       28;
       13;
       29;
       14;
       15]
  lhs {VV$35$F12 : GHC.Types.Bool | [(VV$35$F12 = lq_anf__d12t)]}
  rhs {VV$35$F12 : GHC.Types.Bool | [(? Prop([VV$35$F12]))]}
  id 12 tag [6]
  // META constraint id 12 : tests/pos/test000.hs:10:47-50


constraint:
  env [0;
       1;
       2;
       3;
       19;
       4;
       20;
       84;
       5;
       6;
       7;
       23;
       8;
       24;
       9;
       25;
       10;
       26;
       11;
       27;
       12;
       13;
       14;
       15]
  lhs {VV$35$F13 : GHC.Types.Bool | [(VV$35$F13 = GHC.Types.False$35$68)]}
  rhs {VV$35$F13 : GHC.Types.Bool | [$k__273[VV$35$272:=VV$35$F13][VV$35$489:=VV$35$F13][VV$35$F:=VV$35$F13]]}
  id 13 tag [6]
  // META constraint id 13 : tests/pos/test000.hs:10:57-61


constraint:
  env [0;
       1;
       2;
       3;
       19;
       4;
       20;
       5;
       21;
       6;
       22;
       86;
       7;
       8;
       9;
       10;
       11;
       12;
       13;
       14;
       15]
  lhs {VV$35$F14 : GHC.Types.Bool | [(VV$35$F14 = GHC.Types.False$35$68)]}
  rhs {VV$35$F14 : GHC.Types.Bool | [$k__273[VV$35$272:=VV$35$F14][VV$35$F:=VV$35$F14][VV$35$492:=VV$35$F14]]}
  id 14 tag [6]
  // META constraint id 14 : tests/pos/test000.hs:11:19-23


constraint:
  env [0;
       16;
       1;
       17;
       2;
       18;
       3;
       4;
       5;
       6;
       7;
       8;
       88;
       9;
       10;
       11;
       12;
       13;
       14;
       15]
  lhs {VV$35$F15 : GHC.Types.Bool | [((? Prop([VV$35$F15])) <=> (lq_anf__d12q > lq_anf__d12r))]}
  rhs {VV$35$F15 : GHC.Types.Bool | [$k__235[VV$35$F:=VV$35$F15][VV$35$495:=VV$35$F15][VV$35$234:=VV$35$F15]]}
  id 15 tag [5]
  // META constraint id 15 : tests/pos/test000.hs:6:1-22




wf:
  env [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
  reft {VV$35$234 : GHC.Types.Bool | [$k__235]}
  // META wf : <no location info>


wf:
  env [0; 1; 2; 3; 19; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 30; 15]
  reft {VV$35$307 : int | [$k__308]}
  // META wf : <no location info>


wf:
  env [0; 1; 2; 3; 19; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
  reft {VV$35$272 : GHC.Types.Bool | [$k__273]}
  // META wf : tests/pos/test000.hs:(9,1)-(11,23)