{-# 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.Algebra.Consequences.Base 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.Primitive
import qualified MAlonzo.Code.Data.Sum.Base

-- Algebra.Consequences.Base._.sel⇒idem
d_sel'8658'idem_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny
d_sel'8658'idem_20 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
d_sel'8658'idem_20 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> AgdaAny
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 AgdaAny -> AgdaAny -> T__'8846'__30
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
du_sel'8658'idem_20 AgdaAny -> AgdaAny -> T__'8846'__30
v5 AgdaAny
v6
du_sel'8658'idem_20 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny
du_sel'8658'idem_20 :: (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
du_sel'8658'idem_20 AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v1
  = (T__'8846'__30 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_reduce_76 ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v1 AgdaAny
v1)
-- Algebra.Consequences.Base._.reflexive∧selfInverse⇒involutive
d_reflexive'8743'selfInverse'8658'involutive_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_reflexive'8743'selfInverse'8658'involutive_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_reflexive'8743'selfInverse'8658'involutive_36 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 AgdaAny -> AgdaAny
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4
                                                AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_reflexive'8743'selfInverse'8658'involutive_36 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_reflexive'8743'selfInverse'8658'involutive_36 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_reflexive'8743'selfInverse'8658'involutive_36 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_reflexive'8743'selfInverse'8658'involutive_36 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3))
-- Algebra.Consequences.Base.reflexive+selfInverse⇒involutive
d_reflexive'43'selfInverse'8658'involutive_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_reflexive'43'selfInverse'8658'involutive_42 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_reflexive'43'selfInverse'8658'involutive_42 ~T_Level_18
v0 ~T_Level_18
v1
  = T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_reflexive'43'selfInverse'8658'involutive_42
du_reflexive'43'selfInverse'8658'involutive_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_reflexive'43'selfInverse'8658'involutive_42 :: T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_reflexive'43'selfInverse'8658'involutive_42 T_Level_18
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> T_Level_18
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_reflexive'8743'selfInverse'8658'involutive_36 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5