{-# 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.Relation.Binary.Reasoning.Base.Single where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Primitive

-- Relation.Binary.Reasoning.Base.Single._IsRelatedTo_
d__IsRelatedTo__26 :: p -> p -> p -> p -> p -> p -> p -> p -> ()
d__IsRelatedTo__26 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 = ()
newtype T__IsRelatedTo__26 = C_relTo_34 AgdaAny
-- Relation.Binary.Reasoning.Base.Single.begin_
d_begin__40 :: T__IsRelatedTo__26 -> AgdaAny
d_begin__40 :: T__IsRelatedTo__26 -> AgdaAny
d_begin__40 T__IsRelatedTo__26
v0
  = case T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0 of
      C_relTo_34 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T__IsRelatedTo__26
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Single.step-∼
d_step'45''8764'_50 ::
  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 ->
  AgdaAny -> T__IsRelatedTo__26 -> AgdaAny -> T__IsRelatedTo__26
d_step'45''8764'_50 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
d_step'45''8764'_50 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 T__IsRelatedTo__26
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8764'_50 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 T__IsRelatedTo__26
v9 AgdaAny
v10
du_step'45''8764'_50 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__26 -> AgdaAny -> T__IsRelatedTo__26
du_step'45''8764'_50 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8764'_50 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__26
v4 AgdaAny
v5
  = case T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v4 of
      C_relTo_34 AgdaAny
v6 -> (AgdaAny -> T__IsRelatedTo__26) -> AgdaAny -> T__IsRelatedTo__26
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__26
C_relTo_34 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5 AgdaAny
v6)
      T__IsRelatedTo__26
_ -> T__IsRelatedTo__26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Single.step-≡
d_step'45''8801'_62 ::
  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 ->
  AgdaAny ->
  T__IsRelatedTo__26 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__26
d_step'45''8801'_62 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__'8801'__12
-> T__IsRelatedTo__26
d_step'45''8801'_62 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny -> AgdaAny
v4 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__26
v9 ~T__'8801'__12
v10
  = T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801'_62 T__IsRelatedTo__26
v9
du_step'45''8801'_62 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801'_62 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801'_62 T__IsRelatedTo__26
v0 = T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0
-- Relation.Binary.Reasoning.Base.Single.step-≡˘
d_step'45''8801''728'_72 ::
  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 ->
  AgdaAny ->
  T__IsRelatedTo__26 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__26
d_step'45''8801''728'_72 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__'8801'__12
-> T__IsRelatedTo__26
d_step'45''8801''728'_72 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny -> AgdaAny
v4 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__26
v9
                         ~T__'8801'__12
v10
  = T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801''728'_72 T__IsRelatedTo__26
v9
du_step'45''8801''728'_72 ::
  T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801''728'_72 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801''728'_72 T__IsRelatedTo__26
v0 = T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0
-- Relation.Binary.Reasoning.Base.Single._≡⟨⟩_
d__'8801''10216''10217'__80 ::
  T__IsRelatedTo__26 -> T__IsRelatedTo__26
d__'8801''10216''10217'__80 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
d__'8801''10216''10217'__80 T__IsRelatedTo__26
v0 = T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0
-- Relation.Binary.Reasoning.Base.Single._∎
d__'8718'_86 ::
  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 -> T__IsRelatedTo__26
d__'8718'_86 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T__IsRelatedTo__26
d__'8718'_86 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny
v4 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 = (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
du__'8718'_86 AgdaAny -> AgdaAny
v4 AgdaAny
v6
du__'8718'_86 ::
  (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
du__'8718'_86 :: (AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
du__'8718'_86 AgdaAny -> AgdaAny
v0 AgdaAny
v1 = (AgdaAny -> T__IsRelatedTo__26) -> AgdaAny -> T__IsRelatedTo__26
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__26
C_relTo_34 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1)