{-# 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.VerifiedCompilation.Certificate 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.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.VerifiedCompilation.Trace

-- VerifiedCompilation.Certificate.CertResult
d_CertResult_12 :: p -> p -> ()
d_CertResult_12 p
a0 p
a1 = ()
data T_CertResult_12
  = C_proof_18 AgdaAny |
    C_ce_26 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
            AgdaAny AgdaAny |
    C_abort_32 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
               AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.ProofOrCE
d_ProofOrCE_38 :: p -> p -> ()
d_ProofOrCE_38 p
a0 p
a1 = ()
data T_ProofOrCE_38
  = C_proof_44 AgdaAny |
    C_ce_52 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
            AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.Proof?
d_Proof'63'_58 :: p -> p -> ()
d_Proof'63'_58 p
a0 p
a1 = ()
data T_Proof'63'_58
  = C_proof_64 AgdaAny |
    C_abort_70 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
               AgdaAny AgdaAny
-- VerifiedCompilation.Certificate._>>=_
d__'62''62''61'__80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58
d__'62''62''61'__80 :: ()
-> ()
-> ()
-> ()
-> T_Proof'63'_58
-> (AgdaAny -> T_Proof'63'_58)
-> T_Proof'63'_58
d__'62''62''61'__80 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Proof'63'_58
v4 AgdaAny -> T_Proof'63'_58
v5
  = T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58
du__'62''62''61'__80 T_Proof'63'_58
v4 AgdaAny -> T_Proof'63'_58
v5
du__'62''62''61'__80 ::
  T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58
du__'62''62''61'__80 :: T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58
du__'62''62''61'__80 T_Proof'63'_58
v0 AgdaAny -> T_Proof'63'_58
v1
  = case T_Proof'63'_58 -> T_Proof'63'_58
forall a b. a -> b
coe T_Proof'63'_58
v0 of
      C_proof_64 AgdaAny
v2 -> (AgdaAny -> T_Proof'63'_58) -> AgdaAny -> T_Proof'63'_58
forall a b. a -> b
coe AgdaAny -> T_Proof'63'_58
v1 AgdaAny
v2
      C_abort_70 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_Proof'63'_58)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_Proof'63'_58
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_Proof'63'_58
C_abort_70 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6
      T_Proof'63'_58
_ -> T_Proof'63'_58
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.DecidableCE
d_DecidableCE_100 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_100 :: () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_100 = () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.Checkable
d_Checkable_118 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_118 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_118 = () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.Certifiable
d_Certifiable_134 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_134 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_134 = () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.checker
d_checker_148 ::
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> T_Proof'63'_58) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
d_checker_148 :: ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Proof'63'_58)
-> AgdaAny
-> AgdaAny
-> T_CertResult_12
d_checker_148 ~()
v0 ~AgdaAny -> AgdaAny -> ()
v1 AgdaAny -> AgdaAny -> T_Proof'63'_58
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Proof'63'_58)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_148 AgdaAny -> AgdaAny -> T_Proof'63'_58
v2 AgdaAny
v3 AgdaAny
v4
du_checker_148 ::
  (AgdaAny -> AgdaAny -> T_Proof'63'_58) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_148 :: (AgdaAny -> AgdaAny -> T_Proof'63'_58)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_148 AgdaAny -> AgdaAny -> T_Proof'63'_58
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Proof'63'_58)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Proof'63'_58
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_CertResult_12
forall a b. a -> b
coe
      (case AgdaAny -> T_Proof'63'_58
forall a b. a -> b
coe AgdaAny
v3 of
         C_proof_64 AgdaAny
v4 -> (AgdaAny -> T_CertResult_12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_CertResult_12
C_proof_18 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
         C_abort_70 T_SimplifierTag_4
v6 AgdaAny
v7 AgdaAny
v8 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12
C_abort_32 T_SimplifierTag_4
v6 AgdaAny
v7 AgdaAny
v8
         T_Proof'63'_58
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decider
d_decider_184 ::
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
d_decider_184 :: ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny
-> AgdaAny
-> T_CertResult_12
d_decider_184 ~()
v0 ~AgdaAny -> AgdaAny -> ()
v1 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_184 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v2 AgdaAny
v3 AgdaAny
v4
du_decider_184 ::
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_184 :: (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_184 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_38
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_CertResult_12
forall a b. a -> b
coe
      (case AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny
v3 of
         C_proof_44 AgdaAny
v4 -> (AgdaAny -> T_CertResult_12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_CertResult_12
C_proof_18 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
         C_ce_52 T_SimplifierTag_4
v7 AgdaAny
v8 AgdaAny
v9 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12
C_ce_26 T_SimplifierTag_4
v7 AgdaAny
v8 AgdaAny
v9
         T_ProofOrCE_38
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decToPCE
d_decToPCE_226 ::
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
d_decToPCE_226 :: ()
-> ()
-> T_SimplifierTag_4
-> T_Dec_20
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
d_decToPCE_226 ~()
v0 ~()
v1 T_SimplifierTag_4
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5 = T_SimplifierTag_4
-> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_226 T_SimplifierTag_4
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5
du_decToPCE_226 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_226 :: T_SimplifierTag_4
-> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_226 T_SimplifierTag_4
v0 T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v6
                      -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_38
C_proof_44 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                    T_Reflects_16
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5) ((T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 AgdaAny
v2 AgdaAny
v3)
      T_Dec_20
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.pceToDec
d_pceToDec_240 ::
  () ->
  T_ProofOrCE_38 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pceToDec_240 :: () -> T_ProofOrCE_38 -> T_Dec_20
d_pceToDec_240 ~()
v0 T_ProofOrCE_38
v1 = T_ProofOrCE_38 -> T_Dec_20
du_pceToDec_240 T_ProofOrCE_38
v1
du_pceToDec_240 ::
  T_ProofOrCE_38 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pceToDec_240 :: T_ProofOrCE_38 -> T_Dec_20
du_pceToDec_240 T_ProofOrCE_38
v0
  = case T_ProofOrCE_38 -> T_ProofOrCE_38
forall a b. a -> b
coe T_ProofOrCE_38
v0 of
      C_proof_44 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
             Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      C_ce_52 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
             Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
      T_ProofOrCE_38
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.matchOrCE
d_matchOrCE_254 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
d_matchOrCE_254 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
d_matchOrCE_254 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
  = T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
du_matchOrCE_254 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_matchOrCE_254 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_matchOrCE_254 :: T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
du_matchOrCE_254 T_SimplifierTag_4
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = let v4 :: AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3 in
    AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe
      (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v4 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v7
                         -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_38
C_proof_44 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)
                       T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6) ((T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 AgdaAny
v2 AgdaAny
v3)
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.pcePointwise
d_pcePointwise_296 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
d_pcePointwise_296 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
d_pcePointwise_296 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v5 [AgdaAny]
v6 [AgdaAny]
v7
  = T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
du_pcePointwise_296 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_pcePointwise_296 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
du_pcePointwise_296 :: T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
du_pcePointwise_296 T_SimplifierTag_4
v0 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v1 [AgdaAny]
v2 [AgdaAny]
v3
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe
                    AgdaAny -> T_ProofOrCE_38
C_proof_44
                    (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe
                       T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
             (:) AgdaAny
v4 [AgdaAny]
v5 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 [AgdaAny]
v2 [AgdaAny]
v5
             [AgdaAny]
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             [] -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 [AgdaAny]
v5 [AgdaAny]
v3
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_38
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe
                    (case AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny
v8 of
                       C_proof_44 AgdaAny
v9
                         -> let v10 :: AgdaAny
v10
                                  = (T_SimplifierTag_4
 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
du_pcePointwise_296 (T_SimplifierTag_4 -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4
v0) ((AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_38
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny
v10 of
                                 C_proof_44 AgdaAny
v11
                                   -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_ProofOrCE_38
C_proof_44
                                        ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                           AgdaAny
v9 AgdaAny
v11)
                                 C_ce_52 T_SimplifierTag_4
v14 AgdaAny
v15 AgdaAny
v16 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v14 AgdaAny
v15 AgdaAny
v16
                                 T_ProofOrCE_38
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       C_ce_52 T_SimplifierTag_4
v12 AgdaAny
v13 AgdaAny
v14 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v12 AgdaAny
v13 AgdaAny
v14
                       T_ProofOrCE_38
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError