{-# 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.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
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'__110 ::
  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_1280 ->
  Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__110 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._._<⁺_
d__'60''8314'__112 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__112 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._._≈∙_
d__'8776''8729'__114 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__114 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._.Key⁺
d_Key'8314'_116 ::
  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_1280 -> ()
d_Key'8314'_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
d_Key'8314'_116 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.irrefl⁺
d_irrefl'8314'_118 ::
  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_1280 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl'8314'_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
d_irrefl'8314'_118 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
forall a. a
erased
-- Data.Tree.AVL.Indexed._.refl⁺
d_refl'8314'_120 ::
  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_1280 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_120 T_StrictTotalOrder_1280
v3
du_refl'8314'_120 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_120 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_120 T_StrictTotalOrder_1280
v0
  = (T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> AgdaAny -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_refl'8314'_96 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
-- Data.Tree.AVL.Indexed._.strictPartialOrder
d_strictPartialOrder_122 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_strictPartialOrder_122 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_StrictPartialOrder_760
d_strictPartialOrder_122 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3
  = T_StrictTotalOrder_1280 -> T_StrictPartialOrder_760
du_strictPartialOrder_122 T_StrictTotalOrder_1280
v3
du_strictPartialOrder_122 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
du_strictPartialOrder_122 :: T_StrictTotalOrder_1280 -> T_StrictPartialOrder_760
du_strictPartialOrder_122 T_StrictTotalOrder_1280
v0
  = (T_StrictTotalOrder_1280 -> T_StrictPartialOrder_760)
-> AgdaAny -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_StrictTotalOrder_1280 -> T_StrictPartialOrder_760
MAlonzo.Code.Data.Tree.AVL.Key.du_strictPartialOrder_120 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
-- Data.Tree.AVL.Indexed._.strictTotalOrder
d_strictTotalOrder_124 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
d_strictTotalOrder_124 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_StrictTotalOrder_1280
d_strictTotalOrder_124 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 = T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_strictTotalOrder_124 T_StrictTotalOrder_1280
v3
du_strictTotalOrder_124 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
du_strictTotalOrder_124 :: T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_strictTotalOrder_124 T_StrictTotalOrder_1280
v0
  = (T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280)
-> AgdaAny -> T_StrictTotalOrder_1280
forall a b. a -> b
coe
      T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
MAlonzo.Code.Data.Tree.AVL.Key.du_strictTotalOrder_212 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
-- Data.Tree.AVL.Indexed._.sym⁺
d_sym'8314'_126 ::
  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_1280 ->
  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'_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_126 T_StrictTotalOrder_1280
v3
du_sym'8314'_126 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  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'_126 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_126 T_StrictTotalOrder_1280
v0
  = (T_StrictTotalOrder_1280
 -> 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_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_sym'8314'_102 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
-- Data.Tree.AVL.Indexed._.trans⁺
d_trans'8314'_128 ::
  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_1280 ->
  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'_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_128 T_StrictTotalOrder_1280
v3
du_trans'8314'_128 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  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'_128 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_128 T_StrictTotalOrder_1280
v0
  = (T_StrictTotalOrder_1280
 -> 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_1280
-> 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'_110 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
-- Data.Tree.AVL.Indexed._.⊥⁺<[_]<⊤⁺
d_'8869''8314''60''91'_'93''60''8868''8314'_130 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_130 :: T_StrictTotalOrder_1280 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_130 ~T_StrictTotalOrder_1280
v0 ~AgdaAny
v1
  = T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_130
du_'8869''8314''60''91'_'93''60''8868''8314'_130 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_130 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_130
  = (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_146 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  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_146 :: T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'91'_'93''45'injective_146 = T_StrictTotalOrder_1280
-> 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'__152 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_K'38'__152 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._.Value
d_Value_158 :: p -> p -> p -> p -> p -> T_Level_18
d_Value_158 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Data.Tree.AVL.Indexed._.const
d_const_162 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40
d_const_162 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> T_Value_40
d_const_162 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 = T_Level_18 -> T_Level_18 -> T_Value_40
du_const_162
du_const_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40
du_const_162 :: T_Level_18 -> T_Level_18 -> T_Value_40
du_const_162 T_Level_18
v0 T_Level_18
v1
  = T_Value_40 -> T_Value_40
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96
-- Data.Tree.AVL.Indexed._.fromPair
d_fromPair_164 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58
d_fromPair_164 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> T_Σ_14
-> T_K'38'__58
d_fromPair_164 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 = T_Level_18 -> T_Value_40 -> T_Σ_14 -> T_K'38'__58
du_fromPair_164
du_fromPair_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58
du_fromPair_164 :: T_Level_18 -> T_Value_40 -> T_Σ_14 -> T_K'38'__58
du_fromPair_164 T_Level_18
v0 T_Value_40
v1 T_Σ_14
v2
  = (T_Σ_14 -> T_K'38'__58) -> T_Σ_14 -> T_K'38'__58
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__58
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_88 T_Σ_14
v2
-- Data.Tree.AVL.Indexed._.key
d_key_166 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 -> AgdaAny
d_key_166 :: T_K'38'__58 -> AgdaAny
d_key_166 T_K'38'__58
v0
  = (T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v0)
-- Data.Tree.AVL.Indexed._.toPair
d_toPair_168 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_168 :: T_K'38'__58 -> T_Σ_14
d_toPair_168 = (T_K'38'__58 -> T_Σ_14) -> T_K'38'__58 -> T_Σ_14
forall a b. a -> b
coe T_K'38'__58 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_82
-- Data.Tree.AVL.Indexed._.value
d_value_170 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 -> AgdaAny
d_value_170 :: T_K'38'__58 -> AgdaAny
d_value_170 T_K'38'__58
v0
  = (T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_70 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v0)
-- Data.Tree.AVL.Indexed._.K&_.key
d_key_174 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 -> AgdaAny
d_key_174 :: T_K'38'__58 -> AgdaAny
d_key_174 T_K'38'__58
v0
  = (T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v0)
-- Data.Tree.AVL.Indexed._.K&_.value
d_value_176 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 -> AgdaAny
d_value_176 :: T_K'38'__58 -> AgdaAny
d_value_176 T_K'38'__58
v0
  = (T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_70 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v0)
-- Data.Tree.AVL.Indexed._.Value.family
d_family_180 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_family_180 :: T_Value_40 -> AgdaAny -> T_Level_18
d_family_180 = T_Value_40 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.Value.respects
d_respects_182 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_182 :: T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_182 T_Value_40
v0
  = (T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_50 (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v0)
-- Data.Tree.AVL.Indexed.Tree
d_Tree_192 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Tree_192 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_Tree_192
  = C_leaf_204 MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 |
    C_node_220 Integer Integer
               MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 T_Tree_192 T_Tree_192
               MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30
-- Data.Tree.AVL.Indexed._.ordered
d_ordered_236 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_192 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_ordered_236 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> T__'60''8314'__20
d_ordered_236 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_192
v9
  = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
du_ordered_236 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 T_Tree_192
v9
du_ordered_236 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  T_Tree_192 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_ordered_236 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
du_ordered_236 T_StrictTotalOrder_1280
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 T_Tree_192
v3
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v3 of
      C_leaf_204 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_220 Integer
v4 Integer
v5 T_K'38'__58
v7 T_Tree_192
v8 T_Tree_192
v9 T__'8764'_'8852'__30
v10
        -> (T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'60''8314'__20
forall a b. a -> b
coe
             T_StrictTotalOrder_1280
-> 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'_110 T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v7))))
             Maybe (Maybe AgdaAny)
v2
             ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
du_ordered_236 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v7))))
                (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v8))
             ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
du_ordered_236 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v7))))
                (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v9))
      T_Tree_192
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.Val
d_Val_248 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_248 :: T_Value_40 -> AgdaAny -> T_Level_18
d_Val_248 = T_Value_40 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.V≈
d_V'8776'_250 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_250 :: T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_250 T_Value_40
v0
  = (T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_50 (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v0)
-- Data.Tree.AVL.Indexed._.leaf-injective
d_leaf'45'injective_260 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  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_260 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
d_leaf'45'injective_260 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> 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_292 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  T_Tree_192 ->
  T_Tree_192 ->
  T_Tree_192 ->
  T_Tree_192 ->
  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_292 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__58
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
d_node'45'injective'45'key_292 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__58
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T_Tree_192
-> T_Tree_192
-> 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'_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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_192 -> T_Tree_192
d_cast'737'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T__'60''8314'__20
-> T_Tree_192
-> T_Tree_192
d_cast'737'_302 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T__'60''8314'__20
v10 T_Tree_192
v11
  = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_192
-> T_Tree_192
du_cast'737'_302 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T__'60''8314'__20
v10 T_Tree_192
v11
du_cast'737'_302 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_192 -> T_Tree_192
du_cast'737'_302 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_192
-> T_Tree_192
du_cast'737'_302 T_StrictTotalOrder_1280
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4 T_Tree_192
v5
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v5 of
      C_leaf_204 T__'60''8314'__20
v6
        -> (T__'60''8314'__20 -> T_Tree_192) -> AgdaAny -> T_Tree_192
forall a b. a -> b
coe
             T__'60''8314'__20 -> T_Tree_192
C_leaf_204
             ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_1280
-> 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_1280
-> 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'_110 T_StrictTotalOrder_1280
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_220 Integer
v6 Integer
v7 T_K'38'__58
v9 T_Tree_192
v10 T_Tree_192
v11 T__'8764'_'8852'__30
v12
        -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v6 Integer
v7 T_K'38'__58
v9
             ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T_Tree_192
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_192
-> T_Tree_192
du_cast'737'_302 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v9))))
                (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v4) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v10))
             T_Tree_192
v11 T__'8764'_'8852'__30
v12
      T_Tree_192
_ -> T_Tree_192
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.castʳ
d_cast'691'_328 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_192 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_192
d_cast'691'_328 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
d_cast'691'_328 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T_Tree_192
v10 T__'60''8314'__20
v11
  = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T_Tree_192
v10 T__'60''8314'__20
v11
du_cast'691'_328 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  T_Tree_192 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_192
du_cast'691'_328 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 T_StrictTotalOrder_1280
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T_Tree_192
v4 T__'60''8314'__20
v5
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v4 of
      C_leaf_204 T__'60''8314'__20
v6
        -> (T__'60''8314'__20 -> T_Tree_192) -> AgdaAny -> T_Tree_192
forall a b. a -> b
coe
             T__'60''8314'__20 -> T_Tree_192
C_leaf_204
             ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_1280
-> 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_1280
-> 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'_110 T_StrictTotalOrder_1280
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_220 Integer
v6 Integer
v7 T_K'38'__58
v9 T_Tree_192
v10 T_Tree_192
v11 T__'8764'_'8852'__30
v12
        -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_192
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v6 Integer
v7 T_K'38'__58
v9 T_Tree_192
v10
             ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v11) (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v5))
             T__'8764'_'8852'__30
v12
      T_Tree_192
_ -> T_Tree_192
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinˡ⁺
d_join'737''8314'_378 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_192 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8314'_378 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8314'_378 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__58
v11 T_Σ_14
v12 T_Tree_192
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_378 Integer
v8 Integer
v9 T_K'38'__58
v11 T_Σ_14
v12 T_Tree_192
v13 T__'8764'_'8852'__30
v14
du_join'737''8314'_378 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_192 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8314'_378 :: Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_378 Integer
v0 Integer
v1 T_K'38'__58
v2 T_Σ_14
v3 T_Tree_192
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_10
forall a b. a -> b
coe AgdaAny
v6 of
             T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
               -> (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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                    ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                       Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                       (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                          (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                       Integer
v1 T_K'38'__58
v2 AgdaAny
v7 T_Tree_192
v4 T__'8764'_'8852'__30
v5)
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                              ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (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'__58
v2 AgdaAny
v7 T_Tree_192
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 Integer
v0 T_K'38'__58
v2 AgdaAny
v7 T_Tree_192
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_192
forall a b. a -> b
coe AgdaAny
v7 of
                              C_node_220 Integer
v11 Integer
v12 T_K'38'__58
v14 T_Tree_192
v15 T_Tree_192
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_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v16 of
                                            C_node_220 Integer
v19 Integer
v20 T_K'38'__58
v22 T_Tree_192
v23 T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                                   ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                      Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                                      (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'__58
v22
                                                      ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v1 Integer
v19 T_K'38'__58
v14 T_Tree_192
v15 T_Tree_192
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'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v20 Integer
v1 T_K'38'__58
v2 T_Tree_192
v24 T_Tree_192
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_192
_ -> 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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                               (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                            ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (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'__58
v14 T_Tree_192
v15
                                               ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (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'__58
v2 T_Tree_192
v16 T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                            ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (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'__58
v14 T_Tree_192
v15
                                               ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v1 Integer
v1 T_K'38'__58
v2 T_Tree_192
v16 T_Tree_192
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_192
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_10
_ -> 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'_468 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  T_Tree_192 ->
  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'_468 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8314'_468 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__58
v11 T_Tree_192
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_468 Integer
v8 Integer
v9 T_K'38'__58
v11 T_Tree_192
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8314'_468 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  T_Tree_192 ->
  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'_468 :: Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_468 Integer
v0 Integer
v1 T_K'38'__58
v2 T_Tree_192
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_10
forall a b. a -> b
coe AgdaAny
v6 of
             T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
               -> (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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                    ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                       Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0
                       (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                          (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                       T_K'38'__58
v2 T_Tree_192
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
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_192
forall a b. a -> b
coe AgdaAny
v7 of
                              C_node_220 Integer
v11 Integer
v12 T_K'38'__58
v14 T_Tree_192
v15 T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                            ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (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'__58
v14
                                               ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0 Integer
v0 T_K'38'__58
v2 T_Tree_192
v3 T_Tree_192
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_192
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                               (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                            ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (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'__58
v14
                                               ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 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'__58
v2 T_Tree_192
v3 T_Tree_192
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_192
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_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v15 of
                                            C_node_220 Integer
v19 Integer
v20 T_K'38'__58
v22 T_Tree_192
v23 T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                                   ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                      Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                                      (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'__58
v22
                                                      ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0 Integer
v19 T_K'38'__58
v2 T_Tree_192
v3 T_Tree_192
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'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v20 Integer
v0 T_K'38'__58
v14 T_Tree_192
v24 T_Tree_192
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_192
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_Tree_192
_ -> 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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 T_K'38'__58
v2 T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                              ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (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_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                 T_K'38'__58
v2 T_Tree_192
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_10
_ -> 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'_544 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_192 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8315'_544 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8315'_544 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__58
v11 T_Σ_14
v12 T_Tree_192
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_544 Integer
v8 Integer
v9 T_K'38'__58
v11 T_Σ_14
v12 T_Tree_192
v13 T__'8764'_'8852'__30
v14
du_join'737''8315'_544 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_192 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8315'_544 :: Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_544 Integer
v0 Integer
v1 T_K'38'__58
v2 T_Σ_14
v3 T_Tree_192
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_10
forall a b. a -> b
coe AgdaAny
v6 of
                    T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                      -> (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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                              (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                           ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                              Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                              (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                 (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                              Integer
v1 T_K'38'__58
v2 AgdaAny
v7 T_Tree_192
v4 T__'8764'_'8852'__30
v5)
                    MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                                 Integer
v1 T_K'38'__58
v2 AgdaAny
v7 T_Tree_192
v4 T__'8764'_'8852'__30
v5))
                    T_Fin_10
_ -> 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_10
forall a b. a -> b
coe AgdaAny
v7 of
                       T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                         -> 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'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_468
                                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))
                                     (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                           (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                        (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                     ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                        Integer
v0 T_K'38'__58
v2 AgdaAny
v8 T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                     ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                        Integer
v6 T_K'38'__58
v2 AgdaAny
v8 T_Tree_192
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_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                    (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                 ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> AgdaAny
-> T_Tree_192
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                    Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220
                                    (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                       ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                          T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                          (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                    Integer
v1 T_K'38'__58
v2 AgdaAny
v8 T_Tree_192
v4 T__'8764'_'8852'__30
v5))
                       T_Fin_10
_ -> 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'_606 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  T_Tree_192 ->
  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'_606 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8315'_606 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__58
v11 T_Tree_192
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 Integer
v8 Integer
v9 T_K'38'__58
v11 T_Tree_192
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8315'_606 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  T_Tree_192 ->
  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'_606 :: Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 Integer
v0 Integer
v1 T_K'38'__58
v2 T_Tree_192
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_10
forall a b. a -> b
coe AgdaAny
v6 of
                    T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                      -> (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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                              (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                           ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                              Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0
                              (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                 (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                              T_K'38'__58
v2 T_Tree_192
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
                    MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                                 T_K'38'__58
v2 T_Tree_192
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5))
                    T_Fin_10
_ -> 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_10
forall a b. a -> b
coe AgdaAny
v7 of
                       T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                         -> 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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                     ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v6
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                        T_K'38'__58
v2 T_Tree_192
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                     ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v1
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                        T_K'38'__58
v2 T_Tree_192
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'__58
 -> T_Σ_14
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_378 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
                                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1))
                                     (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                           (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                        (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_10
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                    (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                 ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                    Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v0
                                    (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                       ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                          T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                          (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                    T_K'38'__58
v2 T_Tree_192
v3 AgdaAny
v8 T__'8764'_'8852'__30
v5))
                       T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL.Indexed._.headTail
d_headTail_660 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer -> T_Tree_192 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_660 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> T_Σ_14
d_headTail_660 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_192
v9
  = Integer -> T_Tree_192 -> T_Σ_14
du_headTail_660 Integer
v8 T_Tree_192
v9
du_headTail_660 ::
  Integer -> T_Tree_192 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_660 :: Integer -> T_Tree_192 -> T_Σ_14
du_headTail_660 Integer
v0 T_Tree_192
v1
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v1 of
      C_node_220 Integer
v2 Integer
v3 T_K'38'__58
v5 T_Tree_192
v6 T_Tree_192
v7 T__'8764'_'8852'__30
v8
        -> let v9 :: AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                     (let v10 :: AgdaAny
v10 = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Σ_14
du_headTail_660 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
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'__58
 -> T_Σ_14
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_544 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v5)
                                               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v6 of
                C_leaf_204 T__'60''8314'__20
v10
                  -> let v11 :: AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                                     (let v12 :: AgdaAny
v12 = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Σ_14
du_headTail_660 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6) in
                                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (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
                                             -> 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'__58
 -> T_Σ_14
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                               Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_544 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                                                               (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
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'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                                   (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v7)))
                                       AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11
                                 AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
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'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v7)))
                          T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                T_Tree_192
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)
      T_Tree_192
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.initLast
d_initLast_710 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer -> T_Tree_192 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_710 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> T_Σ_14
d_initLast_710 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_192
v9
  = Integer -> T_Tree_192 -> T_Σ_14
du_initLast_710 Integer
v8 T_Tree_192
v9
du_initLast_710 ::
  Integer -> T_Tree_192 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_710 :: Integer -> T_Tree_192 -> T_Σ_14
du_initLast_710 Integer
v0 T_Tree_192
v1
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v1 of
      C_node_220 Integer
v2 Integer
v3 T_K'38'__58
v5 T_Tree_192
v6 T_Tree_192
v7 T__'8764'_'8852'__30
v8
        -> let v9 :: AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                     (let v10 :: AgdaAny
v10 = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Σ_14
du_initLast_710 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v7) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
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'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v5)
                                               (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v7 of
                C_leaf_204 T__'60''8314'__20
v10
                  -> let v11 :: AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                                     (let v12 :: AgdaAny
v12 = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Σ_14
du_initLast_710 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v7) in
                                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (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
                                             -> 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'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                                                               (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v5) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
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'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6)))
                                 AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11
                          T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                T_Tree_192
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)
      T_Tree_192
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.join
d_join_766 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  T_Tree_192 ->
  T_Tree_192 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join_766 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join_766 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_192
v12 T_Tree_192
v13 T__'8764'_'8852'__30
v14
  = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_766 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_192
v12 T_Tree_192
v13 T__'8764'_'8852'__30
v14
du_join_766 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  T_Tree_192 ->
  T_Tree_192 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join_766 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_766 T_StrictTotalOrder_1280
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 Integer
v4 Integer
v5 Integer
v6 T_Tree_192
v7 T_Tree_192
v8 T__'8764'_'8852'__30
v9
  = let v10 :: AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
              (let v11 :: AgdaAny
v11 = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Σ_14
du_headTail_660 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v10) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v8) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
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'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 (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_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))))
                                     (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v8 of
         C_leaf_204 T__'60''8314'__20
v11
           -> let v12 :: AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe
                              (let v13 :: AgdaAny
v13 = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Σ_14
du_headTail_660 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v12) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v8) in
                               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 (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
                                      -> 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'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 (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_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                     T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                              T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68
                                                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))))
                                                     (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                          ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                             T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                   T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
du_cast'691'_328 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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
v12
                   T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12)
         T_Tree_192
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10)
-- Data.Tree.AVL.Indexed._.empty
d_empty_802 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_192
d_empty_802 :: T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_192
d_empty_802 ~T_Value_40
v0 ~Maybe (Maybe AgdaAny)
v1 ~Maybe (Maybe AgdaAny)
v2 = T__'60''8314'__20 -> T_Tree_192
du_empty_802
du_empty_802 ::
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_192
du_empty_802 :: T__'60''8314'__20 -> T_Tree_192
du_empty_802 = (T__'60''8314'__20 -> T_Tree_192)
-> T__'60''8314'__20 -> T_Tree_192
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_192
C_leaf_204
-- Data.Tree.AVL.Indexed._.singleton
d_singleton_810 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_192
d_singleton_810 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Tree_192
d_singleton_810 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
  = AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_192
du_singleton_810 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
du_singleton_810 ::
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_192
du_singleton_810 :: AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_192
du_singleton_810 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'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_192
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 (Integer
0 :: Integer) (Integer
0 :: Integer)
             ((AgdaAny -> AgdaAny -> T_K'38'__58)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_K'38'__58
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 (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_192) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_192
C_leaf_204 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)) ((T__'60''8314'__20 -> T_Tree_192) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_192
C_leaf_204 (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_192
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.insertWith
d_insertWith_830 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  (Maybe AgdaAny -> AgdaAny) ->
  T_Tree_192 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insertWith_830 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
d_insertWith_830 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_192
v11 T_Σ_14
v12
  = T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insertWith_830 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_192
v11 T_Σ_14
v12
du_insertWith_830 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny ->
  (Maybe AgdaAny -> AgdaAny) ->
  T_Tree_192 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insertWith_830 :: T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insertWith_830 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_192
v4 T_Σ_14
v5
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v4 of
      C_leaf_204 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_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
             ((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_192)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_192
du_singleton_810 (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_220 Integer
v6 Integer
v7 T_K'38'__58
v9 T_Tree_192
v10 T_Tree_192
v11 T__'8764'_'8852'__30
v12
        -> case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v9 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 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 :: AgdaAny
v17
                               = (T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634
                                   (T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
                                      (T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))
                                   AgdaAny
v2 AgdaAny
v13 in
                         AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
v17 of
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v18
                                -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Σ_14
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_378 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v9)
                                     ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insertWith_830 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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'_180 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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                     ((Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v6 Integer
v7
                                        ((AgdaAny -> AgdaAny -> T_K'38'__58)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> AgdaAny -> T_K'38'__58
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                           ((T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                              T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_50 T_Value_40
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_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                       T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_50
                                                       T_Value_40
v1 AgdaAny
v13 AgdaAny
v2
                                                       ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                          T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
                                                          (T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
                                                             ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
                                                                T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
                                                                ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                   T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
                                                                   (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))))
                                                          AgdaAny
v2 AgdaAny
v13 AgdaAny
v19)
                                                       AgdaAny
v14)))))
                                        T_Tree_192
v10 T_Tree_192
v11 T__'8764'_'8852'__30
v12)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v20
                                -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_468 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v9) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v10)
                                     ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insertWith_830 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                    T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_K'38'__58
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_192
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.insert
d_insert_932 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  AgdaAny ->
  T_Tree_192 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insert_932 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
d_insert_932 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 AgdaAny
v10
  = T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insert_932 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny
v9 AgdaAny
v10
du_insert_932 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny ->
  AgdaAny ->
  T_Tree_192 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insert_932 :: T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insert_932 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 AgdaAny
v3
  = (T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_insertWith_830 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
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_948 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_192 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_delete_948 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
d_delete_948 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_192
v10 T_Σ_14
v11
  = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_delete_948 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_192
v10 T_Σ_14
v11
du_delete_948 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_192 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_delete_948 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_delete_948 T_StrictTotalOrder_1280
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Integer
v3 AgdaAny
v4 T_Tree_192
v5 T_Σ_14
v6
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v5 of
      C_leaf_204 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_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v5)
      C_node_220 Integer
v7 Integer
v8 T_K'38'__58
v10 T_Tree_192
v11 T_Tree_192
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'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v10 of
                MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 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 :: AgdaAny
v19
                                  = (T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                      T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634
                                      (T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
                                         (T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))
                                      AgdaAny
v15 AgdaAny
v4 in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
v19 of
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v20
                                   -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> 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'__58
-> T_Tree_192
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_606 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v10) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v11)
                                        ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                           T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_delete_948 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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'_180 AgdaAny
v21
                                   -> (T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> Integer
 -> Integer
 -> T_Tree_192
 -> T_Tree_192
 -> 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_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_766 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v11) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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'_188 AgdaAny
v22
                                   -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Σ_14
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__58
-> T_Σ_14
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_544 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v10)
                                        ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                           T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
du_delete_948 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v12) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_K'38'__58
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Tree_192
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.lookup
d_lookup_1046 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_192 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
d_lookup_1046 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> AgdaAny
-> T_Σ_14
-> Maybe AgdaAny
d_lookup_1046 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_192
v9 AgdaAny
v10 T_Σ_14
v11
  = T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1046 T_StrictTotalOrder_1280
v3 T_Value_40
v5 T_Tree_192
v9 AgdaAny
v10 T_Σ_14
v11
du_lookup_1046 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_192 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
du_lookup_1046 :: T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1046 T_StrictTotalOrder_1280
v0 T_Value_40
v1 T_Tree_192
v2 AgdaAny
v3 T_Σ_14
v4
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v2 of
      C_leaf_204 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_220 Integer
v5 Integer
v6 T_K'38'__58
v8 T_Tree_192
v9 T_Tree_192
v10 T__'8764'_'8852'__30
v11
        -> case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v8 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 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 :: AgdaAny
v16
                               = (T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                   T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634
                                   (T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
                                      (T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))
                                   AgdaAny
v12 AgdaAny
v3 in
                         AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
                           (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
v16 of
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v17
                                -> (T_StrictTotalOrder_1280
 -> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1046 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v1) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v10) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                                     ((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'_180 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_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_50 T_Value_40
v1 AgdaAny
v12 AgdaAny
v3 AgdaAny
v18
                                        AgdaAny
v13)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v19
                                -> (T_StrictTotalOrder_1280
 -> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1046 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v1) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v9) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                                     ((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_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                    T_Σ_14
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_K'38'__58
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_192
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.foldr
d_foldr_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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_192 -> AgdaAny
d_foldr_1126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> T_Level_18
-> T_Level_18
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_192
-> AgdaAny
d_foldr_1126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
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_192
v13
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_192 -> AgdaAny
du_foldr_1126 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 T_Tree_192
v13
du_foldr_1126 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_192 -> AgdaAny
du_foldr_1126 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_192 -> AgdaAny
du_foldr_1126 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_192
v2
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v2 of
      C_leaf_204 T__'60''8314'__20
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      C_node_220 Integer
v3 Integer
v4 T_K'38'__58
v6 T_Tree_192
v7 T_Tree_192
v8 T__'8764'_'8852'__30
v9
        -> case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v6 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 AgdaAny
v10 AgdaAny
v11
               -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_192 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_192 -> AgdaAny
du_foldr_1126 ((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_192 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_192 -> AgdaAny
du_foldr_1126 ((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_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v8)))
                    (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v7)
             T_K'38'__58
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_192
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.toDiffList
d_toDiffList_1152 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_192 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58] ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58]
d_toDiffList_1152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> [T_K'38'__58]
-> [T_K'38'__58]
d_toDiffList_1152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_192
v9
  = T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58]
du_toDiffList_1152 T_Tree_192
v9
du_toDiffList_1152 ::
  T_Tree_192 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58] ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58]
du_toDiffList_1152 :: T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58]
du_toDiffList_1152 T_Tree_192
v0
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v0 of
      C_leaf_204 T__'60''8314'__20
v1 -> (AgdaAny -> AgdaAny) -> [T_K'38'__58] -> [T_K'38'__58]
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)
      C_node_220 Integer
v1 Integer
v2 T_K'38'__58
v4 T_Tree_192
v5 T_Tree_192
v6 T__'8764'_'8852'__30
v7
        -> (([AgdaAny] -> [AgdaAny])
 -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_K'38'__58] -> [T_K'38'__58]
forall a b. a -> b
coe
             ([AgdaAny] -> [AgdaAny])
-> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'43''43'__38
             ((T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58]
du_toDiffList_1152 (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v5))
             ((AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> T_K'38'__58 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'8759'__28 T_K'38'__58
v4
                ((T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58]
du_toDiffList_1152 (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6)))
      T_Tree_192
_ -> [T_K'38'__58] -> [T_K'38'__58]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.toList
d_toList_1166 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_192 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58]
d_toList_1166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> [T_K'38'__58]
d_toList_1166 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_192
v9
  = T_Tree_192 -> [T_K'38'__58]
du_toList_1166 T_Tree_192
v9
du_toList_1166 ::
  T_Tree_192 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58]
du_toList_1166 :: T_Tree_192 -> [T_K'38'__58]
du_toList_1166 T_Tree_192
v0
  = (T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58])
-> T_Tree_192 -> AgdaAny -> [T_K'38'__58]
forall a b. a -> b
coe
      T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58]
du_toDiffList_1152 T_Tree_192
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_1176 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) -> Integer -> T_Tree_192 -> Integer
d_size_1176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Value_40
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> Integer
d_size_1176 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Value_40
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 = T_Tree_192 -> Integer
du_size_1176
du_size_1176 :: T_Tree_192 -> Integer
du_size_1176 :: T_Tree_192 -> Integer
du_size_1176
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_192 -> Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (([AgdaAny] -> Integer) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> Integer
MAlonzo.Code.Data.List.Base.du_length_268)
      ((T_Tree_192 -> [T_K'38'__58]) -> AgdaAny
forall a b. a -> b
coe T_Tree_192 -> [T_K'38'__58]
du_toList_1166)
-- Data.Tree.AVL.Indexed._.Val
d_Val_1190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_1190 :: T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> T_Level_18
d_Val_1190 = T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.Wal
d_Wal_1192 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Wal_1192 :: T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> T_Level_18
d_Wal_1192 = T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.map
d_map_1200 ::
  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_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) -> Integer -> T_Tree_192 -> T_Tree_192
d_map_1200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
-> T_Level_18
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_192
-> T_Tree_192
d_map_1200 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1280
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Value_40
v6 ~T_Value_40
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 ~Maybe (Maybe AgdaAny)
v9 ~Maybe (Maybe AgdaAny)
v10 ~Integer
v11 T_Tree_192
v12
  = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192
du_map_1200 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_192
v12
du_map_1200 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192
du_map_1200 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192
du_map_1200 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_192
v1
  = case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v1 of
      C_leaf_204 T__'60''8314'__20
v2 -> T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v1
      C_node_220 Integer
v2 Integer
v3 T_K'38'__58
v5 T_Tree_192
v6 T_Tree_192
v7 T__'8764'_'8852'__30
v8
        -> case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v5 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 AgdaAny
v9 AgdaAny
v10
               -> (Integer
 -> Integer
 -> T_K'38'__58
 -> T_Tree_192
 -> T_Tree_192
 -> T__'8764'_'8852'__30
 -> T_Tree_192)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_192
forall a b. a -> b
coe
                    Integer
-> Integer
-> T_K'38'__58
-> T_Tree_192
-> T_Tree_192
-> T__'8764'_'8852'__30
-> T_Tree_192
C_node_220 Integer
v2 Integer
v3
                    ((AgdaAny -> AgdaAny -> T_K'38'__58)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_K'38'__58
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__72 (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_192 -> T_Tree_192)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192
du_map_1200 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6))
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192
du_map_1200 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v7)) T__'8764'_'8852'__30
v8
             T_K'38'__58
_ -> T_Tree_192
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_192
_ -> T_Tree_192
forall a. a
MAlonzo.RTE.mazUnreachableError