Normal Forms

Posted by Ranjit Jhala Sep 5, 2016

Tags: measures

I have been preparing an undergraduate course on Compilers in which we build a compiler that crunches an ML-like language to X86 assembly. One of my favorite steps in the compilation is the conversion to A-Normal Form (ANF) where, informally speaking, each call or primitive operation’s arguments are immediate values, i.e. constants or variable lookups whose values can be loaded with a single machine instruction. For example, the expression

25: ((2 + 3) * (12 - 4)) * (7 + 8)

has the A-Normal Form:

31: let anf0 = 2 + 3
32:     anf1 = 12 - 4
33:     anf2 = anf0 * anf1
34:     anf3 = 7 + 8
35: in
36:     anf2 * anf3

The usual presentation of ANF conversion is very elegant but relies upon a clever use of continuations. Lets look at another perhaps simpler approach, where we can use refinements to light the way.

Source Language

Lets commence by defining the source language that we wish to work with:

82: data Expr
83:   = EInt  Int               -- ^ Integers
84:   | EVar  Var               -- ^ Variables
85:   | EBin  Op   Expr Expr    -- ^ Binary Operators
86:   | ELet  Var  Expr Expr    -- ^ Let-binders
87:   | ELam  Var  Expr         -- ^ Function definitions
88:   | EApp  Expr Expr         -- ^ Function applications
89:   deriving ((GHC.Show.Show ANF.Expr)Show)

The language, defined by Expr has integers, variables, binary operators, let-binders and function definitions (lambdas) and calls (applications). In the above, Var and Op are simply:

97: type Var = String
98: 
99: data Op  = Plus | Minus | Times
100:          deriving ((GHC.Show.Show ANF.Op)Show)

For example, the source expression above corresponds to the value:

106: -- ((2 + 3) * (12 - 4)) * (7 + 8)
107: srcExpr :: Expr
108: {VV : ANF.Expr | VV /= ANF.e1
                 && VV /= ANF.e2
                 && VV /= ANF.e2'
                 && VV /= ANF.e3
                 && ((Prop : func(0, [GHC.Types.Bool;
                                      bool])) ((isImm : func(0, [ANF.Expr;
                                                                 GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false)}srcExpr = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Times
109:             ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Times
110:               ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Plus  ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt  2) ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 3))
111:               ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Minus ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 12) ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 4)))
112:             ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Plus ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 7) ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 8))

A-Normal Form

Before we can describe a conversion to A-Normal Form (ANF), we must pin down what ANF is. Our informal description was: ``each call or primitive operation’s arguments are immediate values, i.e. constants or variable lookups’’.

We could define a brand new datatypes, say IExpr and AExpr whose values correspond to immediate and ANF terms. (Try it, as an exercise.) Unfortunately, doing so leads to a bunch of code duplication, e.g. duplicate printers for Expr and AExpr. Instead, lets see how we can use refinements to carve out suitable subsets.

Immediate Expressions

An Expr is immediate if it is a Number or a Var; we can formalize this as a Haskell predicate:

136: {-@ measure isImm @-}
137: isImm :: Expr -> Bool
138: x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isImm x1)}isImm (EInt _) = True
139: isImm (EVar _) = True
140: isImm _        = False

and then we can use the predicate to define a refinement type for immediate expressions:

147: {-@ type ImmExpr = {v:Expr | isImm v} @-}

For example, e1 is immediate but e2 is not:

153: {-@ e1 :: ImmExpr @-}
154: {v : ANF.Expr | Prop (isImm v)}e1 = {v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 7
155: 
156: {-@ e2 :: ImmExpr @-}
157: {v : ANF.Expr | Prop (isImm v)}e2 = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Plus e1 e1

ANF Expressions

Similiarly, an Expr is in ANF if all arguments for operators and applications are immediate. Once again, we can formalize this intuition as a Haskell predicate:

167: {-@ measure isAnf @-}
168: isAnf :: Expr -> Bool
169: x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf (EInt {})      = True
170: isAnf (EVar {})      = True
171: isAnf (EBin _ e1 e2) = {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e1 {v : x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x1
                                                                                && Prop x2} | v == GHC.Classes.&&}&& {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e2  -- args for operators
172: isAnf (EApp e1 e2)   = {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e1 {v : x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x1
                                                                                && Prop x2} | v == GHC.Classes.&&}&& {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e2  -- must be immediate,
173: isAnf (ELet _ e1 e2) = x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf e1 {v : x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x1
                                                                                && Prop x2} | v == GHC.Classes.&&}&& x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf e2  -- and sub-expressions
174: isAnf (ELam _ e)     = x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf e               -- must be in ANF

and then use the predicate to define the subset of legal ANF expressions:

180: {-@ type AnfExpr = {v:Expr | isAnf v} @-}

For example, e2 above is in ANF but e3 is not:

186: {-@ e2' :: AnfExpr @-}
187: {v : ANF.Expr | Prop (isAnf v)}e2' = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Plus e1 e1
188: 
189: {-@ e3 :: AnfExpr @-}
190: {v : ANF.Expr | Prop (isAnf v)}e3 = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin Plus e2' e2'

ANF Conversion: Intuition

Now that we have clearly demarcated the territories belonging to plain Expr, immediate ImmExpr and A-Normal AnfExpr, lets see how we can convert the former to the latter.

Recall that our goal is to convert expressions like

203: ((2 + 3) * (12 - 4)) * (7 + 8)

into

209: let anf0 = 2 + 3
210:     anf1 = 12 - 4
211:     anf2 = anf0 * anf1
212:     anf3 = 7 + 8
213: in
214:     anf2 * anf3

Generalising a bit, we want to convert

220: e1 + e2

into

226: let x1  = a1  ... xn  = an
227:     x1' = a1' ... xm' = am'
228: in
229:     v1 + v2

where, v1 and v2 are immediate, and ai are ANF.

Making Arguments Immediate

In other words, the key requirement is a way to crunch arbitrary argument expressions like e1 into a pair

240: ([(x1, a1) ... (xn, an)], v1)

where

  1. a1...an are AnfExpr, and
  2. v1 is an immediate ImmExpr

such that e1 is equivalent to let x1 = a1 ... xn = an in v1. Thus, we need a function

252: imm :: Expr -> ([(Var, AnfExpr)], ImmExpr)

which we will use to make arguments immediate thereby yielding a top level conversion function

259: anf :: Expr -> AnfExpr

As we need to generate “temporary” intermediate binders, it will be convenient to work within a monad that generates fresh variables:

267: type AnfM a = State Int a
268: 
269: fresh :: AnfM Var
270: (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {VV : [GHC.Types.Char] | (len : func(2, [(@(0)  @(1));
                                                                                                                             int])) (VV : [@(0)]) > 0
                                                                                                             && (len : func(2, [(@(0)  @(1));
                                                                                                                                int])) (VV : [@(0)]) >= 0})fresh = do
271:   GHC.Types.Intn <- (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity GHC.Types.Int)get
272:   GHC.Types.Int -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ())put (GHC.Types.Intnx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+1)
273:   [GHC.Types.Char] -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity [GHC.Types.Char])return ([GHC.Types.Char]"anf" ++ GHC.Types.Int -> [GHC.Types.Char]show n)

Thus, the conversion functions will have the types:

279: anf :: Expr -> AnfM AnfExpr
280: imm :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr)

ANF Conversion: Code

We can now define the top-level conversion thus:

289: --------------------------------------------------------------------------------
290: {-@ anf :: Expr -> AnfM AnfExpr @-}
291: --------------------------------------------------------------------------------
292: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf (EInt n) =
293:   ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt n)
294: 
295: anf (EVar x) =
296:   ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                         && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar x)
297: 
298: anf (ELet x e1 e2) = do
299:   {v : ANF.Expr | Prop (isAnf v)}a1 <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e1
300:   {v : ANF.Expr | Prop (isAnf v)}a2 <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e2
301:   ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : [GHC.Types.Char] -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                                       && (Prop (isAnf v) <=> Prop (isAnf x2)
                                                                                              && Prop (isAnf x3))} | v == ANF.ELet}ELet x a1 a2)
302: 
303: anf (EBin o e1 e2) = do
304:   (b1s, v1) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e1
305:   (b2s, v2) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e2
306:   ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet ({v : [([GHC.Types.Char], ANF.Expr)] | len v == len b1s + len b2s}b1s ++ b2s) ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin o v1 v2))
307: 
308: anf (ELam x e) = do
309:   {v : ANF.Expr | Prop (isAnf v)}a <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e
310:   ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : [GHC.Types.Char] -> x2:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                        && (Prop (isAnf v) <=> Prop (isAnf x2))} | v == ANF.ELam}ELam x a)
311: 
312: anf (EApp e1 e2) = do
313:   (b1s, v1) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e1
314:   (b2s, v2) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e2
315:   ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet ({v : [([GHC.Types.Char], ANF.Expr)] | len v == len b1s + len b2s}b1s ++ b2s) ({v : x1:ANF.Expr -> x2:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                   && (Prop (isAnf v) <=> Prop (isImm x1)
                                                                          && Prop (isImm x2))} | v == ANF.EApp}EApp v1 v2))

In anf the real work happens inside imm which takes an arbitary argument expression and makes it immediate by generating temporary (ANF) bindings. The resulting bindings (and immediate values) are composed by the helper mkLet that takes a list of binders and a body AnfExpr and stitches them into a single AnfExpr:

325: {-@ mkLet :: [(Var, AnfExpr)] -> AnfExpr -> AnfExpr @-}
326: [([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet []         {v : ANF.Expr | Prop (isAnf v)}e' = e'
327: mkLet ((x,e):bs) e' = {v : [GHC.Types.Char] -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                                       && (Prop (isAnf v) <=> Prop (isAnf x2)
                                                                                              && Prop (isAnf x3))} | v == ANF.ELet}ELet x e ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet bs e')

The arguments are made immediate by imm defined as:

333: --------------------------------------------------------------------------------
334: {-@ imm :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr) @-}
335: --------------------------------------------------------------------------------
336: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm (EInt n)       = ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return ([], {v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                      && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt n)
337: imm (EVar x)       = ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return ([], {v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                         && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar x)
338: imm e@(ELet {})    = ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))immExpr e
339: imm e@(ELam {})    = ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))immExpr e
340: imm (EBin o e1 e2) = ANF.Expr -> ANF.Expr -> (x4:{VV : ANF.Expr | VV /= ANF.srcExpr
                                             && ((Prop : func(0, [GHC.Types.Bool;
                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                             GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                            GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x5:{VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                                                        && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                             bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                        GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && VV /= x5
                                                                                                                                                                                                                                                                                                && VV /= ANF.e2
                                                                                                                                                                                                                                                                                                && VV /= x4
                                                                                                                                                                                                                                                                                                && VV /= ANF.e1}) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ({VV : [([GHC.Types.Char], {VV : ANF.Expr | ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)})] | (len : func(2, [(@(0)  @(1));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             int])) (VV : [@(0)]) > 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (len : func(2, [(@(0)  @(1));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                int])) (VV : [@(0)]) >= 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (VV : @(43)) == ((fst : func(0, [(Tuple  @(43)  @(44));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 @(43)])) (VV : (Tuple  @(45)  @(44))) : @(43))}, {VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (VV : @(42)) == ((snd : func(0, [(Tuple  @(45)  @(42));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       @(42)])) (VV : (Tuple  @(45)  @(44))) : @(42))}))imm2 e1 e2 ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                             && (Prop (isAnf v) <=> Prop (isImm x2)
                                                                                    && Prop (isImm x3))} | v == ANF.EBin}EBin o)
341: imm (EApp e1 e2)   = ANF.Expr -> ANF.Expr -> (x4:{VV : ANF.Expr | VV /= ANF.srcExpr
                                             && ((Prop : func(0, [GHC.Types.Bool;
                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                             GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                            GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x5:{VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                                                        && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                             bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                        GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && VV /= x5
                                                                                                                                                                                                                                                                                                && VV /= ANF.e2
                                                                                                                                                                                                                                                                                                && VV /= x4
                                                                                                                                                                                                                                                                                                && VV /= ANF.e1}) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ({VV : [([GHC.Types.Char], {VV : ANF.Expr | ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)})] | (len : func(2, [(@(0)  @(1));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             int])) (VV : [@(0)]) > 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (len : func(2, [(@(0)  @(1));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                int])) (VV : [@(0)]) >= 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (VV : @(43)) == ((fst : func(0, [(Tuple  @(43)  @(44));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 @(43)])) (VV : (Tuple  @(45)  @(44))) : @(43))}, {VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (VV : @(42)) == ((snd : func(0, [(Tuple  @(45)  @(42));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       @(42)])) (VV : (Tuple  @(45)  @(44))) : @(42))}))imm2 e1 e2 {v : x1:ANF.Expr -> x2:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false)
                                                   && (Prop (isAnf v) <=> Prop (isImm x1)
                                                                          && Prop (isImm x2))} | v == ANF.EApp}EApp
  • Numbers and variables are already immediate, and are returned directly.

  • Let-binders and lambdas are simply converted to ANF, and assigned to a fresh binder:

350: {-@ immExpr :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr) @-}
351: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))immExpr ANF.Expre = do
352:   {v : ANF.Expr | Prop (isAnf v)}a <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e
353:   {v : [GHC.Types.Char] | (len : func(2, [(@(0)  @(1));
                                        int])) (v : [@(0)]) > 0
                        && (len : func(2, [(@(0)  @(1)); int])) (v : [@(0)]) >= 0}t <- fresh
354:   ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return ([(t, a)], {v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                         && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar t)
  • Finally, binary operators and applications are converted by imm2 that takes two arbitrary expressions and an expression constructor, yielding the anf-binders and immediate expression.
362: imm2 :: Expr -> Expr -> (ImmExpr -> ImmExpr -> AnfExpr)
363:      -> AnfM ([(Var, AnfExpr)], ImmExpr)
364: ANF.Expr -> ANF.Expr -> (x4:{VV : ANF.Expr | VV /= ANF.srcExpr
                                             && ((Prop : func(0, [GHC.Types.Bool;
                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                             GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                            GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x5:{VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                                                        && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                             bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                        GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                        && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                     bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                && VV /= x5
                                                                                                                                                                                                                                                                                                && VV /= ANF.e2
                                                                                                                                                                                                                                                                                                && VV /= x4
                                                                                                                                                                                                                                                                                                && VV /= ANF.e1}) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ({VV : [([GHC.Types.Char], {VV : ANF.Expr | ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                     && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                         bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)})] | (len : func(2, [(@(0)  @(1));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             int])) (VV : [@(0)]) > 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (len : func(2, [(@(0)  @(1));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                int])) (VV : [@(0)]) >= 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             && (VV : @(43)) == ((fst : func(0, [(Tuple  @(43)  @(44));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 @(43)])) (VV : (Tuple  @(45)  @(44))) : @(43))}, {VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   && (VV : @(42)) == ((snd : func(0, [(Tuple  @(45)  @(42));
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       @(42)])) (VV : (Tuple  @(45)  @(44))) : @(42))}))imm2 ANF.Expre1 ANF.Expre2 x1:{VV : ANF.Expr | VV /= ANF.srcExpr
                    && ((Prop : func(0, [GHC.Types.Bool;
                                         bool])) ((isImm : func(0, [ANF.Expr;
                                                                    GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                    && (Prop : func(0, [GHC.Types.Bool;
                                        bool])) ((isImm : func(0, [ANF.Expr;
                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x2:{VV : ANF.Expr | VV /= ANF.srcExpr
                                                                                                                                               && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                    bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                               GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                              GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false)
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                               && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                   bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                              GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                           GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && VV /= x2
                                                                                                                                                                                                                                                                       && VV /= ANF.e2
                                                                                                                                                                                                                                                                       && VV /= x1
                                                                                                                                                                                                                                                                       && VV /= ANF.e1}f = do
365:   (b1s, v1) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e1
366:   (b2s, v2) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e2
367:   {v : [GHC.Types.Char] | (len : func(2, [(@(0)  @(1));
                                        int])) (v : [@(0)]) > 0
                        && (len : func(2, [(@(0)  @(1)); int])) (v : [@(0)]) >= 0}t         <- fresh
368:   let [([GHC.Types.Char], ANF.Expr)]bs'    = [([GHC.Types.Char], ANF.Expr)]b1s ++ [([GHC.Types.Char], ANF.Expr)]b2s ++ [(t, {v : x1:{v : ANF.Expr | v /= ANF.srcExpr
                        && ((Prop : func(0, [GHC.Types.Bool;
                                             bool])) ((isImm : func(0, [ANF.Expr;
                                                                        GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> true)
                        && (Prop : func(0, [GHC.Types.Bool;
                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool)} -> x2:{v : ANF.Expr | v /= ANF.srcExpr
                                                                                                                                                 && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                      bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                 GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                 && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                     bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool)} -> {v : ANF.Expr | (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                        bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                   GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> false)
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)
                                                                                                                                                                                                                                                                                                                                                                              && (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                                  bool])) ((isImm : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                             GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> true)
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && ((Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                            bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                       GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool;
                                                                                                                                                                                                                                                                                                                                                                                               bool])) ((isAnf : func(0, [ANF.Expr;
                                                                                                                                                                                                                                                                                                                                                                                                                          GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool))
                                                                                                                                                                                                                                                                       && v /= x2
                                                                                                                                                                                                                                                                       && v /= ANF.e2
                                                                                                                                                                                                                                                                       && v /= x1
                                                                                                                                                                                                                                                                       && v /= ANF.e1} | v == f}f v1 v2)]
369:   ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return      (bs', {v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true)
                                         && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar t)

You can run it thus:

376: toAnf :: Expr -> AnfExpr
377: ANF.Expr -> ANF.ExprtoAnf ANF.Expre = GHC.Types.Int -> ANF.ExprevalState (ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e) 0
381: ghci> toAnf srcExpr
382: ELet "anf0" (EBin Plus (EInt 2) (EInt 3))
383:  (ELet "anf1" (EBin Minus (EInt 12) (EInt 4))
384:    (ELet "anf2" (EBin Times (EVar "anf0") (EVar "anf1"))
385:      (ELet "anf3" (EBin Plus (EInt 7) (EInt 8))
386:        (EBin Times (EVar "anf2") (EVar "anf3")))))

which, can be pretty-printed to yield exactly the outcome desired at the top:

392: let anf0 = 2 + 3
393:     anf1 = 12 - 4
394:     anf2 = anf0 * anf1
395:     anf3 = 7 + 8
396: in
397:     anf2 * anf3

There! The refinements make this tricky conversion quite straightforward and natural, without requiring us to duplicate types and code. As an exercise, can you use refinements to:

  1. Port the classic continuation-based conversion ?
  2. Check that the conversion yields well-scoped terms ?