{-# 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.Builtin.List
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 UntypedPlutusCore.Transform.Certify.Trace
import qualified UntypedPlutusCore.Transform.Certify.Hints as Hints
-- VerifiedCompilation.Certificate.SimplifierTag
d_SimplifierTag_4 :: ()
d_SimplifierTag_4 = ()
type T_SimplifierTag_4 = SimplifierStage
pattern $mC_floatDelayT_6 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_floatDelayT_6 :: SimplifierStage
C_floatDelayT_6 = FloatDelay
pattern $mC_forceDelayT_8 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceDelayT_8 :: SimplifierStage
C_forceDelayT_8 = ForceDelay
pattern $mC_forceCaseDelayT_10 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceCaseDelayT_10 :: SimplifierStage
C_forceCaseDelayT_10 = ForceCaseDelay
pattern $mC_caseOfCaseT_12 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseOfCaseT_12 :: SimplifierStage
C_caseOfCaseT_12 = CaseOfCase
pattern $mC_caseReduceT_14 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseReduceT_14 :: SimplifierStage
C_caseReduceT_14 = CaseReduce
pattern $mC_inlineT_16 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_inlineT_16 :: SimplifierStage
C_inlineT_16 = Inline
pattern $mC_cseT_18 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_cseT_18 :: SimplifierStage
C_cseT_18 = CSE
check_floatDelayT_6 :: T_SimplifierTag_4
check_floatDelayT_6 :: SimplifierStage
check_floatDelayT_6 = SimplifierStage
FloatDelay
check_forceDelayT_8 :: T_SimplifierTag_4
check_forceDelayT_8 :: SimplifierStage
check_forceDelayT_8 = SimplifierStage
ForceDelay
check_forceCaseDelayT_10 :: T_SimplifierTag_4
check_forceCaseDelayT_10 :: SimplifierStage
check_forceCaseDelayT_10 = SimplifierStage
ForceCaseDelay
check_caseOfCaseT_12 :: T_SimplifierTag_4
check_caseOfCaseT_12 :: SimplifierStage
check_caseOfCaseT_12 = SimplifierStage
CaseOfCase
check_caseReduceT_14 :: T_SimplifierTag_4
check_caseReduceT_14 :: SimplifierStage
check_caseReduceT_14 = SimplifierStage
CaseReduce
check_inlineT_16 :: T_SimplifierTag_4
check_inlineT_16 :: SimplifierStage
check_inlineT_16 = SimplifierStage
Inline
check_cseT_18 :: T_SimplifierTag_4
check_cseT_18 :: SimplifierStage
check_cseT_18 = SimplifierStage
CSE
cover_SimplifierTag_4 :: SimplifierStage -> ()
cover_SimplifierTag_4 :: SimplifierStage -> ()
cover_SimplifierTag_4 SimplifierStage
x
  = case SimplifierStage
x of
      SimplifierStage
FloatDelay -> ()
      SimplifierStage
ForceDelay -> ()
      SimplifierStage
ForceCaseDelay -> ()
      SimplifierStage
CaseOfCase -> ()
      SimplifierStage
CaseReduce -> ()
      SimplifierStage
Inline -> ()
      SimplifierStage
CSE -> ()
-- VerifiedCompilation.Certificate.InlineHints
d_InlineHints_20 :: ()
d_InlineHints_20 = ()
type T_InlineHints_20 = Hints.Inline
pattern $mC_var_22 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_var_22 :: Inline
C_var_22 = Hints.InlVar
pattern $mC_expand_24 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_expand_24 :: Inline -> Inline
C_expand_24 a0 = Hints.InlExpand a0
pattern $mC_ƛ_26 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_ƛ_26 :: Inline -> Inline
C_ƛ_26 a0 = Hints.InlLam a0
pattern $mC__'183'__28 :: forall {r}. Inline -> (Inline -> Inline -> r) -> ((# #) -> r) -> r
$bC__'183'__28 :: Inline -> Inline -> Inline
C__'183'__28 a0 a1 = Hints.InlApply a0 a1
pattern $mC__'183''8595'_30 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC__'183''8595'_30 :: Inline -> Inline
C__'183''8595'_30 a0 = Hints.InlDrop a0
pattern $mC_force_32 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_force_32 :: Inline -> Inline
C_force_32 a0 = Hints.InlForce a0
pattern $mC_delay_34 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_delay_34 :: Inline -> Inline
C_delay_34 a0 = Hints.InlDelay a0
pattern $mC_con_36 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_con_36 :: Inline
C_con_36 = Hints.InlCon
pattern $mC_builtin_38 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_builtin_38 :: Inline
C_builtin_38 = Hints.InlBuiltin
pattern $mC_error_40 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_error_40 :: Inline
C_error_40 = Hints.InlError
pattern $mC_constr_42 :: forall {r}. Inline -> ([Inline] -> r) -> ((# #) -> r) -> r
$bC_constr_42 :: [Inline] -> Inline
C_constr_42 a0 = Hints.InlConstr a0
pattern $mC_case_44 :: forall {r}.
Inline -> (Inline -> [Inline] -> r) -> ((# #) -> r) -> r
$bC_case_44 :: Inline -> [Inline] -> Inline
C_case_44 a0 a1 = Hints.InlCase a0 a1
check_var_22 :: T_InlineHints_20
check_var_22 :: Inline
check_var_22 = Inline
Hints.InlVar
check_expand_24 :: T_InlineHints_20 -> T_InlineHints_20
check_expand_24 :: Inline -> Inline
check_expand_24 = Inline -> Inline
Hints.InlExpand
check_ƛ_26 :: T_InlineHints_20 -> T_InlineHints_20
check_ƛ_26 :: Inline -> Inline
check_ƛ_26 = Inline -> Inline
Hints.InlLam
check__'183'__28 ::
  T_InlineHints_20 -> T_InlineHints_20 -> T_InlineHints_20
check__'183'__28 :: Inline -> Inline -> Inline
check__'183'__28 = Inline -> Inline -> Inline
Hints.InlApply
check__'183''8595'_30 :: T_InlineHints_20 -> T_InlineHints_20
check__'183''8595'_30 :: Inline -> Inline
check__'183''8595'_30 = Inline -> Inline
Hints.InlDrop
check_force_32 :: T_InlineHints_20 -> T_InlineHints_20
check_force_32 :: Inline -> Inline
check_force_32 = Inline -> Inline
Hints.InlForce
check_delay_34 :: T_InlineHints_20 -> T_InlineHints_20
check_delay_34 :: Inline -> Inline
check_delay_34 = Inline -> Inline
Hints.InlDelay
check_con_36 :: T_InlineHints_20
check_con_36 :: Inline
check_con_36 = Inline
Hints.InlCon
check_builtin_38 :: T_InlineHints_20
check_builtin_38 :: Inline
check_builtin_38 = Inline
Hints.InlBuiltin
check_error_40 :: T_InlineHints_20
check_error_40 :: Inline
check_error_40 = Inline
Hints.InlError
check_constr_42 ::
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_20 ->
  T_InlineHints_20
check_constr_42 :: [Inline] -> Inline
check_constr_42 = [Inline] -> Inline
Hints.InlConstr
check_case_44 ::
  T_InlineHints_20 ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_20 ->
  T_InlineHints_20
check_case_44 :: Inline -> [Inline] -> Inline
check_case_44 = Inline -> [Inline] -> Inline
Hints.InlCase
cover_InlineHints_20 :: Hints.Inline -> ()
cover_InlineHints_20 :: Inline -> ()
cover_InlineHints_20 Inline
x
  = case Inline
x of
      Inline
Hints.InlVar -> ()
      Hints.InlExpand Inline
_ -> ()
      Hints.InlLam Inline
_ -> ()
      Hints.InlApply Inline
_ Inline
_ -> ()
      Hints.InlDrop Inline
_ -> ()
      Hints.InlForce Inline
_ -> ()
      Hints.InlDelay Inline
_ -> ()
      Inline
Hints.InlCon -> ()
      Inline
Hints.InlBuiltin -> ()
      Inline
Hints.InlError -> ()
      Hints.InlConstr [Inline]
_ -> ()
      Hints.InlCase Inline
_ [Inline]
_ -> ()
-- VerifiedCompilation.Certificate.Hints
d_Hints_46 :: ()
d_Hints_46 = ()
type T_Hints_46 = Hints.Hints
pattern $mC_inline_48 :: forall {r}. Hints -> (Inline -> r) -> ((# #) -> r) -> r
$bC_inline_48 :: Inline -> Hints
C_inline_48 a0 = Hints.Inline a0
pattern $mC_none_50 :: forall {r}. Hints -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_none_50 :: Hints
C_none_50 = Hints.NoHints
check_inline_48 :: T_InlineHints_20 -> T_Hints_46
check_inline_48 :: Inline -> Hints
check_inline_48 = Inline -> Hints
Hints.Inline
check_none_50 :: T_Hints_46
check_none_50 :: Hints
check_none_50 = Hints
Hints.NoHints
cover_Hints_46 :: Hints.Hints -> ()
cover_Hints_46 :: Hints -> ()
cover_Hints_46 Hints
x
  = case Hints
x of
      Hints.Inline Inline
_ -> ()
      Hints
Hints.NoHints -> ()
-- VerifiedCompilation.Certificate.CertResult
d_CertResult_60 :: p -> p -> ()
d_CertResult_60 p
a0 p
a1 = ()
data T_CertResult_60
  = C_proof_66 AgdaAny | C_ce_74 T_SimplifierTag_4 AgdaAny AgdaAny |
    C_abort_80 T_SimplifierTag_4 AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.ProofOrCE
d_ProofOrCE_86 :: p -> p -> ()
d_ProofOrCE_86 p
a0 p
a1 = ()
data T_ProofOrCE_86
  = C_proof_92 AgdaAny | C_ce_100 T_SimplifierTag_4 AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.Proof?
d_Proof'63'_106 :: p -> p -> ()
d_Proof'63'_106 p
a0 p
a1 = ()
data T_Proof'63'_106
  = C_proof_112 AgdaAny |
    C_abort_118 T_SimplifierTag_4 AgdaAny AgdaAny
-- VerifiedCompilation.Certificate._>>=_
d__'62''62''61'__128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  T_Proof'63'_106 -> (AgdaAny -> T_Proof'63'_106) -> T_Proof'63'_106
d__'62''62''61'__128 :: ()
-> ()
-> ()
-> ()
-> T_Proof'63'_106
-> (AgdaAny -> T_Proof'63'_106)
-> T_Proof'63'_106
d__'62''62''61'__128 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Proof'63'_106
v4 AgdaAny -> T_Proof'63'_106
v5
  = T_Proof'63'_106 -> (AgdaAny -> T_Proof'63'_106) -> T_Proof'63'_106
du__'62''62''61'__128 T_Proof'63'_106
v4 AgdaAny -> T_Proof'63'_106
v5
du__'62''62''61'__128 ::
  T_Proof'63'_106 -> (AgdaAny -> T_Proof'63'_106) -> T_Proof'63'_106
du__'62''62''61'__128 :: T_Proof'63'_106 -> (AgdaAny -> T_Proof'63'_106) -> T_Proof'63'_106
du__'62''62''61'__128 T_Proof'63'_106
v0 AgdaAny -> T_Proof'63'_106
v1
  = case T_Proof'63'_106 -> T_Proof'63'_106
forall a b. a -> b
coe T_Proof'63'_106
v0 of
      C_proof_112 AgdaAny
v2 -> (AgdaAny -> T_Proof'63'_106) -> AgdaAny -> T_Proof'63'_106
forall a b. a -> b
coe AgdaAny -> T_Proof'63'_106
v1 AgdaAny
v2
      C_abort_118 SimplifierStage
v4 AgdaAny
v5 AgdaAny
v6 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_Proof'63'_106)
-> SimplifierStage -> AgdaAny -> AgdaAny -> T_Proof'63'_106
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_Proof'63'_106
C_abort_118 SimplifierStage
v4 AgdaAny
v5 AgdaAny
v6
      T_Proof'63'_106
_ -> T_Proof'63'_106
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.decToPCE
d_decToPCE_148 ::
  () ->
  () ->
  T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_86
d_decToPCE_148 :: ()
-> ()
-> SimplifierStage
-> T_Dec_20
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_86
d_decToPCE_148 ~()
v0 ~()
v1 SimplifierStage
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5 = SimplifierStage -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
du_decToPCE_148 SimplifierStage
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5
du_decToPCE_148 ::
  T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_86
du_decToPCE_148 :: SimplifierStage -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
du_decToPCE_148 SimplifierStage
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_86) -> AgdaAny -> T_ProofOrCE_86
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_86
C_proof_92 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                    T_Reflects_16
_ -> T_ProofOrCE_86
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ProofOrCE_86
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) ((SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
C_ce_100 SimplifierStage
v0 AgdaAny
v2 AgdaAny
v3)
      T_Dec_20
_ -> T_ProofOrCE_86
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.pceToDec
d_pceToDec_162 ::
  () ->
  T_ProofOrCE_86 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pceToDec_162 :: () -> T_ProofOrCE_86 -> T_Dec_20
d_pceToDec_162 ~()
v0 T_ProofOrCE_86
v1 = T_ProofOrCE_86 -> T_Dec_20
du_pceToDec_162 T_ProofOrCE_86
v1
du_pceToDec_162 ::
  T_ProofOrCE_86 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pceToDec_162 :: T_ProofOrCE_86 -> T_Dec_20
du_pceToDec_162 T_ProofOrCE_86
v0
  = case T_ProofOrCE_86 -> T_ProofOrCE_86
forall a b. a -> b
coe T_ProofOrCE_86
v0 of
      C_proof_92 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_100 SimplifierStage
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_86
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.MatchOrCE
d_MatchOrCE_176 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> ()
d_MatchOrCE_176 :: () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_MatchOrCE_176 = () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.matchOrCE
d_matchOrCE_196 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_86
d_matchOrCE_196 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> SimplifierStage
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_86
d_matchOrCE_196 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
  = SimplifierStage
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_86
du_matchOrCE_196 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_matchOrCE_196 ::
  T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_86
du_matchOrCE_196 :: SimplifierStage
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_86
du_matchOrCE_196 SimplifierStage
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_86
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_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_86
C_proof_92 (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) ((SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
C_ce_100 SimplifierStage
v0 AgdaAny
v2 AgdaAny
v3)
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.pcePointwise
d_pcePointwise_238 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_86) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_86
d_pcePointwise_238 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_86
d_pcePointwise_238 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_86
v5 [AgdaAny]
v6 [AgdaAny]
v7
  = SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_86
du_pcePointwise_238 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_86
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_pcePointwise_238 ::
  T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_86) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_86
du_pcePointwise_238 :: SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_86
du_pcePointwise_238 SimplifierStage
v0 AgdaAny -> AgdaAny -> T_ProofOrCE_86
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_86) -> AgdaAny -> T_ProofOrCE_86
forall a b. a -> b
coe
                    AgdaAny -> T_ProofOrCE_86
C_proof_92
                    (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 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> SimplifierStage -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_86
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
C_ce_100 SimplifierStage
v0 [AgdaAny]
v2 [AgdaAny]
v5
             [AgdaAny]
_ -> T_ProofOrCE_86
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             [] -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> SimplifierStage -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_86
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
C_ce_100 SimplifierStage
v0 [AgdaAny]
v5 [AgdaAny]
v3
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_86
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_ProofOrCE_86
forall a b. a -> b
coe
                    (case AgdaAny -> T_ProofOrCE_86
forall a b. a -> b
coe AgdaAny
v8 of
                       C_proof_92 AgdaAny
v9
                         -> let v10 :: AgdaAny
v10
                                  = (SimplifierStage
 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_86)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_ProofOrCE_86)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_86
du_pcePointwise_238 (SimplifierStage -> AgdaAny
forall a b. a -> b
coe SimplifierStage
v0) ((AgdaAny -> AgdaAny -> T_ProofOrCE_86) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_86
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_86
forall a b. a -> b
coe AgdaAny
v10 of
                                 C_proof_92 AgdaAny
v11
                                   -> (AgdaAny -> T_ProofOrCE_86) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_ProofOrCE_86
C_proof_92
                                        ((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_100 SimplifierStage
v14 AgdaAny
v15 AgdaAny
v16 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
C_ce_100 SimplifierStage
v14 AgdaAny
v15 AgdaAny
v16
                                 T_ProofOrCE_86
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       C_ce_100 SimplifierStage
v12 AgdaAny
v13 AgdaAny
v14 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_86
C_ce_100 SimplifierStage
v12 AgdaAny
v13 AgdaAny
v14
                       T_ProofOrCE_86
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_ProofOrCE_86
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_ProofOrCE_86
forall a. a
MAlonzo.RTE.mazUnreachableError