{-# 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.List.Relation.Binary.Sublist.Heterogeneous.Properties 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
import qualified MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous
import qualified MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Data.Maybe.Relation.Unary.All
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d_'8759''45'injective'737'_46 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
[AgdaAny] ->
[AgdaAny] ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8759''45'injective'737'_46 = erased
d_'8759''45'injective'691'_64 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
[AgdaAny] ->
[AgdaAny] ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8759''45'injective'691'_64 = erased
d_'8759''691''45'injective_76 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8759''691''45'injective_76 = erased
d_length'45'mono'45''8804'_98 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_length'45'mono'45''8804'_98 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_length'45'mono'45''8804'_98 v6 v7 v8
du_length'45'mono'45''8804'_98 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_length'45'mono'45''8804'_98 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v6
-> case coe v1 of
(:) v7 v8
-> coe du_length'45'mono'45''8804'_98 (coe v0) (coe v8) (coe v6)
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v7 v8
-> case coe v0 of
(:) v9 v10
-> case coe v1 of
(:) v11 v12
-> coe
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30
(coe du_length'45'mono'45''8804'_98 (coe v10) (coe v12) (coe v8))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_fromPointwise_108 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_fromPointwise_108 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_fromPointwise_108 v6 v7 v8
du_fromPointwise_108 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_fromPointwise_108 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v7 v8
-> case coe v0 of
(:) v9 v10
-> case coe v1 of
(:) v11 v12
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v7 (coe du_fromPointwise_108 (coe v10) (coe v12) (coe v8))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_toPointwise_118 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_toPointwise_118 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 v9
= du_toPointwise_118 v6 v7 v9
du_toPointwise_118 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_toPointwise_118 v0 v1 v2
= case coe v1 of
[]
-> coe
seq (coe v2)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
(:) v3 v4
-> case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v8
-> coe MAlonzo.Code.Data.Empty.du_'8869''45'elim_10
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v9 v10
-> case coe v0 of
(:) v11 v12
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
v9 (coe du_toPointwise_118 (coe v12) (coe v4) (coe v10))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_tail'45'Sublist_162 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18
d_tail'45'Sublist_162 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_tail'45'Sublist_162 v6 v7 v8
du_tail'45'Sublist_162 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18
du_tail'45'Sublist_162 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe MAlonzo.Code.Data.Maybe.Relation.Unary.All.C_nothing_32
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v6
-> case coe v1 of
(:) v7 v8
-> coe
MAlonzo.Code.Data.Maybe.Relation.Unary.All.du_map_60
(coe
(\ v9 ->
coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36))
(coe MAlonzo.Code.Data.List.Base.du_tail_490 (coe v0))
(coe du_tail'45'Sublist_162 (coe v0) (coe v8) (coe v6))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v7 v8
-> coe
MAlonzo.Code.Data.Maybe.Relation.Unary.All.C_just_30
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
v8)
_ -> MAlonzo.RTE.mazUnreachableError
d_take'45'Sublist_180 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
Integer ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_take'45'Sublist_180 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
= du_take'45'Sublist_180 v6 v7 v8 v9
du_take'45'Sublist_180 ::
[AgdaAny] ->
[AgdaAny] ->
Integer ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_take'45'Sublist_180 v0 v1 v2 v3
= let v4
= coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v1) in
case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> case coe v2 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v1)
_ -> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v8
-> case coe v1 of
(:) v9 v10
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_take'45'Sublist_180 (coe v0) (coe v10) (coe v2) (coe v8))
_ -> coe v4
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v9 v10
-> let v11
= case coe v2 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v1)
_ -> coe v4 in
case coe v0 of
(:) v12 v13
-> let v14
= case coe v2 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v1)
_ -> coe v4 in
case coe v1 of
(:) v15 v16
-> case coe v2 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v1)
_ -> let v17 = subInt (coe v2) (coe (1 :: Integer)) in
coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v9
(coe
du_take'45'Sublist_180 (coe v13) (coe v16) (coe v17) (coe v10))
_ -> coe v14
_ -> coe v11
_ -> MAlonzo.RTE.mazUnreachableError
d_drop'45'Sublist_200 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_drop'45'Sublist_200 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
= du_drop'45'Sublist_200 v6 v7 v8 v9
du_drop'45'Sublist_200 ::
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_drop'45'Sublist_200 v0 v1 v2 v3
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe seq (coe v0) (coe v3)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v2 of
(:) v8 v9
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_drop'45'Sublist_200 (coe v0) (coe v1) (coe v9) (coe v7))
_ -> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> let v10
= case coe v0 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8 v9
_ -> coe v3 in
case coe v1 of
(:) v11 v12
-> let v13
= case coe v0 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8 v9
_ -> coe v3 in
case coe v2 of
(:) v14 v15
-> case coe v0 of
0 -> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8 v9
_ -> let v16 = subInt (coe v0) (coe (1 :: Integer)) in
coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_drop'45'Sublist_200 (coe v16) (coe v12) (coe v15) (coe v9))
_ -> coe v13
_ -> coe v10
_ -> MAlonzo.RTE.mazUnreachableError
d_takeWhile'45'Sublist_244 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_takeWhile'45'Sublist_244 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
v10 v11
= du_takeWhile'45'Sublist_244 v8 v9 v10 v11
du_takeWhile'45'Sublist_244 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_takeWhile'45'Sublist_244 v0 v1 v2 v3
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v2 of
(:) v8 v9
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_takeWhile'45'Sublist_244 (coe v0) (coe v1) (coe v9) (coe v7))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> case coe v1 of
(:) v10 v11
-> case coe v2 of
(:) v12 v13
-> let v14
= MAlonzo.Code.Relation.Nullary.d_does_42 (coe v0 v10) in
if coe v14
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8
(coe
du_takeWhile'45'Sublist_244 (coe v0) (coe v11) (coe v13)
(coe v9))
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v2)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_dropWhile'45'Sublist_282 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_dropWhile'45'Sublist_282 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
v10 v11
= du_dropWhile'45'Sublist_282 v8 v9 v10 v11
du_dropWhile'45'Sublist_282 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_dropWhile'45'Sublist_282 v0 v1 v2 v3
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v2 of
(:) v8 v9
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_dropWhile'45'Sublist_282 (coe v0) (coe v1) (coe v9) (coe v7))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> case coe v1 of
(:) v10 v11
-> case coe v2 of
(:) v12 v13
-> let v14
= MAlonzo.Code.Relation.Nullary.d_does_42 (coe v0 v10) in
if coe v14
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_dropWhile'45'Sublist_282 (coe v0) (coe v11) (coe v13)
(coe v9))
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8 v9
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_filter'45'Sublist_320 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_filter'45'Sublist_320 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
v11
= du_filter'45'Sublist_320 v8 v9 v10 v11
du_filter'45'Sublist_320 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_filter'45'Sublist_320 v0 v1 v2 v3
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v2 of
(:) v8 v9
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_filter'45'Sublist_320 (coe v0) (coe v1) (coe v9) (coe v7))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> case coe v1 of
(:) v10 v11
-> case coe v2 of
(:) v12 v13
-> let v14
= MAlonzo.Code.Relation.Nullary.d_does_42 (coe v0 v10) in
if coe v14
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8
(coe
du_filter'45'Sublist_320 (coe v0) (coe v11) (coe v13) (coe v9))
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_filter'45'Sublist_320 (coe v0) (coe v11) (coe v13) (coe v9))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'8759''737''8315'_376 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'8759''737''8315'_376 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
= du_'8759''737''8315'_376 v8 v9
du_'8759''737''8315'_376 ::
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'8759''737''8315'_376 v0 v1
= case coe v1 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v5
-> case coe v0 of
(:) v6 v7
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_'8759''737''8315'_376 (coe v7) (coe v5))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v6 v7
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
v7
_ -> MAlonzo.RTE.mazUnreachableError
d_'8759''691''8315'_394 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
[AgdaAny] ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'8759''691''8315'_394 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
~v10 v11
= du_'8759''691''8315'_394 v11
du_'8759''691''8315'_394 ::
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'8759''691''8315'_394 v0
= case coe v0 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v4
-> coe v4
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v5 v6
-> coe MAlonzo.Code.Data.Empty.du_'8869''45'elim_10
_ -> MAlonzo.RTE.mazUnreachableError
d_'8759''8315'_416 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'8759''8315'_416 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9 v10
= du_'8759''8315'_416 v9 v10
du_'8759''8315'_416 ::
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'8759''8315'_416 v0 v1
= case coe v1 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v5
-> coe du_'8759''737''8315'_376 (coe v0) (coe v5)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v6 v7
-> coe v7
_ -> MAlonzo.RTE.mazUnreachableError
d_map'8314'_462 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_map'8314'_462 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11
~v12 ~v13 v14
= du_map'8314'_462 v10 v11 v14
du_map'8314'_462 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_map'8314'_462 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v2
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v6
-> case coe v1 of
(:) v7 v8
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_map'8314'_462 (coe v0) (coe v8) (coe v6))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v7 v8
-> case coe v0 of
(:) v9 v10
-> case coe v1 of
(:) v11 v12
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v7 (coe du_map'8314'_462 (coe v10) (coe v12) (coe v8))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_map'8315'_496 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_map'8315'_496 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11
~v12 ~v13 v14
= du_map'8315'_496 v10 v11 v14
du_map'8315'_496 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_map'8315'_496 v0 v1 v2
= case coe v0 of
[]
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v1)
(:) v3 v4
-> case coe v1 of
(:) v5 v6
-> case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v10
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_map'8315'_496 (coe v0) (coe v6) (coe v10))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v11 v12
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v11 (coe du_map'8315'_496 (coe v4) (coe v6) (coe v12))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'43''43''8314'_560 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'43''43''8314'_560 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 ~v9 v10 v11
= du_'43''43''8314'_560 v6 v7 v10 v11
du_'43''43''8314'_560 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'43''43''8314'_560 v0 v1 v2 v3
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v1 of
(:) v8 v9
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_'43''43''8314'_560 (coe v0) (coe v9) (coe v7) (coe v3))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> case coe v0 of
(:) v10 v11
-> case coe v1 of
(:) v12 v13
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8
(coe du_'43''43''8314'_560 (coe v11) (coe v13) (coe v9) (coe v3))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'43''43''8315'_584 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'43''43''8315'_584 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 v9 ~v10 v11
= du_'43''43''8315'_584 v6 v7 v9 v11
du_'43''43''8315'_584 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'43''43''8315'_584 v0 v1 v2 v3
= case coe v0 of
[] -> coe seq (coe v1) (coe v3)
(:) v4 v5
-> case coe v1 of
(:) v6 v7
-> coe
du_'43''43''8315'_584 (coe v5) (coe v7) (coe v2)
(coe
du_'8759''8315'_416
(coe
MAlonzo.Code.Data.List.Base.du__'43''43'__60 (coe v7) (coe v2))
(coe v3))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'43''43''737'_608 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'43''43''737'_608 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
= du_'43''43''737'_608 v8
du_'43''43''737'_608 ::
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'43''43''737'_608 v0
= coe
du_'43''43''8314'_560
(coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) (coe v0)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v0))
d_'43''43''691'_618 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'43''43''691'_618 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
= du_'43''43''691'_618 v6 v7 v8 v9
du_'43''43''691'_618 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'43''43''691'_618 v0 v1 v2 v3
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v2)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v1 of
(:) v8 v9
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe du_'43''43''691'_618 (coe v0) (coe v9) (coe v2) (coe v7))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> case coe v0 of
(:) v10 v11
-> case coe v1 of
(:) v12 v13
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8 (coe du_'43''43''691'_618 (coe v11) (coe v13) (coe v2) (coe v9))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_concat'8314'_638 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[[AgdaAny]] ->
[[AgdaAny]] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_concat'8314'_638 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_concat'8314'_638 v6 v7 v8
du_concat'8314'_638 ::
[[AgdaAny]] ->
[[AgdaAny]] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_concat'8314'_638 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v2
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v6
-> case coe v1 of
(:) v7 v8
-> coe
du_'43''43''737'_608 v7
(coe du_concat'8314'_638 (coe v0) (coe v8) (coe v6))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v7 v8
-> case coe v0 of
(:) v9 v10
-> case coe v1 of
(:) v11 v12
-> coe
du_'43''43''8314'_560 (coe v9) (coe v11) (coe v7)
(coe du_concat'8314'_638 (coe v10) (coe v12) (coe v8))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_take'8314'_656 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
Integer ->
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_take'8314'_656 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
= du_take'8314'_656 v7 v8 v9 v10 v11
du_take'8314'_656 ::
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_take'8314'_656 v0 v1 v2 v3 v4
= case coe v3 of
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe MAlonzo.Code.Data.List.Base.du_take_500 (coe v0) (coe v2))
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 v7
-> let v8 = subInt (coe v0) (coe (1 :: Integer)) in
case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v13 v14
-> case coe v1 of
(:) v15 v16
-> case coe v2 of
(:) v17 v18
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v13
(coe
du_take'8314'_656 (coe v8) (coe v16) (coe v18) (coe v7)
(coe v14))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_drop'8314'_676 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
Integer ->
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_drop'8314'_676 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 ~v7 v8 v9 v10 v11
= du_drop'8314'_676 v6 v8 v9 v10 v11
du_drop'8314'_676 ::
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_drop'8314'_676 v0 v1 v2 v3 v4
= case coe v3 of
MAlonzo.Code.Data.Nat.Base.C_z'8804'n_22
-> coe du_drop'45'Sublist_200 (coe v0) (coe v1) (coe v2) (coe v4)
MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 v7
-> let v8 = subInt (coe v0) (coe (1 :: Integer)) in
case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v4
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v12
-> case coe v2 of
(:) v13 v14
-> coe
du_drop'8314'_676 (coe v0) (coe v1) (coe v14) (coe v7) (coe v12)
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v13 v14
-> case coe v1 of
(:) v15 v16
-> case coe v2 of
(:) v17 v18
-> coe
du_drop'8314'_676 (coe v8) (coe v16) (coe v18) (coe v7) (coe v14)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_drop'8314''45''8805'_704 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
Integer ->
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_drop'8314''45''8805'_704 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 ~v7 v8 v9 v10
v11
= du_drop'8314''45''8805'_704 v6 v8 v9 v10 v11
du_drop'8314''45''8805'_704 ::
Integer ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_drop'8314''45''8805'_704 v0 v1 v2 v3 v4
= coe
du_drop'8314'_676 (coe v0) (coe v1) (coe v2) (coe v3)
(coe du_fromPointwise_108 (coe v1) (coe v2) (coe v4))
d_drop'8314''45''8838'_716 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
Integer ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_drop'8314''45''8838'_716 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_drop'8314''45''8838'_716 v6 v7 v8
du_drop'8314''45''8838'_716 ::
[AgdaAny] ->
[AgdaAny] ->
Integer ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_drop'8314''45''8838'_716 v0 v1 v2
= coe
du_drop'8314'_676 (coe v2) (coe v0) (coe v1)
(coe
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_1698 (coe v2))
d_'8838''45'takeWhile'45'Sublist_756 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'8838''45'takeWhile'45'Sublist_756 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
~v7 ~v8 ~v9 v10 v11 v12 v13 ~v14 v15
= du_'8838''45'takeWhile'45'Sublist_756 v10 v11 v12 v13 v15
du_'8838''45'takeWhile'45'Sublist_756 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'8838''45'takeWhile'45'Sublist_756 v0 v1 v2 v3 v4
= case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v9 v10
-> case coe v2 of
(:) v11 v12
-> case coe v3 of
(:) v13 v14
-> let v15 = coe v0 v11 in
let v16 = coe v1 v13 in
case coe v15 of
MAlonzo.Code.Relation.Nullary.C__because__46 v17 v18
-> if coe v17
then case coe v16 of
MAlonzo.Code.Relation.Nullary.C__because__46 v19 v20
-> if coe v19
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v9
(coe
du_'8838''45'takeWhile'45'Sublist_756
(coe v0) (coe v1) (coe v12) (coe v14)
(coe v10))
else coe
seq (coe v18)
(coe
seq (coe v20)
(coe
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10))
_ -> MAlonzo.RTE.mazUnreachableError
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(let v19
= MAlonzo.Code.Relation.Nullary.d_does_42
(coe v16) in
if coe v19
then coe
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
(coe v13)
(coe
MAlonzo.Code.Data.List.Base.du_takeWhile_552
(coe v1) (coe v14))
else coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'8839''45'dropWhile'45'Sublist_832 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'8839''45'dropWhile'45'Sublist_832 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
~v7 ~v8 ~v9 v10 v11 v12 v13 ~v14 v15
= du_'8839''45'dropWhile'45'Sublist_832 v10 v11 v12 v13 v15
du_'8839''45'dropWhile'45'Sublist_832 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'8839''45'dropWhile'45'Sublist_832 v0 v1 v2 v3 v4
= case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v9 v10
-> case coe v2 of
(:) v11 v12
-> case coe v3 of
(:) v13 v14
-> let v15 = coe v0 v11 in
let v16 = coe v1 v13 in
case coe v15 of
MAlonzo.Code.Relation.Nullary.C__because__46 v17 v18
-> if coe v17
then case coe v16 of
MAlonzo.Code.Relation.Nullary.C__because__46 v19 v20
-> if coe v19
then coe
du_'8839''45'dropWhile'45'Sublist_832
(coe v0) (coe v1) (coe v12) (coe v14)
(coe v10)
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_dropWhile'45'Sublist_282 (coe v0)
(coe v12) (coe v14)
(coe
du_fromPointwise_108 (coe v12)
(coe v14) (coe v10)))
_ -> MAlonzo.RTE.mazUnreachableError
else (case coe v16 of
MAlonzo.Code.Relation.Nullary.C__because__46 v19 v20
-> if coe v19
then coe
seq (coe v18)
(coe
seq (coe v20)
(coe
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10))
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v9
(coe
du_fromPointwise_108 (coe v12) (coe v14)
(coe v10))
_ -> MAlonzo.RTE.mazUnreachableError)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'8838''45'filter'45'Sublist_922 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'8838''45'filter'45'Sublist_922 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7
~v8 ~v9 v10 v11 v12 v13 ~v14 v15
= du_'8838''45'filter'45'Sublist_922 v10 v11 v12 v13 v15
du_'8838''45'filter'45'Sublist_922 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'8838''45'filter'45'Sublist_922 v0 v1 v2 v3 v4
= case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v4
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v8
-> case coe v3 of
(:) v9 v10
-> let v11 = MAlonzo.Code.Relation.Nullary.d_does_42 (coe v1 v9) in
if coe v11
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_'8838''45'filter'45'Sublist_922 (coe v0) (coe v1) (coe v2)
(coe v10) (coe v8))
else coe
du_'8838''45'filter'45'Sublist_922 (coe v0) (coe v1) (coe v2)
(coe v10) (coe v8)
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v9 v10
-> case coe v2 of
(:) v11 v12
-> case coe v3 of
(:) v13 v14
-> let v15 = coe v0 v11 in
let v16 = coe v1 v13 in
case coe v15 of
MAlonzo.Code.Relation.Nullary.C__because__46 v17 v18
-> if coe v17
then case coe v16 of
MAlonzo.Code.Relation.Nullary.C__because__46 v19 v20
-> if coe v19
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v9
(coe
du_'8838''45'filter'45'Sublist_922
(coe v0) (coe v1) (coe v12) (coe v14)
(coe v10))
else coe
seq (coe v18)
(coe
seq (coe v20)
(coe
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10))
_ -> MAlonzo.RTE.mazUnreachableError
else (case coe v16 of
MAlonzo.Code.Relation.Nullary.C__because__46 v19 v20
-> if coe v19
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_'8838''45'filter'45'Sublist_922
(coe v0) (coe v1) (coe v12) (coe v14)
(coe v10))
else coe
du_'8838''45'filter'45'Sublist_922 (coe v0)
(coe v1) (coe v12) (coe v14) (coe v10)
_ -> MAlonzo.RTE.mazUnreachableError)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_takeWhile'45'filter_1046 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_takeWhile'45'filter_1046 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_takeWhile'45'filter_1046 v6 v7 v8
du_takeWhile'45'filter_1046 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_takeWhile'45'filter_1046 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v7 v8
-> case coe v1 of
(:) v9 v10
-> let v11 = MAlonzo.Code.Relation.Nullary.d_does_42 (coe v0 v9) in
if coe v11
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v7 (coe du_takeWhile'45'filter_1046 (coe v0) (coe v10) (coe v8))
else coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe MAlonzo.Code.Data.List.Base.du_filter_608 (coe v0) (coe v10))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_filter'45'dropWhile_1078 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_filter'45'dropWhile_1078 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_filter'45'dropWhile_1078 v6 v7 v8
du_filter'45'dropWhile_1078 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_filter'45'dropWhile_1078 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v7 v8
-> case coe v1 of
(:) v9 v10
-> let v11 = MAlonzo.Code.Relation.Nullary.d_does_42 (coe v0 v9) in
if coe v11
then coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v7
(coe
du_filter'45'Sublist_320 (coe v0) (coe v10) (coe v10)
(coe du_fromPointwise_108 (coe v10) (coe v10) (coe v8)))
else coe du_filter'45'dropWhile_1078 (coe v0) (coe v10) (coe v8)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_reverseAcc'8314'_1132 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_reverseAcc'8314'_1132 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 ~v9 v10
v11
= du_reverseAcc'8314'_1132 v6 v7 v10 v11
du_reverseAcc'8314'_1132 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_reverseAcc'8314'_1132 v0 v1 v2 v3
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe v3
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v1 of
(:) v8 v9
-> coe
du_reverseAcc'8314'_1132 (coe v0) (coe v9) (coe v7)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
v3)
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v8 v9
-> case coe v0 of
(:) v10 v11
-> case coe v1 of
(:) v12 v13
-> coe
du_reverseAcc'8314'_1132 (coe v11) (coe v13) (coe v9)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v8 v3)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'691''43''43''8314'_1156 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_'691''43''43''8314'_1156 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 ~v9
= du_'691''43''43''8314'_1156 v6 v7
du_'691''43''43''8314'_1156 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_'691''43''43''8314'_1156 v0 v1
= coe du_reverseAcc'8314'_1132 (coe v0) (coe v1)
d_reverse'8314'_1162 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_reverse'8314'_1162 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_reverse'8314'_1162 v6 v7 v8
du_reverse'8314'_1162 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_reverse'8314'_1162 v0 v1 v2
= coe
du_reverseAcc'8314'_1132 (coe v0) (coe v1) (coe v2)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28)
d_reverse'8315'_1170 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_reverse'8315'_1170 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_reverse'8315'_1170 v6 v7 v8
du_reverse'8315'_1170 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_reverse'8315'_1170 v0 v1 v2
= coe
du_reverse'8314'_1162
(coe MAlonzo.Code.Data.List.Base.du_reverse_804 v0)
(coe MAlonzo.Code.Data.List.Base.du_reverse_804 v1) (coe v2)
d_cast_1182 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_cast_1182 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9
= du_cast_1182 v9
du_cast_1182 ::
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_cast_1182 v0 = coe v0
d_'8759''8315''185'_1208 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
[AgdaAny] ->
AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_928
d_'8759''8315''185'_1208 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9 v10
= du_'8759''8315''185'_1208 v9 v10
du_'8759''8315''185'_1208 ::
[AgdaAny] ->
AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_928
du_'8759''8315''185'_1208 v0 v1
= coe
MAlonzo.Code.Function.Bundles.du_mk'8660'_1322
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v1)
(coe du_'8759''8315'_416 (coe v0))
d_'8759''691''8315''185'_1214 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
[AgdaAny] ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Function.Bundles.T_Equivalence_928
d_'8759''691''8315''185'_1214 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
~v9 ~v10
= du_'8759''691''8315''185'_1214
du_'8759''691''8315''185'_1214 ::
MAlonzo.Code.Function.Bundles.T_Equivalence_928
du_'8759''691''8315''185'_1214
= coe
MAlonzo.Code.Function.Bundles.du_mk'8660'_1322
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36)
(coe du_'8759''691''8315'_394)
d_Sublist'45''91''93''45'irrelevant_1236 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_Sublist'45''91''93''45'irrelevant_1236 = erased
d_toAny'45'injective_1254 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
AgdaAny ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_toAny'45'injective_1254 = erased
d_fromAny'45'injective_1276 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
AgdaAny ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_fromAny'45'injective_1276 = erased
d_toAny'8728'fromAny'8791'id_1292 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
AgdaAny ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_toAny'8728'fromAny'8791'id_1292 = erased
d_Sublist'45''91'x'93''45'bijection_1302 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] -> MAlonzo.Code.Function.Bundles.T_Bijection_844
d_Sublist'45''91'x'93''45'bijection_1302 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
~v6 v7
= du_Sublist'45''91'x'93''45'bijection_1302 v7
du_Sublist'45''91'x'93''45'bijection_1302 ::
[AgdaAny] -> MAlonzo.Code.Function.Bundles.T_Bijection_844
du_Sublist'45''91'x'93''45'bijection_1302 v0
= coe
MAlonzo.Code.Function.Bundles.du_mk'10518'_1312
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_toAny_60
(coe v0))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
(coe
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_fromAny_74
(coe v0))
erased))
d_reflexive_1316 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_reflexive_1316 ~v0 ~v1 ~v2 ~v3 v4 v5 ~v6 ~v7
= du_reflexive_1316 v4 v5
du_reflexive_1316 ::
(AgdaAny -> AgdaAny) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_reflexive_1316 v0 v1
= coe
du_fromPointwise_108 (coe v1) (coe v1)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_refl_30
(coe v0) (coe v1))
d_refl_1318 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_refl_1318 ~v0 ~v1 ~v2 ~v3 v4 v5 = du_refl_1318 v4 v5
du_refl_1318 ::
(AgdaAny -> AgdaAny) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_refl_1318 v0 v1 = coe du_reflexive_1316 (coe v0) (coe v1)
d_trans_1348 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_trans_1348 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10 ~v11 v12
v13 v14 v15 v16 v17
= du_trans_1348 v12 v13 v14 v15 v16 v17
du_trans_1348 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
du_trans_1348 v0 v1 v2 v3 v4 v5
= case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe seq (coe v4) (coe v5)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v9
-> case coe v3 of
(:) v10 v11
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_trans_1348 (coe v0) (coe v1) (coe v2) (coe v11) (coe v4)
(coe v9))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v10 v11
-> case coe v2 of
(:) v12 v13
-> case coe v3 of
(:) v14 v15
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v19
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(coe
du_trans_1348 (coe v0) (coe v1) (coe v13) (coe v15) (coe v19)
(coe v11))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v20 v21
-> case coe v1 of
(:) v22 v23
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
(coe v0 v22 v12 v14 v20 v10)
(coe
du_trans_1348 (coe v0) (coe v23) (coe v13) (coe v15)
(coe v21) (coe v11))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_antisym_1396 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_antisym_1396 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11 v12
v13 v14
= du_antisym_1396 v10 v11 v12 v13 v14
du_antisym_1396 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_antisym_1396 v0 v1 v2 v3 v4
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
seq (coe v4)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v8
-> coe
seq (coe v4) (coe MAlonzo.Code.Data.Empty.du_'8869''45'elim_10)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v9 v10
-> case coe v1 of
(:) v11 v12
-> case coe v2 of
(:) v13 v14
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v18
-> coe MAlonzo.Code.Data.Empty.du_'8869''45'elim_10
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v19 v20
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
(coe v0 v11 v13 v9 v19)
(coe
du_antisym_1396 (coe v0) (coe v12) (coe v14) (coe v10)
(coe v20))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_sublist'63'_1478 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_sublist'63'_1478 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
= du_sublist'63'_1478 v6 v7 v8
du_sublist'63'_1478 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_sublist'63'_1478 v0 v1 v2
= case coe v1 of
[]
-> coe
MAlonzo.Code.Relation.Nullary.C__because__46
(coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(coe
MAlonzo.Code.Relation.Nullary.C_of'696'_22
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v2)))
(:) v3 v4
-> case coe v2 of
[]
-> coe
MAlonzo.Code.Relation.Nullary.C__because__46
(coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(coe MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
(:) v5 v6
-> let v7 = coe v0 v3 v5 in
case coe v7 of
MAlonzo.Code.Relation.Nullary.C__because__46 v8 v9
-> if coe v8
then coe
MAlonzo.Code.Relation.Nullary.Decidable.du_map_14
(coe
du_'8759''8315''185'_1208 (coe v6)
(coe
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20
(coe v9)))
(coe du_sublist'63'_1478 (coe v0) (coe v4) (coe v6))
else coe
MAlonzo.Code.Relation.Nullary.Decidable.du_map_14
(coe du_'8759''691''8315''185'_1214)
(coe du_sublist'63'_1478 (coe v0) (coe v1) (coe v6))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_isPreorder_1534 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_1534 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
= du_isPreorder_1534 v6
du_isPreorder_1534 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_1534 v0
= coe
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_2409
(coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
(coe
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
(coe v0)))
(coe
(\ v1 v2 v3 ->
coe
du_fromPointwise_108 (coe v1) (coe v2)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.du_map_120
(coe
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (coe v0))
(coe v1) (coe v2) (coe v3))))
(coe
du_trans_1348
(coe MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (coe v0)))
d_isPartialOrder_1570 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_isPartialOrder_1570 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
= du_isPartialOrder_1570 v6
du_isPartialOrder_1570 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_isPartialOrder_1570 v0
= coe
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_6659
(coe
du_isPreorder_1534
(coe
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (coe v0)))
(coe
du_antisym_1396
(coe
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172 (coe v0)))
d_isDecPartialOrder_1610 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_isDecPartialOrder_1610 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
= du_isDecPartialOrder_1610 v6
du_isDecPartialOrder_1610 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_isDecPartialOrder_1610 v0
= coe
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_8061
(coe
du_isPartialOrder_1570
(coe
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_216
(coe v0)))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
(coe
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__218 (coe v0)))
(coe
du_sublist'63'_1478
(coe
MAlonzo.Code.Relation.Binary.Structures.d__'8804''63'__220
(coe v0)))
d_preorder_1672 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_1672 ~v0 ~v1 ~v2 v3 = du_preorder_1672 v3
du_preorder_1672 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_1672 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_1855
(coe
du_isPreorder_1534
(coe
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (coe v0)))
d_poset_1728 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_poset_1728 ~v0 ~v1 ~v2 v3 = du_poset_1728 v3
du_poset_1728 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_poset_1728 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_4405
(coe
du_isPartialOrder_1570
(coe
MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_304
(coe v0)))
d_decPoset_1790 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
d_decPoset_1790 ~v0 ~v1 ~v2 v3 = du_decPoset_1790 v3
du_decPoset_1790 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
du_decPoset_1790 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_5757
(coe
du_isDecPartialOrder_1610
(coe
MAlonzo.Code.Relation.Binary.Bundles.d_isDecPartialOrder_382
(coe v0)))
d__'8838'__1880 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() -> (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'8838'__1880 = erased
d_DisjointUnion'8594'Disjoint_1896 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
d_DisjointUnion'8594'Disjoint_1896 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
v9 v10 v11 v12 v13
= du_DisjointUnion'8594'Disjoint_1896 v6 v7 v8 v9 v10 v11 v12 v13
du_DisjointUnion'8594'Disjoint_1896 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
du_DisjointUnion'8594'Disjoint_1896 v0 v1 v2 v3 v4 v5 v6 v7
= case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v16
-> case coe v2 of
(:) v17 v18
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v26
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v30
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_DisjointUnion'8594'Disjoint_1896 (coe v0) (coe v1)
(coe v18) (coe v3) (coe v22) (coe v26) (coe v30)
(coe v16))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240 v18
-> case coe v0 of
(:) v19 v20
-> case coe v2 of
(:) v21 v22
-> case coe v3 of
(:) v23 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v29 v30
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v34
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v39 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164
(coe
du_DisjointUnion'8594'Disjoint_1896
(coe v20) (coe v1) (coe v22) (coe v24)
(coe v30) (coe v34) (coe v40) (coe v18))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262 v18
-> case coe v1 of
(:) v19 v20
-> case coe v2 of
(:) v21 v22
-> case coe v3 of
(:) v23 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v28
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v33 v34
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v39 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182
(coe
du_DisjointUnion'8594'Disjoint_1896
(coe v0) (coe v20) (coe v22) (coe v24)
(coe v28) (coe v34) (coe v40) (coe v18))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_Disjoint'8594'DisjointUnion_1924 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_Disjoint'8594'DisjointUnion_1924 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
v9 v10 v11
= du_Disjoint'8594'DisjointUnion_1924 v6 v7 v8 v9 v10 v11
du_Disjoint'8594'DisjointUnion_1924 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_Disjoint'8594'DisjointUnion_1924 v0 v1 v2 v3 v4 v5
= case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132
-> coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146 v12
-> case coe v2 of
(:) v13 v14
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v18
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1)
(coe v14) (coe v18) (coe v22) (coe v12)))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
(MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0)
(coe v1) (coe v14) (coe v18) (coe v22)
(coe v12)))))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0)
(coe v1) (coe v14) (coe v18) (coe v22)
(coe v12))))))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164 v14
-> case coe v0 of
(:) v15 v16
-> case coe v2 of
(:) v17 v18
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v23 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v28
-> coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v15)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v16)
(coe v1) (coe v18) (coe v24) (coe v28)
(coe v14))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v23
(MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924
(coe v16) (coe v1) (coe v18) (coe v24)
(coe v28) (coe v14)))))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
(MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924
(coe v16) (coe v1) (coe v18) (coe v24)
(coe v28) (coe v14))))))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182 v14
-> case coe v1 of
(:) v15 v16
-> case coe v2 of
(:) v17 v18
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v27 v28
-> coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v15)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0)
(coe v16) (coe v18) (coe v22) (coe v28)
(coe v14))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v27
(MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0)
(coe v16) (coe v18) (coe v22) (coe v28)
(coe v14)))))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
(MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0)
(coe v16) (coe v18) (coe v22) (coe v28)
(coe v14))))))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_'8838''45'disjoint'63'_1948 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8838''45'disjoint'63'_1948 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
v10
= du_'8838''45'disjoint'63'_1948 v6 v7 v8 v9 v10
du_'8838''45'disjoint'63'_1948 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8838''45'disjoint'63'_1948 v0 v1 v2 v3 v4
= case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
seq (coe v4)
(coe
MAlonzo.Code.Relation.Nullary.C__because__46
(coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(coe
MAlonzo.Code.Relation.Nullary.C_of'696'_22
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132)))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v8
-> case coe v2 of
(:) v9 v10
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v14
-> coe
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146)
(coe
du_'8838''45'disjoint'63'_1948 (coe v0) (coe v1) (coe v10) (coe v8)
(coe v14))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v15 v16
-> case coe v1 of
(:) v17 v18
-> coe
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182)
(coe
du_'8838''45'disjoint'63'_1948 (coe v0) (coe v18) (coe v10)
(coe v8) (coe v16))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v9 v10
-> case coe v0 of
(:) v11 v12
-> case coe v2 of
(:) v13 v14
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v18
-> coe
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164)
(coe
du_'8838''45'disjoint'63'_1948 (coe v12) (coe v1) (coe v14)
(coe v10) (coe v18))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v19 v20
-> coe
MAlonzo.Code.Relation.Nullary.C__because__46
(coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(coe MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_Disjoint'45'irrelevant_2004 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_Disjoint'45'irrelevant_2004 = erased
d_Disjoint'45'irrefl'8242'_2036 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_Disjoint'45'irrefl'8242'_2036 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8
v9
= du_Disjoint'45'irrefl'8242'_2036 v7 v8 v9
du_Disjoint'45'irrefl'8242'_2036 ::
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_Disjoint'45'irrefl'8242'_2036 v0 v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132
-> coe MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146 v9
-> case coe v0 of
(:) v10 v11
-> case coe v1 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v15
-> coe
du_Disjoint'45'irrefl'8242'_2036 (coe v11) (coe v15) (coe v9)
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_Disjoint'45'irrefl_2048 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_Disjoint'45'irrefl_2048 = erased
d_DisjointUnion'45'sym_2072 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_DisjointUnion'45'sym_2072 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
v11 v12 v13
= du_DisjointUnion'45'sym_2072 v6 v7 v8 v9 v10 v11 v12 v13
du_DisjointUnion'45'sym_2072 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
du_DisjointUnion'45'sym_2072 v0 v1 v2 v3 v4 v5 v6 v7
= case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200
-> coe v7
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v16
-> case coe v3 of
(:) v17 v18
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v26
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v30
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(coe
du_DisjointUnion'45'sym_2072 (coe v0) (coe v1) (coe v2)
(coe v18) (coe v22) (coe v26) (coe v30) (coe v16))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240 v18
-> case coe v0 of
(:) v19 v20
-> case coe v2 of
(:) v21 v22
-> case coe v3 of
(:) v23 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v29 v30
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v34
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v39 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
(coe
du_DisjointUnion'45'sym_2072 (coe v20)
(coe v1) (coe v22) (coe v24) (coe v30)
(coe v34) (coe v40) (coe v18))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262 v18
-> case coe v1 of
(:) v19 v20
-> case coe v2 of
(:) v21 v22
-> case coe v3 of
(:) v23 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v28
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v33 v34
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v39 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
(coe
du_DisjointUnion'45'sym_2072 (coe v0)
(coe v20) (coe v22) (coe v24) (coe v28)
(coe v34) (coe v40) (coe v18))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_Disjoint'45'sym_2096 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
d_Disjoint'45'sym_2096 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10 v11
= du_Disjoint'45'sym_2096 v6 v7 v8 v9 v10 v11
du_Disjoint'45'sym_2096 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
du_Disjoint'45'sym_2096 v0 v1 v2 v3 v4 v5
= case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132
-> coe v5
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146 v12
-> case coe v2 of
(:) v13 v14
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v18
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_Disjoint'45'sym_2096 (coe v0) (coe v1) (coe v14) (coe v18)
(coe v22) (coe v12))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164 v14
-> case coe v0 of
(:) v15 v16
-> case coe v2 of
(:) v17 v18
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v23 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v28
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182
(coe
du_Disjoint'45'sym_2096 (coe v16) (coe v1) (coe v18)
(coe v24) (coe v28) (coe v14))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182 v14
-> case coe v1 of
(:) v15 v16
-> case coe v2 of
(:) v17 v18
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v27 v28
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164
(coe
du_Disjoint'45'sym_2096 (coe v0) (coe v16) (coe v18)
(coe v22) (coe v28) (coe v14))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_DisjointUnion'45''91''93''737'_2118 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_DisjointUnion'45''91''93''737'_2118 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
v8 v9
= du_DisjointUnion'45''91''93''737'_2118 v6 v7 v8 v9
du_DisjointUnion'45''91''93''737'_2118 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
du_DisjointUnion'45''91''93''737'_2118 v0 v1 v2 v3
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
seq (coe v3)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v1 of
(:) v8 v9
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v13
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(coe
du_DisjointUnion'45''91''93''737'_2118 (coe v0) (coe v9) (coe v7)
(coe v13))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v14 v15
-> case coe v0 of
(:) v16 v17
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
(coe
du_DisjointUnion'45''91''93''737'_2118 (coe v17) (coe v9)
(coe v7) (coe v15))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_DisjointUnion'45''91''93''691'_2142 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_DisjointUnion'45''91''93''691'_2142 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
v8 v9
= du_DisjointUnion'45''91''93''691'_2142 v6 v7 v8 v9
du_DisjointUnion'45''91''93''691'_2142 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
du_DisjointUnion'45''91''93''691'_2142 v0 v1 v2 v3
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
seq (coe v3)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v7
-> case coe v1 of
(:) v8 v9
-> case coe v3 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v13
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(coe
du_DisjointUnion'45''91''93''691'_2142 (coe v0) (coe v9) (coe v7)
(coe v13))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v14 v15
-> case coe v0 of
(:) v16 v17
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
(coe
du_DisjointUnion'45''91''93''691'_2142 (coe v17) (coe v9)
(coe v7) (coe v15))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166 ~v0
~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9
= du_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166
v7 v8 v9
du_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166 ::
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
du_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166 v0
v1 v2
= case coe v2 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v6
-> case coe v1 of
(:) v7 v8
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(coe
du_DisjointUnion'45'fromAny'8728'toAny'45''8759''737''8315'_2166
(coe v0) (coe v8) (coe v6))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v7 v8
-> case coe v1 of
(:) v9 v10
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
(coe
du_DisjointUnion'45''91''93''737'_2118 (coe v0) (coe v10)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.du_minimum_48
(coe v10))
(coe v8))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_DisjointUnion'179'_2202 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
a13 a14 a15 a16 a17 a18
= ()
data T_DisjointUnion'179'_2202
= C_DisjointUnion'179''46'constructor_450417 [AgdaAny]
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_union'179'_2240 :: T_DisjointUnion'179'_2202 -> [AgdaAny]
d_union'179'_2240 v0
= case coe v0 of
C_DisjointUnion'179''46'constructor_450417 v1 v2 v3 v4 v5 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
d_sub'179'_2242 ::
T_DisjointUnion'179'_2202 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26
d_sub'179'_2242 v0
= case coe v0 of
C_DisjointUnion'179''46'constructor_450417 v1 v2 v3 v4 v5 -> coe v2
_ -> MAlonzo.RTE.mazUnreachableError
d_join'8321'_2244 ::
T_DisjointUnion'179'_2202 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_join'8321'_2244 v0
= case coe v0 of
C_DisjointUnion'179''46'constructor_450417 v1 v2 v3 v4 v5 -> coe v3
_ -> MAlonzo.RTE.mazUnreachableError
d_join'8322'_2246 ::
T_DisjointUnion'179'_2202 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_join'8322'_2246 v0
= case coe v0 of
C_DisjointUnion'179''46'constructor_450417 v1 v2 v3 v4 v5 -> coe v4
_ -> MAlonzo.RTE.mazUnreachableError
d_join'8323'_2248 ::
T_DisjointUnion'179'_2202 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_join'8323'_2248 v0
= case coe v0 of
C_DisjointUnion'179''46'constructor_450417 v1 v2 v3 v4 v5 -> coe v5
_ -> MAlonzo.RTE.mazUnreachableError
d__'8759''691''45'DisjointUnion'179'__2278 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
d__'8759''691''45'DisjointUnion'179'__2278 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
~v6 ~v7 ~v8 ~v9 ~v10 ~v11 ~v12 ~v13 ~v14 ~v15 ~v16 ~v17
~v18 ~v19 v20
= du__'8759''691''45'DisjointUnion'179'__2278 v20
du__'8759''691''45'DisjointUnion'179'__2278 ::
T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
du__'8759''691''45'DisjointUnion'179'__2278 v0
= case coe v0 of
C_DisjointUnion'179''46'constructor_450417 v1 v2 v3 v4 v5
-> coe
C_DisjointUnion'179''46'constructor_450417 (coe v1)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36
v2)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
v3)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
v4)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
v5)
_ -> MAlonzo.RTE.mazUnreachableError
d__'8759''8321''45'DisjointUnion'179'__2322 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
AgdaAny ->
AgdaAny ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
d__'8759''8321''45'DisjointUnion'179'__2322 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
~v6 ~v7 ~v8 ~v9 ~v10 ~v11 ~v12 ~v13 ~v14 ~v15 ~v16 ~v17
~v18 v19 ~v20 v21 v22
= du__'8759''8321''45'DisjointUnion'179'__2322 v19 v21 v22
du__'8759''8321''45'DisjointUnion'179'__2322 ::
AgdaAny ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
du__'8759''8321''45'DisjointUnion'179'__2322 v0 v1 v2
= case coe v2 of
C_DisjointUnion'179''46'constructor_450417 v3 v4 v5 v6 v7
-> coe
C_DisjointUnion'179''46'constructor_450417
(coe
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v0) (coe v3))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v1 v4)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
v5)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
v6)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
v7)
_ -> MAlonzo.RTE.mazUnreachableError
d__'8759''8322''45'DisjointUnion'179'__2366 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
AgdaAny ->
AgdaAny ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
d__'8759''8322''45'DisjointUnion'179'__2366 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
~v6 ~v7 ~v8 ~v9 ~v10 ~v11 ~v12 ~v13 ~v14 ~v15 ~v16 ~v17
~v18 v19 ~v20 v21 v22
= du__'8759''8322''45'DisjointUnion'179'__2366 v19 v21 v22
du__'8759''8322''45'DisjointUnion'179'__2366 ::
AgdaAny ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
du__'8759''8322''45'DisjointUnion'179'__2366 v0 v1 v2
= case coe v2 of
C_DisjointUnion'179''46'constructor_450417 v3 v4 v5 v6 v7
-> coe
C_DisjointUnion'179''46'constructor_450417
(coe
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v0) (coe v3))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v1 v4)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
v5)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
v6)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
v7)
_ -> MAlonzo.RTE.mazUnreachableError
d__'8759''8323''45'DisjointUnion'179'__2410 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
AgdaAny ->
AgdaAny ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
d__'8759''8323''45'DisjointUnion'179'__2410 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
~v6 ~v7 ~v8 ~v9 ~v10 ~v11 ~v12 ~v13 ~v14 ~v15 ~v16 ~v17
~v18 v19 ~v20 v21 v22
= du__'8759''8323''45'DisjointUnion'179'__2410 v19 v21 v22
du__'8759''8323''45'DisjointUnion'179'__2410 ::
AgdaAny ->
AgdaAny -> T_DisjointUnion'179'_2202 -> T_DisjointUnion'179'_2202
du__'8759''8323''45'DisjointUnion'179'__2410 v0 v1 v2
= case coe v2 of
C_DisjointUnion'179''46'constructor_450417 v3 v4 v5 v6 v7
-> coe
C_DisjointUnion'179''46'constructor_450417
(coe
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v0) (coe v3))
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46
v1 v4)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
v5)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
v6)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
v7)
_ -> MAlonzo.RTE.mazUnreachableError
d_disjointUnion'179'_2448 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
T_DisjointUnion'179'_2202
d_disjointUnion'179'_2448 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10
v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
= du_disjointUnion'179'_2448
v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21
du_disjointUnion'179'_2448 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
T_DisjointUnion'179'_2202
du_disjointUnion'179'_2448 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
v12 v13 v14 v15
= case coe v13 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200
-> coe
seq (coe v14)
(coe
seq (coe v15)
(coe
C_DisjointUnion'179''46'constructor_450417
(coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28)
(coe v13) (coe v13) (coe v13)))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v24
-> case coe v3 of
(:) v25 v26
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v30
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v34
-> case coe v10 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v38
-> case coe v14 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v47
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v51
-> case coe v11 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v55
-> case coe v15 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v64
-> case coe v12 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v68
-> coe
du__'8759''691''45'DisjointUnion'179'__2278
(coe
du_disjointUnion'179'_2448
(coe v0) (coe v1)
(coe v2) (coe v26)
(coe v30) (coe v34)
(coe v51) (coe v7)
(coe v8) (coe v9)
(coe v38) (coe v55)
(coe v68) (coe v24)
(coe v47) (coe v64))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262 v49
-> case coe v2 of
(:) v50 v51
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v56 v57
-> case coe v8 of
(:) v58 v59
-> case coe v11 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v64 v65
-> case coe v15 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262 v76
-> case coe v9 of
(:) v77 v78
-> case coe
v12 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v83 v84
-> coe
du__'8759''8323''45'DisjointUnion'179'__2410
(coe
v50)
(coe
v56)
(coe
du_disjointUnion'179'_2448
(coe
v0)
(coe
v1)
(coe
v51)
(coe
v26)
(coe
v30)
(coe
v34)
(coe
v57)
(coe
v7)
(coe
v59)
(coe
v78)
(coe
v38)
(coe
v65)
(coe
v84)
(coe
v24)
(coe
v49)
(coe
v76))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240 v26
-> case coe v0 of
(:) v27 v28
-> case coe v3 of
(:) v29 v30
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v35 v36
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v40
-> case coe v7 of
(:) v41 v42
-> case coe v10 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v47 v48
-> case coe v14 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240 v59
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v63
-> case coe v8 of
(:) v64 v65
-> case coe v11 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v70 v71
-> case coe v15 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v80
-> case coe
v12 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v84
-> coe
du__'8759''8321''45'DisjointUnion'179'__2322
(coe
v27)
(coe
v35)
(coe
du_disjointUnion'179'_2448
(coe
v28)
(coe
v1)
(coe
v2)
(coe
v30)
(coe
v36)
(coe
v40)
(coe
v63)
(coe
v42)
(coe
v65)
(coe
v9)
(coe
v48)
(coe
v71)
(coe
v84)
(coe
v26)
(coe
v59)
(coe
v80))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262 v26
-> case coe v1 of
(:) v27 v28
-> case coe v3 of
(:) v29 v30
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v34
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v39 v40
-> case coe v7 of
(:) v41 v42
-> case coe v10 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v47 v48
-> case coe v14 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v57
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v61
-> case coe v11 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v65
-> case coe v15 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240 v76
-> case coe v9 of
(:) v77 v78
-> case coe
v12 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v83 v84
-> coe
du__'8759''8322''45'DisjointUnion'179'__2366
(coe
v27)
(coe
v39)
(coe
du_disjointUnion'179'_2448
(coe
v0)
(coe
v28)
(coe
v2)
(coe
v30)
(coe
v34)
(coe
v40)
(coe
v61)
(coe
v42)
(coe
v8)
(coe
v78)
(coe
v48)
(coe
v65)
(coe
v84)
(coe
v26)
(coe
v57)
(coe
v76))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_disjoint'8658'disjoint'45'to'45'union_2514 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
d_disjoint'8658'disjoint'45'to'45'union_2514 ~v0 ~v1 ~v2 ~v3 ~v4
~v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
= du_disjoint'8658'disjoint'45'to'45'union_2514
v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17
du_disjoint'8658'disjoint'45'to'45'union_2514 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
du_disjoint'8658'disjoint'45'to'45'union_2514 v0 v1 v2 v3 v4 v5 v6
v7 v8 v9 v10 v11
= coe
du_DisjointUnion'8594'Disjoint_1896 (coe v0) (coe v3) (coe v4)
(coe
d_union'179'_2240
(coe
du_disjointUnion'179'_2448 (coe v0) (coe v1) (coe v2) (coe v4)
(coe v5) (coe v6) (coe v7)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9)))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10)))
(coe v3)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10))))
(coe v8)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10))))
(coe v11)))
(coe v5) (coe v8)
(coe
d_sub'179'_2242
(coe
du_disjointUnion'179'_2448 (coe v0) (coe v1) (coe v2) (coe v4)
(coe v5) (coe v6) (coe v7)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9)))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10)))
(coe v3)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10))))
(coe v8)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10))))
(coe v11)))
(coe
d_join'8321'_2244
(coe
du_disjointUnion'179'_2448 (coe v0) (coe v1) (coe v2) (coe v4)
(coe v5) (coe v6) (coe v7)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9)))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10)))
(coe v3)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10))))
(coe v8)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v1) (coe v4)
(coe v5) (coe v6) (coe v9))))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe
du_Disjoint'8594'DisjointUnion_1924 (coe v0) (coe v2) (coe v4)
(coe v5) (coe v7) (coe v10))))
(coe v11)))
d_weakenDisjointUnion_2572 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
d_weakenDisjointUnion_2572 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
~v10 ~v11 ~v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
= du_weakenDisjointUnion_2572
v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
du_weakenDisjointUnion_2572 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_DisjointUnion_198
du_weakenDisjointUnion_2572 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9
= case coe v8 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
seq (coe v9)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_200)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v13
-> case coe v4 of
(:) v14 v15
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(coe
du_weakenDisjointUnion_2572 (coe v0) (coe v1) (coe v2) (coe v3)
(coe v15) (coe v5) (coe v6) (coe v7) (coe v13) (coe v9))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v14 v15
-> case coe v3 of
(:) v16 v17
-> case coe v4 of
(:) v18 v19
-> case coe v9 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218 v28
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v32
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v36
-> case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__218
(coe
du_weakenDisjointUnion_2572 (coe v0)
(coe v1) (coe v2) (coe v17) (coe v19)
(coe v32) (coe v36) (coe v40) (coe v15)
(coe v28))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240 v30
-> case coe v0 of
(:) v31 v32
-> case coe v2 of
(:) v33 v34
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v39 v40
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v44
-> case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v49 v50
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__240
(coe
du_weakenDisjointUnion_2572
(coe v32) (coe v1) (coe v34)
(coe v17) (coe v19)
(coe v40) (coe v44)
(coe v50) (coe v15)
(coe v30))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262 v30
-> case coe v1 of
(:) v31 v32
-> case coe v2 of
(:) v33 v34
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v38
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v43 v44
-> case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v49 v50
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__262
(coe
du_weakenDisjointUnion_2572
(coe v0) (coe v32) (coe v34)
(coe v17) (coe v19)
(coe v38) (coe v44)
(coe v50) (coe v15)
(coe v30))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_weakenDisjoint_2616 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
d_weakenDisjoint_2616 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
~v11 ~v12 v13 v14 v15 v16 v17 v18 v19 v20
= du_weakenDisjoint_2616 v13 v14 v15 v16 v17 v18 v19 v20
du_weakenDisjoint_2616 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
du_weakenDisjoint_2616 v0 v1 v2 v3 v4 v5 v6 v7
= case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C_'91''93'_28
-> coe
seq (coe v7)
(coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132)
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v11
-> case coe v3 of
(:) v12 v13
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_weakenDisjoint_2616 (coe v0) (coe v1) (coe v2) (coe v13)
(coe v4) (coe v5) (coe v11) (coe v7))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v12 v13
-> case coe v2 of
(:) v14 v15
-> case coe v3 of
(:) v16 v17
-> case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146 v24
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v28
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v32
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_weakenDisjoint_2616 (coe v0) (coe v1)
(coe v15) (coe v17) (coe v28) (coe v32) (coe v13)
(coe v24))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164 v26
-> case coe v0 of
(:) v27 v28
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v33 v34
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v38
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164
(coe
du_weakenDisjoint_2616 (coe v28) (coe v1)
(coe v15) (coe v17) (coe v34) (coe v38)
(coe v13) (coe v26))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182 v26
-> case coe v1 of
(:) v27 v28
-> case coe v4 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v32
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v37 v38
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182
(coe
du_weakenDisjoint_2616 (coe v0) (coe v28)
(coe v15) (coe v17) (coe v32) (coe v38)
(coe v13) (coe v26))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_shrinkDisjoint_2664 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
d_shrinkDisjoint_2664 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
~v11 ~v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
= du_shrinkDisjoint_2664 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22
du_shrinkDisjoint_2664 ::
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.T_Sublist_26 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130 ->
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.T_Disjoint_130
du_shrinkDisjoint_2664 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9
= case coe v9 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C_'91''93'_132
-> coe seq (coe v5) (coe seq (coe v7) (coe v9))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146 v16
-> case coe v4 of
(:) v17 v18
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v22
-> case coe v8 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v26
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_shrinkDisjoint_2664 (coe v0) (coe v1) (coe v2) (coe v3)
(coe v18) (coe v5) (coe v22) (coe v7) (coe v26) (coe v16))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164 v18
-> case coe v2 of
(:) v19 v20
-> case coe v4 of
(:) v21 v22
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v27 v28
-> case coe v8 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v32
-> case coe v5 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v36
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_shrinkDisjoint_2664 (coe v0) (coe v1)
(coe v20) (coe v3) (coe v22) (coe v36) (coe v28)
(coe v7) (coe v32) (coe v18))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v37 v38
-> case coe v0 of
(:) v39 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8343'__164
(coe
du_shrinkDisjoint_2664 (coe v40) (coe v1)
(coe v20) (coe v3) (coe v22) (coe v38)
(coe v28) (coe v7) (coe v32) (coe v18))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182 v18
-> case coe v3 of
(:) v19 v20
-> case coe v4 of
(:) v21 v22
-> case coe v6 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v26
-> case coe v8 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v31 v32
-> case coe v7 of
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759''691'__36 v36
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''8345'__146
(coe
du_shrinkDisjoint_2664 (coe v0) (coe v1) (coe v2)
(coe v20) (coe v22) (coe v5) (coe v26) (coe v36)
(coe v32) (coe v18))
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.Core.C__'8759'__46 v37 v38
-> case coe v1 of
(:) v39 v40
-> coe
MAlonzo.Code.Data.List.Relation.Binary.Sublist.Heterogeneous.C__'8759''7523'__182
(coe
du_shrinkDisjoint_2664 (coe v0) (coe v40)
(coe v2) (coe v20) (coe v22) (coe v5)
(coe v26) (coe v38) (coe v32) (coe v18))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError