[Compiler.saveBase] size: 7
    def f1 c a b : Nat :=
      cases c : Nat
      | Bool.false =>
        let _x.1 := Nat.add a b;
        return _x.1
      | Bool.true =>
        let _x.2 := Nat.add a b;
        let _x.3 := Nat.mul b a;
        let _x.4 := Nat.add _x.2 _x.3;
        return _x.4
[Compiler.saveBase] size: 7
    def f2 c a b : Nat :=
      cases c : Nat
      | Bool.false =>
        let _x.1 := Nat.add a b;
        return _x.1
      | Bool.true =>
        let _x.2 := Nat.add a b;
        let _x.3 := Nat.mul b a;
        let _x.4 := Nat.add _x.2 _x.3;
        return _x.4
[Compiler.saveBase] size: 22
    def f3 c c' a b : Nat :=
      jp _jp.1 y z : Nat :=
        let _x.2 := Nat.add y z;
        let _x.3 := Nat.mul z y;
        let _x.4 := Nat.add _x.2 _x.3;
        return _x.4;
      jp _jp.5 y z : Nat :=
        let _x.6 := Nat.add z y;
        let _x.7 := Nat.add _x.6 y;
        return _x.7;
      jp _jp.8 y z d : Nat :=
        cases d : Nat
        | C.c1 =>
          goto _jp.1 y z
        | C.c3 =>
          let _x.9 := Nat.mul y y;
          let _x.10 := Nat.add _x.9 a;
          return _x.10
        | _ =>
          goto _jp.5 y z;
      cases c : Nat
      | C.c1 =>
        goto _jp.1 a b
      | C.c2 =>
        goto _jp.5 b b
      | C.c3 =>
        goto _jp.8 b a c'
      | C.c4 =>
        goto _jp.8 a a c'