{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.Tree.AVL.Indexed where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.DifferenceList
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Tree.AVL.Height
import qualified MAlonzo.Code.Data.Tree.AVL.Key
import qualified MAlonzo.Code.Data.Tree.AVL.Value
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.Tree.AVL.Indexed._._<_<_
d__'60'_'60'__88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__88 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._._<⁺_
d__'60''8314'__90 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__90 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._._≈∙_
d__'8776''8729'__92 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__92 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._.Key⁺
d_Key'8314'_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 -> ()
d_Key'8314'_94 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_864 -> T_Level_18
d_Key'8314'_94 = T_Level_18
-> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_864 -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.irrefl⁺
d_irrefl'8314'_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl'8314'_96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_'8869'_4
d_irrefl'8314'_96 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_'8869'_4
forall a. a
erased
-- Data.Tree.AVL.Indexed._.refl⁺
d_refl'8314'_98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_98 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_98 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_98 T_StrictTotalOrder_864
v3
du_refl'8314'_98 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_98 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_98 T_StrictTotalOrder_864
v0
  = (T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> AgdaAny -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_refl'8314'_88 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
-- Data.Tree.AVL.Indexed._.strictPartialOrder
d_strictPartialOrder_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_strictPartialOrder_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictPartialOrder_472
d_strictPartialOrder_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3
  = T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
du_strictPartialOrder_100 T_StrictTotalOrder_864
v3
du_strictPartialOrder_100 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_strictPartialOrder_100 :: T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
du_strictPartialOrder_100 T_StrictTotalOrder_864
v0
  = (T_StrictTotalOrder_864 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe
      T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
MAlonzo.Code.Data.Tree.AVL.Key.du_strictPartialOrder_112 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
-- Data.Tree.AVL.Indexed._.strictTotalOrder
d_strictTotalOrder_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_strictTotalOrder_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictTotalOrder_864
d_strictTotalOrder_102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_strictTotalOrder_102 T_StrictTotalOrder_864
v3
du_strictTotalOrder_102 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
du_strictTotalOrder_102 :: T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_strictTotalOrder_102 T_StrictTotalOrder_864
v0
  = (T_StrictTotalOrder_864 -> T_StrictTotalOrder_864)
-> AgdaAny -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
MAlonzo.Code.Data.Tree.AVL.Key.du_strictTotalOrder_182 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
-- Data.Tree.AVL.Indexed._.sym⁺
d_sym'8314'_104 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_sym'8314'_104 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_104 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_104 T_StrictTotalOrder_864
v3
du_sym'8314'_104 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_sym'8314'_104 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_104 T_StrictTotalOrder_864
v0
  = (T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_sym'8314'_94 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
-- Data.Tree.AVL.Indexed._.trans⁺
d_trans'8314'_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_trans'8314'_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_106 T_StrictTotalOrder_864
v3
du_trans'8314'_106 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_trans'8314'_106 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_106 T_StrictTotalOrder_864
v0
  = (T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
forall a b. a -> b
coe T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_102 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
-- Data.Tree.AVL.Indexed._.⊥⁺<[_]<⊤⁺
d_'8869''8314''60''91'_'93''60''8868''8314'_108 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_108 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_108 ~T_StrictTotalOrder_864
v0 ~AgdaAny
v1
  = T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_108
du_'8869''8314''60''91'_'93''60''8868''8314'_108 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_108 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_108
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
         (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
            T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
      (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
         T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)
-- Data.Tree.AVL.Indexed._.Extrema.[_]-injective
d_'91'_'93''45'injective_124 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'_'93''45'injective_124 :: T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'91'_'93''45'injective_124 = T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Tree.AVL.Indexed._.K&_
d_K'38'__130 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_K'38'__130 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._.Value
d_Value_134 :: p -> p -> p -> p -> p -> T_Level_18
d_Value_134 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Data.Tree.AVL.Indexed._.const
d_const_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
d_const_136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 = T_Level_18 -> T_Level_18 -> T_Value_38
du_const_136
du_const_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_136 :: T_Level_18 -> T_Level_18 -> T_Value_38
du_const_136 T_Level_18
v0 T_Level_18
v1
  = T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94
-- Data.Tree.AVL.Indexed._.fromPair
d_fromPair_138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
d_fromPair_138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_138 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 = T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_138
du_fromPair_138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
du_fromPair_138 :: T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_138 T_Level_18
v0 T_Value_38
v1 T_Σ_14
v2
  = (T_Σ_14 -> T_K'38'__56) -> T_Σ_14 -> T_K'38'__56
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_86 T_Σ_14
v2
-- Data.Tree.AVL.Indexed._.key
d_key_140 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_140 :: T_K'38'__56 -> AgdaAny
d_key_140 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.toPair
d_toPair_142 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_142 :: T_K'38'__56 -> T_Σ_14
d_toPair_142 = (T_K'38'__56 -> T_Σ_14) -> T_K'38'__56 -> T_Σ_14
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80
-- Data.Tree.AVL.Indexed._.value
d_value_144 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_144 :: T_K'38'__56 -> AgdaAny
d_value_144 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.K&_.key
d_key_148 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_148 :: T_K'38'__56 -> AgdaAny
d_key_148 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.K&_.value
d_value_150 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_150 :: T_K'38'__56 -> AgdaAny
d_value_150 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.Value.family
d_family_154 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_154 :: T_Value_38 -> AgdaAny -> T_Level_18
d_family_154 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.Value.respects
d_respects_156 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_156 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_156 T_Value_38
v0
  = (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
-- Data.Tree.AVL.Indexed.Tree
d_Tree_166 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Tree_166 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_Tree_166
  = C_leaf_178 MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 |
    C_node_194 Integer Integer
               MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 T_Tree_166 T_Tree_166
               MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30
-- Data.Tree.AVL.Indexed._.ordered
d_ordered_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_166 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_ordered_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T__'60''8314'__20
d_ordered_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_166
v9
  = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 T_Tree_166
v9
du_ordered_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  T_Tree_166 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_ordered_210 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 T_Tree_166
v3
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
      C_leaf_178 T__'60''8314'__20
v4 -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v4
      C_node_194 Integer
v4 Integer
v5 T_K'38'__56
v7 T_Tree_166
v8 T_Tree_166
v9 T__'8764'_'8852'__30
v10
        -> (T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'60''8314'__20
forall a b. a -> b
coe
             T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_102 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1
             ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
             Maybe (Maybe AgdaAny)
v2
             ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
                (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v8))
             ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
                (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v9))
      T_Tree_166
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.Val
d_Val_222 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_222 :: T_Value_38 -> AgdaAny -> T_Level_18
d_Val_222 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.V≈
d_V'8776'_224 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_224 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_224 T_Value_38
v0
  = (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
-- Data.Tree.AVL.Indexed._.leaf-injective
d_leaf'45'injective_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_leaf'45'injective_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
d_leaf'45'injective_234 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Tree.AVL.Indexed._.node-injective-key
d_node'45'injective'45'key_266 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_166 ->
  T_Tree_166 ->
  T_Tree_166 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_node'45'injective'45'key_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__56
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
d_node'45'injective'45'key_266 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__56
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Tree.AVL.Indexed._.castˡ
d_cast'737'_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_166 -> T_Tree_166
d_cast'737'_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
d_cast'737'_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T__'60''8314'__20
v10 T_Tree_166
v11
  = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
du_cast'737'_276 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T__'60''8314'__20
v10 T_Tree_166
v11
du_cast'737'_276 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_166 -> T_Tree_166
du_cast'737'_276 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
du_cast'737'_276 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4 T_Tree_166
v5
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v5 of
      C_leaf_178 T__'60''8314'__20
v6
        -> (T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> T_Tree_166
forall a b. a -> b
coe
             T__'60''8314'__20 -> T_Tree_166
C_leaf_178
             ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_102 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4
                T__'60''8314'__20
v6)
      C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12
        -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9
             ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T_Tree_166
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
du_cast'737'_276 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9))))
                (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v4) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v10))
             T_Tree_166
v11 T__'8764'_'8852'__30
v12
      T_Tree_166
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.castʳ
d_cast'691'_302 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_166 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_166
d_cast'691'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
d_cast'691'_302 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T_Tree_166
v10 T__'60''8314'__20
v11
  = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T_Tree_166
v10 T__'60''8314'__20
v11
du_cast'691'_302 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  T_Tree_166 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_166
du_cast'691'_302 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T_Tree_166
v4 T__'60''8314'__20
v5
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v4 of
      C_leaf_178 T__'60''8314'__20
v6
        -> (T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> T_Tree_166
forall a b. a -> b
coe
             T__'60''8314'__20 -> T_Tree_166
C_leaf_178
             ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_102 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v6
                T__'60''8314'__20
v5)
      C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12
        -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_166
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10
             ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9))))
                (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11) (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v5))
             T__'8764'_'8852'__30
v12
      T_Tree_166
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinˡ⁺
d_join'737''8314'_352 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8314'_352 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8314'_352 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Σ_14
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
du_join'737''8314'_352 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8314'_352 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_166
v4 T__'8764'_'8852'__30
v5
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
        -> case AgdaAny -> T_Fin_6
forall a b. a -> b
coe AgdaAny
v6 of
             T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                    (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                    ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                       Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                       (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                          (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                       Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4 T__'8764'_'8852'__30
v5)
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v9
               -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
v9)
                    (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                 (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                       T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4
                                 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                 (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                       T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 Integer
v0 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4
                                 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                         -> case AgdaAny -> T_Tree_166
forall a b. a -> b
coe AgdaAny
v7 of
                              C_node_194 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_166
v15 T_Tree_166
v16 T__'8764'_'8852'__30
v17
                                -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v17 of
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                       -> case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v16 of
                                            C_node_194 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_166
v23 T_Tree_166
v24 T__'8764'_'8852'__30
v25
                                              -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                                   ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                      Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v22
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v1 Integer
v19 T_K'38'__56
v14 T_Tree_166
v15 T_Tree_166
v23
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_max'8764'_50
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v20 Integer
v1 T_K'38'__56
v2 T_Tree_166
v24 T_Tree_166
v4
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_'8764'max_58
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                         T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                            T_Tree_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                               (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v14 T_Tree_166
v15
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                                  Integer
v1 T_K'38'__56
v2 T_Tree_166
v16 T_Tree_166
v4
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                  T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v14 T_Tree_166
v15
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v1 Integer
v1 T_K'38'__56
v2 T_Tree_166
v16 T_Tree_166
v4
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                     T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_Tree_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_6
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinʳ⁺
d_join'691''8314'_442 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'691''8314'_442 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8314'_442 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Tree_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8314'_442 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'691''8314'_442 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_166
v3 T_Σ_14
v4 T__'8764'_'8852'__30
v5
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
        -> case AgdaAny -> T_Fin_6
forall a b. a -> b
coe AgdaAny
v6 of
             T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                    (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                    ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                       Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
                       (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                          (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                       T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v9
               -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
v9)
                    (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                         -> case AgdaAny -> T_Tree_166
forall a b. a -> b
coe AgdaAny
v7 of
                              C_node_194 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_166
v15 T_Tree_166
v16 T__'8764'_'8852'__30
v17
                                -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v17 of
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v14
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0 Integer
v0 T_K'38'__56
v2 T_Tree_166
v3 T_Tree_166
v15
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                               T_Tree_166
v16
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                               (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v14
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
                                                  (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v2 T_Tree_166
v3 T_Tree_166
v15
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                                               T_Tree_166
v16
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                  T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                       -> case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v15 of
                                            C_node_194 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_166
v23 T_Tree_166
v24 T__'8764'_'8852'__30
v25
                                              -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                                   ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                      Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v22
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0 Integer
v19 T_K'38'__56
v2 T_Tree_166
v3 T_Tree_166
v23
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_max'8764'_50
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v20 Integer
v0 T_K'38'__56
v14 T_Tree_166
v24 T_Tree_166
v16
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_'8764'max_58
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                         T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                            T_Tree_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_Tree_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
                                 (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                       T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                 (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                       T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                 T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                       T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_6
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinˡ⁻
d_join'737''8315'_518 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8315'_518 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8315'_518 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Σ_14
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
du_join'737''8315'_518 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8315'_518 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_166
v4 T__'8764'_'8852'__30
v5
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
               -> case AgdaAny -> T_Fin_6
forall a b. a -> b
coe AgdaAny
v6 of
                    T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
                      -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                           ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                              (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                           ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                              Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                              (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                 (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                              Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4 T__'8764'_'8852'__30
v5)
                    MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v9
                      -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
v9)
                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                 (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                    ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                       T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                                 Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4 T__'8764'_'8852'__30
v5))
                    T_Fin_6
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
                  -> case AgdaAny -> T_Fin_6
forall a b. a -> b
coe AgdaAny
v7 of
                       T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
                         -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442
                                     ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                        (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))
                                     (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                        ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                           (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                        (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4))
                                     (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34)
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                        (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                        (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                        Integer
v0 T_K'38'__56
v2 AgdaAny
v8 T_Tree_166
v4
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                        (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                        Integer
v6 T_K'38'__56
v2 AgdaAny
v8 T_Tree_166
v4
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                              T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v10
                         -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
v10)
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                    (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                 ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                    Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
                                    (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                       ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                          T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                          (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                    Integer
v1 T_K'38'__56
v2 AgdaAny
v8 T_Tree_166
v4 T__'8764'_'8852'__30
v5))
                       T_Fin_6
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL.Indexed._.joinʳ⁻
d_join'691''8315'_580 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'691''8315'_580 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8315'_580 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Tree_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8315'_580 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'691''8315'_580 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_166
v3 T_Σ_14
v4 T__'8764'_'8852'__30
v5
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
               -> case AgdaAny -> T_Fin_6
forall a b. a -> b
coe AgdaAny
v6 of
                    T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
                      -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                           ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                              (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                           ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                              Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
                              (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                 (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                              T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
                    MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v9
                      -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
v9)
                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
                                 (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                    ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                       T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                                 T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5))
                    T_Fin_6
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
                  -> case AgdaAny -> T_Fin_6
forall a b. a -> b
coe AgdaAny
v7 of
                       T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
                         -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6
                                        (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                        T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v8
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                        (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v1
                                        (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                        T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v8
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
                                     ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                        (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1))
                                     (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v2)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                        ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                           (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                        (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
                                     (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42)
                              T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v10
                         -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
v10)
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                    (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                 ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                    Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
                                    (T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                       ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
                                          T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                          (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                    T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v8 T__'8764'_'8852'__30
v5))
                       T_Fin_6
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL.Indexed._.headTail
d_headTail_634 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_634 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T_Σ_14
d_headTail_634 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_166
v9
  = Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 Integer
v8 T_Tree_166
v9
du_headTail_634 ::
  Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_634 :: Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 Integer
v0 T_Tree_166
v1
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1 of
      C_node_194 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_166
v6 T_Tree_166
v7 T__'8764'_'8852'__30
v8
        -> let v9 :: b
v9
                 = let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   AgdaAny -> b
forall a b. a -> b
coe
                     (let v10 :: t
v10 = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v12 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v6 of
                C_leaf_178 T__'60''8314'__20
v10
                  -> let v11 :: b
v11
                           = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2 of
                               AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                   let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                   AgdaAny -> b
forall a b. a -> b
coe
                                     (let v12 :: t
v12 = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6) in
                                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
                                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v14 of
                                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)
                                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                               Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                                                               (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)
                                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
                               AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v9 in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v8 of
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                            -> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
                                 AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                     case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3 of
                                       AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                           (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                             ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                                ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                                   (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)))
                                       AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                                 AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                            -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                 ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                    ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)))
                          T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
                T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
      T_Tree_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.initLast
d_initLast_684 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_684 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T_Σ_14
d_initLast_684 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_166
v9
  = Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 Integer
v8 T_Tree_166
v9
du_initLast_684 ::
  Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_684 :: Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 Integer
v0 T_Tree_166
v1
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1 of
      C_node_194 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_166
v6 T_Tree_166
v7 T__'8764'_'8852'__30
v8
        -> let v9 :: b
v9
                 = let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   AgdaAny -> b
forall a b. a -> b
coe
                     (let v10 :: t
v10 = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v12 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                               (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v7 of
                C_leaf_178 T__'60''8314'__20
v10
                  -> let v11 :: b
v11
                           = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3 of
                               AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                   let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                   AgdaAny -> b
forall a b. a -> b
coe
                                     (let v12 :: t
v12 = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7) in
                                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
                                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v14 of
                                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)
                                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                                                               (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)
                                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
                               AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v9 in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v8 of
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                            -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                 ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                    ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                       (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)))
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                            -> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
                                 AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                     (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                       ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                          AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                          ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                             (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)))
                                 AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                          T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
                T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
      T_Tree_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.join
d_join_740 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  T_Tree_166 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join_740 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join_740 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_166
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
  = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_740 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_166
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
du_join_740 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  T_Tree_166 ->
  T_Tree_166 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join_740 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_740 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 Integer
v4 Integer
v5 Integer
v6 T_Tree_166
v7 T_Tree_166
v8 T__'8764'_'8852'__30
v9
  = let v10 :: b
v10
          = let v10 :: Integer
v10 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
            AgdaAny -> b
forall a b. a -> b
coe
              (let v11 :: t
v11 = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v8) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v11 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v12 AgdaAny
v13
                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v13 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
                             -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12)
                                  ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
                                     ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                        ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                           ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))))
                                     (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))
                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v9)
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      (case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v8 of
         C_leaf_178 T__'60''8314'__20
v11
           -> let v12 :: b
v12
                    = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5 of
                        AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                            let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                            AgdaAny -> b
forall a b. a -> b
coe
                              (let v13 :: t
v13 = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v12) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v8) in
                               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v13 of
                                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
                                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v15 of
                                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v16 AgdaAny
v17
                                             -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
                                                  ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                     T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
                                                     ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                        AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                        ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                           AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                           ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                              T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
                                                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))))
                                                     (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16))
                                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v9)
                                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
                        AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v10 in
              AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v9 of
                   T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                     -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                          (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                          ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                             T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)
                             (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v11))
                   T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                     -> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6 of
                          AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                              (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                   T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)
                                   (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v11))
                          AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12
                   T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12)
         T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10)
-- Data.Tree.AVL.Indexed._.empty
d_empty_776 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_166
d_empty_776 :: T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
d_empty_776 ~T_Value_38
v0 ~Maybe (Maybe AgdaAny)
v1 ~Maybe (Maybe AgdaAny)
v2 = T__'60''8314'__20 -> T_Tree_166
du_empty_776
du_empty_776 ::
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_166
du_empty_776 :: T__'60''8314'__20 -> T_Tree_166
du_empty_776 = (T__'60''8314'__20 -> T_Tree_166)
-> T__'60''8314'__20 -> T_Tree_166
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_166
C_leaf_178
-- Data.Tree.AVL.Indexed._.singleton
d_singleton_784 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_166
d_singleton_784 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Tree_166
d_singleton_784 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
  = AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
du_singleton_784 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
du_singleton_784 ::
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_166
du_singleton_784 :: AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
du_singleton_784 AgdaAny
v0 AgdaAny
v1 T_Σ_14
v2
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
        -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_166
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (Integer
0 :: Integer) (Integer
0 :: Integer)
             ((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
             ((T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_166
C_leaf_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)) ((T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_166
C_leaf_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
             (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38)
      T_Σ_14
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.insertWith
d_insertWith_804 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  (Maybe AgdaAny -> AgdaAny) ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insertWith_804 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
d_insertWith_804 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_166
v11 T_Σ_14
v12
  = T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_166
v11 T_Σ_14
v12
du_insertWith_804 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny ->
  (Maybe AgdaAny -> AgdaAny) ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insertWith_804 :: T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_166
v4 T_Σ_14
v5
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v4 of
      C_leaf_178 T__'60''8314'__20
v6
        -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
             ((T_Fin_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
                (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
             ((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
du_singleton_784 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                ((Maybe AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v5))
      C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v9 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v13 AgdaAny
v14
               -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v5 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                      -> let v17 :: t
v17
                               = (T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                   T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516
                                   (T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
                                      (T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
                                   AgdaAny
v2 AgdaAny
v13 in
                         AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v18
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9)
                                     ((T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3)
                                        (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v10)
                                        ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)
                                           ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                              ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                 AgdaAny
v18))))
                                     (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v12)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v19
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6 Integer
v7
                                        ((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                           ((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                              T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 T_Value_38
v1 AgdaAny
v2
                                              AgdaAny
v13 AgdaAny
v19
                                              ((Maybe AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 Maybe AgdaAny -> AgdaAny
v3
                                                 ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                    ((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                       T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48
                                                       T_Value_38
v1 AgdaAny
v13 AgdaAny
v2
                                                       (let v21 :: t
v21
                                                              = (T_StrictTotalOrder_864 -> T_StrictPartialOrder_472)
-> AgdaAny -> t
forall a b. a -> b
coe
                                                                  T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.du_strictPartialOrder_916
                                                                  (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) in
                                                        AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                          ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                             T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                                                             (T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
                                                                ((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
                                                                   T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
                                                                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v21)))
                                                             AgdaAny
v2 AgdaAny
v13 AgdaAny
v19))
                                                       AgdaAny
v14)))))
                                        T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v20
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v10)
                                     ((T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3)
                                        (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11)
                                        ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                           ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                              ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                 AgdaAny
v20))
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)))
                                     (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v12)
                              T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                    T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_K'38'__56
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.insert
d_insert_906 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  AgdaAny ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insert_906 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
d_insert_906 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 AgdaAny
v10
  = T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insert_906 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v9 AgdaAny
v10
du_insert_906 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny ->
  AgdaAny ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insert_906 :: T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insert_906 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3
  = (T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL.Indexed._.delete
d_delete_922 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_delete_922 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
d_delete_922 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
  = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
du_delete_922 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_delete_922 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Integer
v3 AgdaAny
v4 T_Tree_166
v5 T_Σ_14
v6
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v5 of
      C_leaf_178 T__'60''8314'__20
v7
        -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
             (T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v5)
      C_node_194 Integer
v7 Integer
v8 T_K'38'__56
v10 T_Tree_166
v11 T_Tree_166
v12 T__'8764'_'8852'__30
v13
        -> let v14 :: Integer
v14 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v10 of
                MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v15 AgdaAny
v16
                  -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v6 of
                       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v17 AgdaAny
v18
                         -> let v19 :: t
v19
                                  = (T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                      T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516
                                      (T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
                                         (T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
                                      AgdaAny
v15 AgdaAny
v4 in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v20
                                   -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11)
                                        ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                           T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
                                           ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                              ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
                                           (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v12)
                                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                              ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                                 ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                    AgdaAny
v20))
                                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v18)))
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v21
                                   -> (T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> Integer
 -> Integer
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_740 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
                                        ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                           ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
                                        (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v14) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v12)
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v22
                                   -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v10)
                                        ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                           T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
                                           ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                              ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
                                           (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11)
                                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17)
                                              ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                                 ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                    AgdaAny
v22))))
                                        (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v12) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Tree_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.lookup
d_lookup_1020 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
d_lookup_1020 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> Maybe AgdaAny
d_lookup_1020 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
  = T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
du_lookup_1020 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny ->
  T_Tree_166 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 T_Tree_166
v3 T_Σ_14
v4
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
      C_leaf_178 T__'60''8314'__20
v5 -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      C_node_194 Integer
v5 Integer
v6 T_K'38'__56
v8 T_Tree_166
v9 T_Tree_166
v10 T__'8764'_'8852'__30
v11
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v8 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v12 AgdaAny
v13
               -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
                      -> let v16 :: t
v16
                               = (T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                   T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516
                                   (T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
                                      (T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
                                   AgdaAny
v12 AgdaAny
v2 in
                         AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
                           (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v17
                                -> (T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v10)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                        ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                           ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                              AgdaAny
v17))
                                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15))
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v18
                                -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                     ((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 T_Value_38
v1 AgdaAny
v12 AgdaAny
v2 AgdaAny
v18
                                        AgdaAny
v13)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v19
                                -> (T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v9)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
                                        ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                           ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                              AgdaAny
v19)))
                              T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                    T_Σ_14
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_K'38'__56
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_166
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.foldr
d_foldr_1100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_166 -> AgdaAny
d_foldr_1100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> T_Level_18
-> T_Level_18
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_166
-> AgdaAny
d_foldr_1100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~Maybe (Maybe AgdaAny)
v8 ~Maybe (Maybe AgdaAny)
v9 ~Integer
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12
             T_Tree_166
v13
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 T_Tree_166
v13
du_foldr_1100 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_166
v2
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v2 of
      C_leaf_178 T__'60''8314'__20
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      C_node_194 Integer
v3 Integer
v4 T_K'38'__56
v6 T_Tree_166
v7 T_Tree_166
v8 T__'8764'_'8852'__30
v9
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v6 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v10 AgdaAny
v11
               -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_166 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0)
                    ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v11 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_166 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v8)))
                    (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)
             T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.toDiffList
d_toDiffList_1126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_166 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toDiffList_1126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> [T_K'38'__56]
-> [T_K'38'__56]
d_toDiffList_1126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_166
v9
  = T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 T_Tree_166
v9
du_toDiffList_1126 ::
  T_Tree_166 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toDiffList_1126 :: T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 T_Tree_166
v0
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v0 of
      C_leaf_178 T__'60''8314'__20
v1 -> (AgdaAny -> AgdaAny) -> [T_K'38'__56] -> [T_K'38'__56]
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)
      C_node_194 Integer
v1 Integer
v2 T_K'38'__56
v4 T_Tree_166
v5 T_Tree_166
v6 T__'8764'_'8852'__30
v7
        -> (([AgdaAny] -> [AgdaAny])
 -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_K'38'__56] -> [T_K'38'__56]
forall a b. a -> b
coe
             ([AgdaAny] -> [AgdaAny])
-> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'43''43'__38
             ((T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v5))
             ((AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> T_K'38'__56 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'8759'__28 T_K'38'__56
v4
                ((T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)))
      T_Tree_166
_ -> [T_K'38'__56] -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.toList
d_toList_1140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_166 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_1140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> [T_K'38'__56]
d_toList_1140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_166
v9
  = T_Tree_166 -> [T_K'38'__56]
du_toList_1140 T_Tree_166
v9
du_toList_1140 ::
  T_Tree_166 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_1140 :: T_Tree_166 -> [T_K'38'__56]
du_toList_1140 T_Tree_166
v0
  = (T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> T_Tree_166 -> AgdaAny -> [T_K'38'__56]
forall a b. a -> b
coe
      T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 T_Tree_166
v0
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
-- Data.Tree.AVL.Indexed._.size
d_size_1150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) -> Integer -> T_Tree_166 -> Integer
d_size_1150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> Integer
d_size_1150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 = T_Tree_166 -> Integer
du_size_1150
du_size_1150 :: T_Tree_166 -> Integer
du_size_1150 :: T_Tree_166 -> Integer
du_size_1150
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_166 -> Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
      (([AgdaAny] -> Integer) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> Integer
MAlonzo.Code.Data.List.Base.du_length_296)
      ((T_Tree_166 -> [T_K'38'__56]) -> AgdaAny
forall a b. a -> b
coe T_Tree_166 -> [T_K'38'__56]
du_toList_1140)
-- Data.Tree.AVL.Indexed._.Val
d_Val_1164 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_1164 :: T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Val_1164 = T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.Wal
d_Wal_1166 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_1166 :: T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Wal_1166 = T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.map
d_map_1174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) -> Integer -> T_Tree_166 -> T_Tree_166
d_map_1174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T_Tree_166
d_map_1174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Value_38
v6 ~T_Value_38
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 ~Maybe (Maybe AgdaAny)
v9 ~Maybe (Maybe AgdaAny)
v10 ~Integer
v11 T_Tree_166
v12
  = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_166
v12
du_map_1174 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_166
v1
  = case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1 of
      C_leaf_178 T__'60''8314'__20
v2 -> T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1
      C_node_194 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_166
v6 T_Tree_166
v7 T__'8764'_'8852'__30
v8
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v5 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v9 AgdaAny
v10
               -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_166
 -> T_Tree_166
 -> T__'8764'_'8852'__30
 -> T_Tree_166)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_166
forall a b. a -> b
coe
                    Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v2 Integer
v3
                    ((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)
                       ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v9 AgdaAny
v10))
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6))
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)) T__'8764'_'8852'__30
v8
             T_K'38'__56
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_166
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError