# Normal Forms

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 ?
Ranjit Jhala
2016-09-05